From 09913f97911b924d7f8c312dfcf7589c4809c645 Mon Sep 17 00:00:00 2001
From: Brandon Schneider <ceo@sovereign-stack.local>
Date: Wed, 27 May 2026 16:35:53 -0500
Subject: [PATCH] chore(lean): stub 6 Q16_16 arithmetic lemmas with
 TODO(lean-port)

FixedPoint.lean: add stubs for abs_triangle, sub_eq_add_neg,
mul_mono_left/right, add_le_add, abs_nonneg, abs_mul_le.
All blocked by the same core issue: calc/rw/omega fail on
ofRawInt-projected Int arithmetic after unfold mul/add/abs/neg.
The pattern that works in PistSimulation (unfold + Int.ediv_le_ediv
+ ofRawInt_toInt_eq_clamp + q16Clamp_monotone) fails here
because the goal structures differ.

Known-working pattern to finalize:
  1. unfold the Q16_16 op
  2. have h2 := raw Int inequality (Int.mul_le_mul_of_nonneg_*)
  3. have hdiv := Int.ediv_le_ediv (by norm_num) h2
  4. rw [ofRawInt_toInt_eq_clamp, ofRawInt_toInt_eq_clamp]
  5. exact q16Clamp_monotone _ _ hdiv

AGENTS.md: document 6 new TODO(lean-port) items in Pending Proof Work.

Build: 3313 jobs, 0 errors (lake build Compiler)
---
 0-Core-Formalism/lean/Semantics/AGENTS.md     | 12 +++++
 .../lean/Semantics/Semantics/FixedPoint.lean  | 47 +++++++++++++++++++
 2 files changed, 59 insertions(+)

diff --git a/0-Core-Formalism/lean/Semantics/AGENTS.md b/0-Core-Formalism/lean/Semantics/AGENTS.md
index 364bb4f1..f3fe85f3 100644
--- a/0-Core-Formalism/lean/Semantics/AGENTS.md
+++ b/0-Core-Formalism/lean/Semantics/AGENTS.md
@@ -204,6 +204,18 @@ after narrowly compiling the file under a scratch target.
 - `SSMS.aciPreservedByMlgruStep`: former sorry replaced by explicit premise
   `hBlendACI` (lines 545–548). Remaining: `TODO(lean-port)` discharge from Q16_16
   triangle inequality, multiplication monotonicity, and saturation associativity.
+- `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.
 
 ## 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 93ecbf73..471f747d 100644
--- a/0-Core-Formalism/lean/Semantics/Semantics/FixedPoint.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/FixedPoint.lean
@@ -614,6 +614,53 @@ theorem epsilon_add_pos {r : Q16_16} (hr : r.toInt ≥ 0) :
       (by norm_num [q16MinRaw]) (by norm_num [q16MaxRaw])
   omega
 
+/-- Subtraction is addition of the negation: a - b = a + (-b). -/
+-- TODO(lean-port): prove using Int.sub_eq_add_neg; tactic chain blocked by
+--   rw/omega failures on Int arithmetic equality after unfold.
+theorem sub_eq_add_neg (a b : Q16_16) : sub a b = add a (neg b) := by
+  admit
+
+/-- 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
+
+/-- 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
+
+/-- Addition is monotone in the left argument:
+    if a ≤ b then a+c ≤ b+c. -/
+-- TODO(lean-port): blocked by q16Clamp_monotone call after ofRawInt_toInt_eq_clamp.
+theorem add_le_add (a b c : Q16_16) (h : a.toInt ≤ b.toInt) :
+    (add a c).toInt ≤ (add b c).toInt := by
+  admit
+
+/-- Absolute value of any Q16_16 value is non-negative. -/
+-- TODO(lean-port): blocked by Int.sub_eq_add_neg rw failure; type mismatch in
+--   ofRawInt_toInt_nonneg call in by_cases then-branch.
+theorem abs_nonneg (a : Q16_16) : (abs a).toInt ≥ 0 := by
+  admit
+
+/-- For non-negative a, |a*b| ≤ a*|b|.
+    Key lemma for bound propagation in SSMS.aciPreservedByMlgruStep. -/
+-- TODO(lean-port): blocked by Int.ediv_le_ediv synthesis and rw failures.
+theorem abs_mul_le (a b : Q16_16) (ha : a.toInt ≥ 0) :
+    (abs (mul a b)).toInt ≤ (mul a (abs b)).toInt := by
+  admit
+
+/-- 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.
+theorem abs_triangle (a b : Q16_16) :
+    (abs (mul a b)).toInt ≤ (mul (abs a) (abs b)).toInt := by
+  admit
+
 end Q16_16
 
 -- ═══════════════════════════════════════════════════════════════════════════