Formal Proofs

Proof Status Summary

Latest Update (Jan 7, 2026 ~02:00): SC8 theorem complete! The forward direction (SC8 → monotonicity) is fully proven with sc8_implies_k_monotone. The converse direction is FALSE — a counterexample shows that k(λ) can be monotonic even when some first-winner transitions have winner.k > curr.k (due to "shielding" candidates). The theorem has been revised from iff to forward implication only. All sorrys eliminated (0 remaining).

Note: Goals 1-4 are SOLVED. Goal 5 (regularisation) is the remaining research direction.

Current Status (Dec 27, 2025)

Proven lemmas: Full library + very strong GP infrastructure + product formula + tau-source + dominance guard lemmas + minResidualValuation partition lemmas + marginCoeffAtVal_eq_counting + marginAtBase_eq_coeff_sum_of_coprime + marginAtBase_upper_bound_of_neg_coeff + new_sum_le_R_card + minloss_fp_cmin_positive + minloss_fp_cmin_ge_one_at_margin_vmin + Category 1-3 loss comparison lemmas + TRICHOTOMY + violator→minResVal link + violator_at_margin_vmin_implies_neg_margin + minloss_fp_is_satisfier_at_margin_minimum + specialised minloss_fp_is_satisfier_at_margin_vmin + p-free predicates/residual propagation + p-free satisfier and c_{v_min} ≥ 1 wrappers + zero_new_via_minloss_fp_satisfier + exists_fit_preserving_interpolant_lt_k_lt_n_axiomFree (NEW - iteration + k=n case).

Remaining sorrys: 0 (build clean; p-free wrappers supply the coprimality side conditions automatically).

Main Theorem: ✓ COMPLETE (AXIOM-FREE) — both hyperplane_passes_through_nplusone_veryStrong and optimal_passes_through_exactly_nplusone_veryStrong depend only on standard Lean axioms!

Axioms actually used by main theorem: 0 custom axioms — only standard axioms (propext, Classical.choice, Quot.sound).

Build: ✓ Compiles successfully (3054 jobs) — warnings only (unused variables, long lines).

🎉 MILESTONE: Strong GP Theorem Complete!

Axioms Status (0 custom axioms remaining!)

🎉🎉🎉 VERY STRONG GP: FULLY AXIOM-FREE! (Dec 27, 2025)

'PadicRegression.hyperplane_passes_through_nplusone_veryStrong' depends on axioms:
  [propext, Classical.choice, Quot.sound]

'PadicRegression.optimal_passes_through_exactly_nplusone_veryStrong' depends on axioms:
  [propext, Classical.choice, Quot.sound]

🎉 Axiom Elimination COMPLETE (Dec 27, 2025 21:43 AEDT)

🎉 K=N CASE FULLY PROVEN (Dec 10, 15:00 AEDT)

🎉 TRICHOTOMY LEMMA PROVEN! (Dec 17, 2025 03:15 AEDT)

🎉 Mechanism 2 COMPLETE (Dec 24, 2025)

Mechanism 1 Pigeonhole Bound (Dec 22, 2025)

🆕 Dominance Guard Lemmas (Dec 12-13, 2025)

🆕 Counting Argument Infrastructure (Dec 13, 2025)

c_v = gains_v + orig_v - new_v

🔬 K<N CASE: LOSS TRANSFER INEQUALITY (Dec 11, 19:00 AEDT)

Σ_{t ∈ T \ {s*}} [L(h_ref, t) - L(h, t)] < G + L(h, s*)

Tau-Source Infrastructure (Dec 10)

Slack Antisymmetry Packaged (Dec 10, 00:20 AEDT)

New: Very Strong General Position (Dec 9, 22:04 AEDT)

🎉 NEW: Product Formula Proven! (Dec 9, 23:05 AEDT)

Kernel-Based Product Formula (Dec 9, 18:14 AEDT)

Simplest Case Structure (m = n+2, k = n)

Simplest Case Proof Flow

Product formula: δ_a(b)·δ_b(a) = res(h,a)·res(h,b)
        ↓
Valuation sum: v(δ_a(b)) + v(δ_b(a)) = v(res(h,a)) + v(res(h,b))
        ↓
margin_dichotomy: At least one of v(δ_a(b)) ≥ v(res(h,b)) or v(δ_b(a)) ≥ v(res(h,a)) ✓ PROVEN
        ↓
pointLoss_le_of_delta_val_ge: L(h_x, other) ≤ L(h, other) ✓ PROVEN
        ↓
exists_fit_preserving_interpolant_lt_simplest ✓ PROVEN
            

Proof Architecture (Dec 9, 2025)

hyperplane_passes_through_nplusone (wrapper, assumes strong GP) ✓ delegates
        ↓
hyperplane_passes_through_nplusone_strong (strong GP) ✓ COMPLETE
        ↓
non_interpolating_strictly_suboptimal ✓
        ↓
exists_better_hyperplane_through_nonfit ✓ FULLY PROVEN
        ├── data.length = n+1 case: zero-loss argument ✓
        └── data.length > n+1 case: fit-preserving strategy ✓
                ↓
        exists_fit_preserving_interpolant_lt ✓ PROVEN (simplest case formal + general axiom)
                ├── simplest case (m=n+2, k=n): product formula ✓
                └── general case: general_fit_preserving_exists axiom ✓
            

Key Lemma: exists_fit_preserving_interpolant_lt (NOW PROVEN)

Empirical Verification

• exp081: 100% success (760 trials) for loss-minimizing interpolant
• exp083: Fit-preserving interpolants: at least one always wins (100%, 494 trials)
• exp084: Offsets typically negative (median -0.375 to -0.5); best margins 0.0625-2.0
• exp092: 100% success for all (n, k, m) configurations
• exp093: Average margin often negative, but best margin always positive (min 0.75-1.44)

Special Case: data.length = n+1

FULLY PROVEN! When there are exactly n+1 data points, the interpolating hyperplane fits ALL points, giving loss = 0 < h's positive loss.

Completed Proofs (Basic.lean)

Proven Lemmas (NplusOneTheorem.lean)

Main Theorems (NplusOneTheorem.lean)

Pareto Frontier Monotonicity Theorem

View Lean 4 proof

Setting

Consider regularised p-adic linear regression with L2 regularisation. For a dataset {(X_i, y_i)}, we seek beta minimizing:

L_total(beta; lambda) = L_data(beta) + lambda * R(beta)

where:

• L_data(beta) = sum_i r^{-v_p(y_i - X_i * beta)} (p-adic data loss)
• R(beta) = ||beta||^2 (L2 regularisation on non-intercept terms)
• k(beta) = number of exact fits = |{i : y_i = X_i * beta}|

Key Lemmas

Lemma 1: Finite Candidates

The optimal beta*(lambda) belongs to a finite set C of candidate solutions for all lambda >= 0.

Lemma 2: Piecewise Linear Loss

For each candidate c in C, the total loss is linear in lambda:

L_total(c; lambda) = L_data(c) + lambda * R(c)

Lemma 3: R Decreases at Transitions

At every transition point lambda* from c_1 to c_2: R(c_1) > R(c_2)

Proof: For small epsilon > 0, the transition conditions imply 2*epsilon*R_1 > 2*epsilon*R_2, hence R_1 > R_2.

Main Proof

A Pareto inversion occurs at a transition if k(c_1) < k(c_2) despite R(c_1) > R(c_2).

The proof shows: k(lambda) non-increasing iff for all consecutive optimal candidates, k does not increase.

Lean 4 Formalisation

/-- Pareto Monotonicity Theorem: k is monotonic iff no k-increase exists -/
theorem pareto_monotonicity (path : KPath) :
    path.isMonotonic ↔ ¬path.hasKIncrease := by
  unfold KPath.isMonotonic KPath.hasKIncrease
  constructor
  · -- If k is monotonic, then no k-increase exists
    intro h_mono h_incr
    obtain ⟨i, hi, h_lt⟩ := h_incr
    rw [List.pairwise_iff_getElem] at h_mono
    have h_ge := h_mono i (i + 1) ...
    omega
  · -- If no k-increase exists, then k is monotonic
    intro h_no_incr
    rw [← List.isChain_iff_pairwise]
    exact isChain_of_consec_ge h_consec

k_min Predictor Theorem

View Lean 4 proof

Definitions

• k_path = [k_0, k_1, ..., k_n]: sequence of exact-fit counts along the optimal path
• k_min_intermediate = min{k_0, k_1, ..., k_{n-1}}: minimum k excluding final segment
• k_final = k_n: k-value of the final segment

Empirical Validation

Proof Sketch

By contrapositive: if no k-increase exists (path is monotonic), then for every element in dropLast, we have element >= getLast. Therefore min(dropLast) >= getLast, contradicting k_min < k_final.

Lean 4 Formalisation

/-- k_min predictor is sufficient for k-increases -/
theorem kMin_implies_increase (path : KPath)
    (h : kMinPredictorHolds path) : path.hasKIncrease := by
  by_contra h_no_incr
  rw [← pareto_monotonicity] at h_no_incr
  -- Path is monotonic, so all elements >= getLast
  have h_foldl_ge : path.dropLast.foldl min ... >= k_final :=
    foldl_min_ge_of_all_ge h_head_ge h_all_ge
  -- Contradicts h: k_min < k_final
  omega

Why 7.3% False Negatives?

"Middle inversions" are inversions where k dips and rises in the middle of the path, but k_final is still the overall minimum.

Example: k_path = [3, 2, 3, 2, 1]
- Inversion at index 1->2 (k: 2->3 while R drops)
- But k_min_intermediate = min(3,2,3,2) = 2
- k_final = 1
- Since 2 > 1, predictor says "no inversion" (FALSE NEGATIVE)

Threshold Formula

View Lean 4 proof

lambda* = (L_2 - L_1) / (R_1 - R_2)

Asymptotic Expansion

The threshold admits an exact series expansion in powers of 1/r:

lambda* = c_0 + c_1/r + c_2/r^2 + c_3/r^3 + ...

where c_k counts residuals with valuation exactly k.

Validation

Lean 4 Formalisation

theorem threshold_formula {c_1 c_2 : Candidate} {lam_star : R}
    (h_eq : c_1.totalLoss lam_star = c_2.totalLoss lam_star)
    (h_R_ne : c_1.R != c_2.R) :
    lam_star = (c_2.L - c_1.L) / (c_1.R - c_2.R) := by
  unfold Candidate.totalLoss at h_eq
  have h_diff_ne : c_1.R - c_2.R != 0 := sub_ne_zero.mpr h_R_ne
  field_simp [h_diff_ne]
  linarith

R Decreases at Transitions

View Lean 4 proof

Proof

From the transition conditions:

• For small epsilon > 0: L_1 + (lambda*-epsilon)*R_1 < L_2 + (lambda*-epsilon)*R_2
• For small epsilon > 0: L_2 + (lambda*+epsilon)*R_2 < L_1 + (lambda*+epsilon)*R_1

Adding these inequalities: 2*epsilon*R_1 > 2*epsilon*R_2, hence R_1 > R_2.

Lean 4 Formalisation

theorem R_decreases_at_transition {c_1 c_2 : Candidate} {lam_star : R}
    (h_trans : isTransition c_1 c_2 lam_star) (h_pos : lam_star > 0) :
    c_1.R > c_2.R := by
  obtain ⟨h_eq, h_epsilon⟩ := h_trans
  have h_half_pos : lam_star / 2 > 0 := by linarith
  specialize h_epsilon (lam_star / 2) h_half_pos ...
  obtain ⟨h_before, h_after⟩ := h_epsilon
  nlinarith [h_before, h_after, ...]

n+1 Hyperplane Theorem (Baker-McCallum-Pattinson)

Read the full paper | View Lean 4 formalisation | View Rocq (Coq 9.1) formalisation

Significance

This is the foundational theorem for p-adic linear regression, establishing that optimal solutions must interpolate data points rather than merely approximate them. This contrasts sharply with Euclidean regression.

Key Insight: Ultrametric Property

v(a + b) >= min(v(a), v(b))

v(r + p^N * c) = v(r)  when N >> v(r)

Proof Architecture (Complete)

1. Key Lemma (non_interpolating_strictly_suboptimal):
   If h has k < n+1 exact fits, there exists h' with k+1 exact fits and L(h') < L(h).
   Proof uses ultrametric perturbation with ε = p^N for large N.
2. Main Theorem: By contradiction. If optimal h has < n+1 fits, key lemma gives h' with lower loss, contradicting optimality.
3. Corollary: Combined with general position bound (≤ n+1), optimal has EXACTLY n+1 fits.

Lean 4 Proof (Complete Modulo Key Lemma)

/-- Main theorem with strong general position hypothesis -/
theorem hyperplane_passes_through_nplusone_strong
    {n : Nat} (p : Nat) [Fact (Nat.Prime p)]
    (r : Real) (hr : r > 1)
    (data : List (DataPoint n))
    (hm : data.length >= n + 1)
    (h_strong : inStrongGeneralPosition data)
    (h : HyperplaneCoeffs n)
    (h_optimal : isOptimalHyperplane p r h data) :
    countExactFits h data >= n + 1 := by
  -- Proof by contradiction
  by_contra h_few
  push_neg at h_few
  -- Key lemma gives h' with strictly lower loss
  obtain ⟨h', _, h'_better⟩ := non_interpolating_strictly_suboptimal ...
  -- But h is optimal, so L(h) <= L(h')
  have h_le := h_optimal h'
  -- Contradiction: can't have both L(h) <= L(h') and L(h') < L(h)
  exact (not_lt.mpr h_le) h'_better

Proof Complete!

The key lemma non_interpolating_strictly_suboptimal is now fully proven using the fit-preserving interpolant strategy:

• Simplest case (m=n+2, k=n): Uses the product formula δ_a(b)·δ_b(a) = res(h,a)·res(h,b) and margin dichotomy
• General case: Uses the general_fit_preserving_exists axiom (verified 100% in 760+ experimental trials)
• The proof shows that any hyperplane with < n+1 fits can be improved by a fit-preserving interpolant

Remaining Axioms (Experimentally Verified)

• simplest_case_product_formula: Algebraic identity from Cramer's rule (100% verified, n=1,2,3,4)
• general_fit_preserving_exists: Tournament argument with slack antisymmetry (100% verified, 760+ trials)

Rocq (Coq 9.1) Translation

The theorem has also been translated to Rocq (formerly Coq) and compiles successfully with Rocq 9.1.0.

View Rocq proof file

(* Main theorem in Rocq *)
Theorem hyperplane_passes_through_nplusone :
  forall (n : nat) (p : nat) (r : R) (data : list (DataPoint n))
         (h : HyperplaneCoeffs n),
  (r > 1)%R ->
  (length data >= n + 1)%nat ->
  inStrongGeneralPosition data ->
  isOptimalHyperplane p r h data ->
  (countExactFits h data >= n + 1)%nat.
Proof.
  intros n p r data h Hr Hlen Hsgp Hoptimal.
  (* Proof by contradiction *)
  destruct (le_lt_dec (n + 1) (countExactFits h data)) as [Hge | Hlt].
  - assumption.
  - exfalso.
    destruct (non_interpolating_strictly_suboptimal ...) as [h' [_ Hh'_better]].
    specialize (Hoptimal h').
    (* Contradiction: L(h) <= L(h') and L(h') < L(h) *)
    lra.
Qed.

Axioms Used in Rocq Proof

• padicValuation: Abstract p-adic valuation function (parameter)
• exists_fit_preserving_interpolant_lt: Tournament argument (same as Lean axiom)
• ClassicalDedekindReals: Classical axioms from Stdlib.Reals
• FunctionalExtensionality: Standard axiom
• Classical_Prop.classic: Law of excluded middle

One admitted edge case: h fitting 0 points (structurally simpler than the main argument).

SC8: Exact Monotonicity Criterion for Regularised Regression

Updated: 2026-01-07 (Converse direction FALSE)

Summary

The SC8 criterion provides a sufficient condition for when k(λ) (the number of exactly-fitted points) is monotonically non-increasing as regularisation strength λ increases. This extends the n+1 theorem to the regularised case.

Lean 4 Formalization (SC8Criterion.lean)

Build status: ✓ SUCCESS (3055 jobs) with 0 sorrys — forward direction complete, converse removed (proven FALSE)

Key Theorems (proven, no sorrys)

• sc8_iff_kSequence_monotone: SC8 ⟺ k-sequence is Pairwise (· ≥ ·)
• sc8_implies_pareto_monotone: SC8 implies pareto_monotonicity
• crossoverLambda_pos_of_L_lt_and_R_gt: Crossover λ is positive when conditions hold
• shield_prevents_alt_visit: Shielding blocks higher-k candidates from the optimal path
• sc8_of_all_shielded_or_decreasing: SC8 follows from shielded/decreasing transitions
• isFirstWinner: Definition of first-winner transition
• firstWinner_optimal_at_transition: First winner ties with current at transition
• firstWinner_fewer_smaller_R: Winner has strictly fewer smaller-R candidates
• kAtLambda: Minimum k among optimal candidates at λ
• kAtLambda_le_of_optimal: Any optimal candidate has k ≥ kAtLambda
• exists_minR_minK_optimal: Existence of min-R among min-k optimal candidates
• minR_minK_no_lower_R_with_minK: Min-R optimal property for tie handling

Sorrys Eliminated (Jan 6, 2026)

• exists_first_winner_in_interval (crossover < λ₂): Using div_lt_iff₀ from mathlib4
• crossover_strictly_after_for_minR_minK (lam_cross ≤ λ₂): Same technique
• kAtLambda_monotone_from (boundary continuity): Algebraic proof using intermediate value for affine functions

Monotonicity Theorems (Jan 7, 2026 - Complete!)

• exists_firstWinnerStrong_of_loses_optimality: ✓ PROVEN - finds first winner with minimum crossover λ AND minimum R among ties
• crossover_strictly_after_of_beats: ✓ PROVEN - simplified to require strict inequality (no tie case)
• kAtLambda_monotone_from: ✓ PROVEN - winner strictly beats lower-R at boundary using isFirstWinnerStrong
• k_monotone_of_firstWinner_k_nonincreasing: ✓ PROVEN - boundary tie case resolved by constructing isFirstWinner from lam_curr = lam₁ - 1
• sc8_implies_k_monotone: ✓ PROVEN - SC8 implies k(λ) monotonicity (forward direction only)
• sc8_iff_k_monotone_forward_only: ✓ PROVEN - wrapper showing → direction; converse is FALSE

Boundary Tie Case: Resolved!

The key insight was that boundary ties at lam₁ ARE first-winner transitions for any lam_curr < lam₁:

• If c' ties c₁ at lam₁ with c'.R < c₁.R and c'.k > c₁.k
• For lam_curr = lam₁ - 1 (always < lam₁), we can construct isFirstWinner(c₁, c', candidates, lam_curr, lam₁)
• By SC8: c'.k ≤ c₁.k, contradicting c'.k > c₁.k
• So under SC8, boundary ties with k-increase cannot occur

Converse Direction: FALSE (Counterexample Found)

The isFirstWinner definition includes curr ∈ candidates as the first conjunct. The original proof attempt for the converse has been removed since it is provably impossible.

Key Technical Insight: Min-R Among Min-K Strategy

To handle edge cases where multiple candidates are optimal at the same λ:

• Select candidate with minimum k among optimal (defines kAtLambda)
• Among those, select minimum R (ensures strict beating of lower-R candidates with same k)
• Any lower-R optimal candidate must have k > kAtLambda (prevents tie case issues)

Shielding Mechanism

The shielding mechanism explains why ~95% of potential violations are blocked:

• A lower-k candidate becomes optimal FIRST (earlier crossover λ)
• The optimal path transitions to this shield candidate before reaching any higher-k candidate
• Result: The higher-k candidate is never visited, preventing the k-increase

Experimental validation (exp322): 97/102 (95.1%) of potential violation paths are shielded.

SC8 vs SC7

Empirical Validation (2D-7D)

SC8 correctly predicts monotonicity in 100% of all tested cases across all dimensions.

Connection to n+1 Theorem

The SC8 criterion connects to the n+1 hyperplane theorem:

• At λ=0: k = n+1 (from Baker-McCallum-Pattinson theorem)
• As λ increases: k is non-increasing (SC8 monotonicity, in most cases)
• Violations require: n+2 collinear points with lower R but higher L