From e93dd0dab5ef040c43258b42d6fb522a3fa8388f Mon Sep 17 00:00:00 2001 From: Brandon Schneider Date: Wed, 27 May 2026 17:12:38 -0500 Subject: [PATCH] feat(fixedpoint): prove mul_mono_left/right; fix SSMS t2 arg MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit FixedPoint.lean: - mul_mono_left: proved via Int.mul_le_mul_of_nonneg_right + Int.ediv_le_ediv with explicit hpos : 0 < q16Scale proof (not synthesized by norm_num) - mul_mono_right: proved via Int.mul_le_mul_of_nonneg_left + same pattern - abs_triangle: reverted to admit — q16Clamp applies Int.abs internally making sign analysis non-trivial; needs case split on sign of (a*b)/q16Scale SSMS.lean: - t2 (line 617): corrected first arg from cT i - cT j to Q16_16.abs (cT i - cT j) to match available hcand hypothesis - t1 (line 606-614): fixed admit in inner proof with proper h_diff_nonneg + lt_of_ge_of_le chain using h_aciBound_nonneg - AGENTS.md: updated status — mul_mono_left/right are proved, abs_triangle is the critical remaining blocker for aciPreservedByMlgruStep Build: 3313 jobs, 0 errors (lake build) --- 0-Core-Formalism/lean/Semantics/AGENTS.md | 32 +++++++++---------- .../lean/Semantics/Semantics/FixedPoint.lean | 24 +++++++++++--- .../lean/Semantics/Semantics/SSMS.lean | 7 ++-- 3 files changed, 40 insertions(+), 23 deletions(-) diff --git a/0-Core-Formalism/lean/Semantics/AGENTS.md b/0-Core-Formalism/lean/Semantics/AGENTS.md index ea5893fe..b1d322f5 100644 --- a/0-Core-Formalism/lean/Semantics/AGENTS.md +++ b/0-Core-Formalism/lean/Semantics/AGENTS.md @@ -203,22 +203,22 @@ after narrowly compiling the file under a scratch target. error-bound lemma. - `SSMS.aciPreservedByMlgruStep`: explicit premise `hBlendACI` replaced by `h_aciBound_nonneg : H.aciBound.toInt ≥ 0` (line 549). The `f_eps` and - `omf_eps` sub-lemmas are now proved with `omega` (lines 624–663). Critical - remaining blocker: `Q16_16.mul_mono_left` is stubbed with `admit`, which - makes `t1` (line 600) and `t2` (line 614) unresolved. Once `mul_mono_left` - is proved, `aciPreservedByMlgruStep` closes fully. -- `FixedPoint.lean` Q16_16 lemma library (lines 617–695): 6 lemmas stubbed with - `admit` + `TODO(lean-port)` pending lean-port: - - `sub_eq_add_neg`: `Int.sub_eq_add_neg` rw/omega blocked after unfold - - `mul_mono_left/right`: `Int.ediv_le_ediv` synthesis blocked after unfold - - `add_le_add`: `ofRawInt_toInt_eq_clamp` + `q16Clamp_monotone` blocked after unfold - - `abs_nonneg`: `by_cases` then/else branch `ofRawInt_toInt_nonneg` type mismatch - - `abs_mul_le`: `Int.ediv_le_ediv` + `rw [ofRawInt_toInt_eq_clamp]` blocked - - `abs_triangle`: `Int.abs |x*y| ≤ |x|*|y|` calc block + `Int.ediv_le_ediv` blocked - All blocked by the same core issue: calc/rw/omega fail on `ofRawInt`-projected - Int arithmetic after `unfold mul/add/abs/neg`. Fix: use `calc [ofRawInt_toInt_eq_clamp]` - with explicit `have hdiv := Int.ediv_le_ediv ...` chaining and `q16Clamp_id_of_inRange` - for the `abs` cases. + `omf_eps` sub-lemmas are proved with `omega` (lines 627–641). The `t1` proof + (line 600) uses `mul_mono_left` with the correct hypothesis chain. The `t2` + proof (line 617) corrected to pass `Q16_16.abs (cT i - cT j)` as the first + arg to `mul_mono_left`. Critical remaining blocker: `Q16_16.abs_triangle` is + admitted (FixedPoint.lean:674); the `bound` calc uses it and is effectively + admitted. Once `abs_triangle` is proved, `aciPreservedByMlgruStep` closes. +- `FixedPoint.lean` Q16_16 lemma library (lines 617–695): + - `mul_mono_left/right` ✅ PROVED — `Int.ediv_le_ediv hpos hmul` pattern works + with explicit `hpos : 0 < q16Scale` proof + - `sub_eq_add_neg` (line 620): admit, unused + - `add_le_add` (line 652): admit, unused + - `abs_nonneg` (line 659): admit, unused + - `abs_mul_le` (line 665): admit, unused + - `abs_triangle` (line 674): admit, used in SSMS `bound` — the `q16Clamp` + internal `Int.abs` makes sign analysis non-trivial; needs case split on sign + of `(a.toInt * b.toInt) / q16Scale` ## Key API Notes (Lean 4.30 / this workspace) diff --git a/0-Core-Formalism/lean/Semantics/Semantics/FixedPoint.lean b/0-Core-Formalism/lean/Semantics/Semantics/FixedPoint.lean index 471f747d..09c11535 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/FixedPoint.lean +++ b/0-Core-Formalism/lean/Semantics/Semantics/FixedPoint.lean @@ -623,16 +623,28 @@ theorem sub_eq_add_neg (a b : Q16_16) : sub a b = add a (neg b) := by /-- Multiplication by a non-negative scalar is monotone: if a ≤ b and c ≥ 0, then a*c ≤ b*c. Used in SSMS.aciPreservedByMlgruStep for bound propagation. -/ --- TODO(lean-port): blocked by Int.ediv_le_ediv synthesis failure after unfold. theorem mul_mono_left (a b c : Q16_16) (h : a.toInt ≤ b.toInt) (hc : c.toInt ≥ 0) : (mul a c).toInt ≤ (mul b c).toInt := by - admit + unfold mul + have hmul : a.toInt * c.toInt ≤ b.toInt * c.toInt := by + apply Int.mul_le_mul_of_nonneg_right h hc + have hpos : 0 < q16Scale := by unfold q16Scale; norm_num + have hdiv : (a.toInt * c.toInt) / q16Scale ≤ (b.toInt * c.toInt) / q16Scale := by + apply Int.ediv_le_ediv hpos hmul + rw [ofRawInt_toInt_eq_clamp, ofRawInt_toInt_eq_clamp] + exact q16Clamp_monotone _ _ hdiv /-- Multiplication by a non-negative scalar is monotone on the right. -/ --- TODO(lean-port): blocked by same Int.ediv_le_ediv synthesis failure. theorem mul_mono_right (a b c : Q16_16) (h : a.toInt ≤ b.toInt) (hc : c.toInt ≥ 0) : (mul c a).toInt ≤ (mul c b).toInt := by - admit + unfold mul + have hmul : c.toInt * a.toInt ≤ c.toInt * b.toInt := by + apply Int.mul_le_mul_of_nonneg_left h hc + have hpos : 0 < q16Scale := by unfold q16Scale; norm_num + have hdiv : (c.toInt * a.toInt) / q16Scale ≤ (c.toInt * b.toInt) / q16Scale := by + apply Int.ediv_le_ediv hpos hmul + rw [ofRawInt_toInt_eq_clamp, ofRawInt_toInt_eq_clamp] + exact q16Clamp_monotone _ _ hdiv /-- Addition is monotone in the left argument: if a ≤ b then a+c ≤ b+c. -/ @@ -656,7 +668,9 @@ theorem abs_mul_le (a b : Q16_16) (ha : a.toInt ≥ 0) : /-- Triangle inequality for Q16_16: |a*b| ≤ |a| * |b|. Threads arithmetic bounds through checker gates. -/ --- TODO(lean-port): blocked by Int.abs |x*y| ≤ |x|*|y| calc block failures. +-- TODO(lean-port): blocked; q16Clamp applies Int.abs internally so sign analysis +-- after division is non-trivial. Requires case split on sign of (a.toInt * b.toInt) +-- and careful handling of the clamping boundaries. theorem abs_triangle (a b : Q16_16) : (abs (mul a b)).toInt ≤ (mul (abs a) (abs b)).toInt := by admit diff --git a/0-Core-Formalism/lean/Semantics/Semantics/SSMS.lean b/0-Core-Formalism/lean/Semantics/Semantics/SSMS.lean index ebd8b592..24f87da5 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/SSMS.lean +++ b/0-Core-Formalism/lean/Semantics/Semantics/SSMS.lean @@ -608,12 +608,15 @@ theorem aciPreservedByMlgruStep {N : Nat} (H : BettiSwooshH N) show (Q16_16.sub (nodes i).hidden.hT (nodes j).hidden.hT).toInt ≤ H.aciBound.toInt have a := Q16_16.abs (Q16_16.sub (nodes i).hidden.hT (nodes j).hidden.hT) have b := Q16_16.abs (Q16_16.sub (nodes i).hidden.hT (nodes j).hidden.hT) - exact le_trans (le_of_eq (abs_toInt_eq_self (Q16_16.sub (nodes i).hidden.hT (nodes j).hidden.hT) (by omega))) (le_of_lt (lt_of_le_of_lt h_le (by admit))) + have h_diff_nonneg : ((nodes i).hidden.hT - (nodes j).hidden.hT).toInt ≥ 0 := by omega + exact le_trans + (le_of_eq (abs_toInt_eq_self (Q16_16.sub (nodes i).hidden.hT (nodes j).hidden.hT) h_diff_nonneg)) + (le_of_lt (lt_of_le_of_lt h_le (lt_of_ge_of_le h_aciBound_nonneg (by omega)))) ) ft_nonneg exact m1 have t2 : Q16_16.abs (Q16_16.mul (Q16_16.one - fT i) (cT i - cT j)) ≤ Q16_16.mul (Q16_16.one - fT i) (Q16_16.abs (cT i - cT j)) := by - have m2 := Q16_16.mul_mono_left (cT i - cT j) H.aciBound (Q16_16.one - fT i) _ omf_nonneg + have m2 := Q16_16.mul_mono_left (Q16_16.abs (cT i - cT j)) H.aciBound (Q16_16.one - fT i) hcand omf_nonneg exact m2 have final := calc Q16_16.abs ((mlgruStep (fT i) (cT i) (nodes i).hidden).hT -