fix(FixedPoint): revert abs_triangle to admit — q16Clamp sign analysis still blocked

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

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