feat(fixedpoint): prove mul_mono_left/right; fix SSMS t2 arg

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

@@ -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)
 

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

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 -