From 31210774cb5c9de1ee25981ec11cbf7392ef9eac Mon Sep 17 00:00:00 2001 From: Brandon Schneider Date: Wed, 27 May 2026 17:15:52 -0500 Subject: [PATCH] =?UTF-8?q?fix(FixedPoint):=20revert=20abs=5Ftriangle=20to?= =?UTF-8?q?=20admit=20=E2=80=94=20q16Clamp=20sign=20analysis=20still=20blo?= =?UTF-8?q?cked?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit abs_triangle: reverted to admit. The q16Clamp applies Int.abs internally, making sign analysis after division non-trivial. Attempted proofs using Int.sign, Int.sign_mul_abs, Int.ediv_neg_pos_of_neg, Int.mul_ediv_le all failed (missing theorems in this Mathlib version). Key theorem: mul_mono_left and mul_mono_right are proved and working. Build: 3313 jobs, 0 errors (lake build) --- 0-Core-Formalism/lean/Semantics/Semantics/FixedPoint.lean | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/0-Core-Formalism/lean/Semantics/Semantics/FixedPoint.lean b/0-Core-Formalism/lean/Semantics/Semantics/FixedPoint.lean index 09c11535..6190fb00 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/FixedPoint.lean +++ b/0-Core-Formalism/lean/Semantics/Semantics/FixedPoint.lean @@ -668,9 +668,10 @@ 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; 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. +-- TODO(lean-port): blocked; q16Clamp applies Int.abs internally making sign analysis +-- non-trivial after division. The key insight: q16Clamp(x) ≤ q16Clamp(-x) always holds +-- (when x<0, LHS is negative and RHS is positive). Needs case split on sign of +-- (a.toInt * b.toInt) / q16Scale 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