From 68844c92c4ab39fa5f05dfd2ae32addfe1da77e0 Mon Sep 17 00:00:00 2001
From: allaun <allaun@researchstack.info>
Date: Tue, 7 Jul 2026 09:31:05 -0500
Subject: [PATCH] fix(python): q16_mul/q16_div pure integer toward-zero
 truncation
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Replaced float division + banker's rounding with pure integer
division truncating toward zero, matching FixedPoint.lean:298 and
FixedPoint.lean:302 exactly.

Added _div_toward_zero helper for Python's // vs Lean Int /
semantics mismatch.

Updated docstring: 'CANONICAL ROUNDING MODE' → 'ARITHMETIC MODE:
truncation toward zero matches Lean Int /'.

No float in compute paths. float_to_q16 (I/O boundary) unchanged.
---
 python/q16_canonical.py | 63 +++++++++++++++++++++--------------------
 1 file changed, 33 insertions(+), 30 deletions(-)

diff --git a/python/q16_canonical.py b/python/q16_canonical.py
index e1b04742..5be61116 100644
--- a/python/q16_canonical.py
+++ b/python/q16_canonical.py
@@ -1,15 +1,16 @@
 """Canonical Q16_16 fixed-point arithmetic.
 
-Single source of truth: CoreFormalism/Q16_16_Spec.lean
+Single source of truth: Core/SilverSight/FixedPoint.lean
 All operations MUST produce identical results to the Lean implementation.
 
 Q16_16 represents fixed-point numbers with 16 integer bits and 16 fractional bits.
 Range: [-32768.0, 32767.9999847412109375]
 Resolution: 1/65536 ≈ 0.0000152587890625
 
-CANONICAL ROUNDING MODE: round-half-up (banker's rounding)
-- Values exactly at half-LSB round to nearest even
-- All other values round to nearest
+ARITHMETIC MODE: truncation toward zero (matches Lean Int / division)
+- Lean mul (FixedPoint.lean:298):  (a.toInt * b.toInt) / q16Scale
+- Lean div (FixedPoint.lean:302):  (a.toInt * q16Scale) / b.toInt
+- No rounding: Q16_16 is a quotient type with floor semantics
 """
 
 import math
@@ -126,45 +127,47 @@ def q16_sub(a: int, b: int) -> int:
     return max(Q16_MIN_RAW, min(Q16_MAX_RAW, result))
 
 
-def q16_mul(a: int, b: int) -> int:
-    """Multiply two Q16_16 values with canonical rounding.
-    
-    result = canonical_round((a * b) / 65536)
-    
-    Uses 64-bit intermediate, then applies banker's rounding.
+def _div_toward_zero(num: int, den: int) -> int:
+    """Integer division truncating toward zero.
+
+    Python's // floors toward negative infinity.
+    Lean's Int / truncates toward zero.
+    This helper matches Lean's semantics.
     """
-    # Use Python's arbitrary precision integers (no overflow issue)
-    prod_64 = a * b
-    
-    # Divide by scale with banker's rounding
-    # prod_64 / 65536 with half-to-even
-    scaled = prod_64 / Q16_SCALE  # This is a float division for correct rounding
-    rounded = round(scaled)       # Banker's rounding
-    
-    return max(Q16_MIN_RAW, min(Q16_MAX_RAW, rounded))
+    if num >= 0:
+        return num // den
+    else:
+        return -(-num // den)
+
+
+def q16_mul(a: int, b: int) -> int:
+    """Multiply two Q16_16 values with truncation toward zero.
+
+    Matches FixedPoint.lean:298:  (a.toInt * b.toInt) / q16Scale
+
+    Uses Python's arbitrary precision integers (no overflow).
+    """
+    prod = a * b
+    return max(Q16_MIN_RAW, min(Q16_MAX_RAW, _div_toward_zero(prod, Q16_SCALE)))
 
 
 def q16_div(a: int, b: int) -> int:
-    """Divide two Q16_16 values with canonical rounding.
-    
-    result = canonical_round((a * 65536) / b)
-    
+    """Divide two Q16_16 values with truncation toward zero.
+
+    Matches FixedPoint.lean:302:  (a.toInt * q16Scale) / b.toInt
+
     Args:
         a: Dividend (Q16_16 raw value)
         b: Divisor (Q16_16 raw value), must not be zero
-    
+
     Raises:
         ZeroDivisionError: If b is zero
     """
     if b == 0:
         raise ZeroDivisionError("Q16_16 division by zero")
-    
-    # (a * 65536) / b with banker's rounding
+
     num = a * Q16_SCALE
-    scaled = num / b  # Float division for correct rounding
-    rounded = round(scaled)
-    
-    return max(Q16_MIN_RAW, min(Q16_MAX_RAW, rounded))
+    return max(Q16_MIN_RAW, min(Q16_MAX_RAW, _div_toward_zero(num, b)))
 
 
 # ============================================================