feat(python): Q16 fraction module for exact-arithmetic mutation exploration

q16_fraction.py uses Python's Fraction for the entire compute path:
  - No float, no truncation during intermediate operations
  - Quantize to Lean-compatible Q16_16 raw int only at to_raw()
  - from_float is the sole float boundary (I/O entry point)

Provides Q16 subclass of Fraction with:
  - Exact q16_mul/q16_div/q16_add/q16_sub (no rounding)
  - to_raw: truncation toward zero (matches FixedPoint.lean:298)
  - to_raw_rounded: round-half-up (alternative output)

Designed for value-set mutation sweeps: explore the full rational
space, quantize only at the final output boundary.

python/q16_fraction.py

@@ -0,0 +1,193 @@
+"""
+Q16_16 Fraction Arithmetic — exact rational exploration (no float in compute path)
+
+Uses Python's Fraction for exact intermediate arithmetic.  Float only at the
+outer I/O boundary (JSON/sensor input).  All compute-path operations are
+pure Fraction arithmetic.
+
+Designed for mutation value-set exploration:
+  - No rounding, no truncation, no float error during sweeps
+  - Quantize to Q16_16 raw int only at the final output boundary
+
+Usage:
+    from q16_fraction import Q16, q16_mul, q16_div, to_raw
+
+    a = Q16.from_float(3.14)       # I/O boundary: float → Fraction
+    b = Q16(1, 2)                  # exact 0.5:  Fraction(1, 2) * 65536
+    c = q16_mul(a, b)              # exact 1.57: no truncation
+    raw = to_raw(c)                # → 102893  (int, Lean-compatible)
+
+Reference: FixedPoint.lean:298 — Lean truncates toward zero at each op.
+           This module TRUNCATES only at the final to_raw() boundary.
+           Exploration path uses exact arithmetic throughout.
+"""
+
+from __future__ import annotations
+
+import math
+import struct
+from fractions import Fraction
+from typing import Union
+
+# ── Constants ──────────────────────────────────────────────────────────────
+
+Q16_SCALE = 65536
+INT32_MAX = 2147483647
+INT32_MIN = -2147483648
+
+
+# ── Q16 type: a Fraction scaled by 65536 in value, but exact in operation ──
+
+class Q16(Fraction):
+    """Q16_16 value as an exact Fraction.
+
+    All arithmetic is exact rational (no float, no truncation).
+    The value is the real number it represents (not the raw int).
+
+    Construction:
+        Q16(num, den)       — Fraction(num, den)  (exact rational)
+        Q16.from_float(f)   — I/O boundary         (float → Fraction)
+        Q16.from_raw(i)     — int raw value        (raw → Fraction)
+
+    Conversion:
+        to_raw(q)           — Fraction → int       (output boundary)
+    """
+
+    __slots__ = ()
+
+    def __repr__(self) -> str:
+        return f"Q16({float(self):.6f})"
+
+    @classmethod
+    def from_float(cls, f: float) -> Q16:
+        """I/O boundary: float → Q16 via exact Fraction conversion.
+
+        Uses Fraction.from_float for exact binary→rational conversion,
+        then limits denominator to 65536 for Q16_16 compatibility.
+        Raises ValueError if f is NaN or infinite.
+        """
+        if math.isnan(f) or math.isinf(f):
+            raise ValueError(f"Non-finite float: {f}")
+        return cls(Fraction.from_float(f).limit_denominator(Q16_SCALE))
+
+    @classmethod
+    def from_raw(cls, raw: int) -> Q16:
+        """Convert a Q16_16 raw integer back to Q16.
+
+        The raw int represents value * 65536 with truncation.
+        This reverses the truncation: the Fraction captures the
+        exact value that the raw int encodes.
+        """
+        return cls(raw, Q16_SCALE)
+
+    def to_raw(self) -> int:
+        """Quantize to Q16_16 raw int (truncation toward zero).
+
+        Matches FixedPoint.lean:298 semantics at the output boundary.
+        Use this when emitting Lean-compatible values.
+        """
+        num = self.numerator * Q16_SCALE
+        den = self.denominator
+        if num >= 0:
+            return max(INT32_MIN, min(INT32_MAX, num // den))
+        else:
+            return max(INT32_MIN, min(INT32_MAX, -(-num // den)))
+
+    def to_raw_rounded(self) -> int:
+        """Quantize to Q16_16 raw int with round-half-up.
+
+        Alternative output boundary for cases where rounding is preferred
+        over truncation.  Not Lean-compatible by default.
+        """
+        return max(
+            INT32_MIN,
+            min(INT32_MAX, int(round(self.numerator * Q16_SCALE / self.denominator))),
+        )
+
+    def to_float(self) -> float:
+        """Debug/convenience: convert to float.
+
+        Not part of the compute path — use only for logging/display.
+        """
+        return float(self)
+
+
+# ── Arithmetic (exact Fraction, no float, no truncation) ──────────────────
+
+def q16_mul(a: Union[Q16, Fraction], b: Union[Q16, Fraction]) -> Q16:
+    """Exact Q16 multiplication.  No truncation, no float.
+
+    Contrast with Lean's truncating mul (FixedPoint.lean:298).
+    This path preserves full precision for mutation exploration.
+    """
+    return Q16(a * b)
+
+
+def q16_div(a: Union[Q16, Fraction], b: Union[Q16, Fraction]) -> Q16:
+    """Exact Q16 division.  No truncation, no float.
+
+    Raises ZeroDivisionError if b is zero.
+    """
+    if b == 0:
+        raise ZeroDivisionError("Q16 division by zero")
+    return Q16(a / b)
+
+
+def q16_add(a: Union[Q16, Fraction], b: Union[Q16, Fraction]) -> Q16:
+    return Q16(a + b)
+
+
+def q16_sub(a: Union[Q16, Fraction], b: Union[Q16, Fraction]) -> Q16:
+    return Q16(a - b)
+
+
+# ── Convenience constructors ───────────────────────────────────────────────
+
+def to_raw(a: Union[Q16, Fraction]) -> int:
+    """Convert any Q16/Fraction to Q16_16 raw int.
+
+    One-shot boundary function for the common case.
+    """
+    if isinstance(a, Fraction) and not isinstance(a, Q16):
+        a = Q16(a)
+    return a.to_raw()
+
+
+def from_raw(raw: int) -> Q16:
+    return Q16.from_raw(raw)
+
+
+def from_float(f: float) -> Q16:
+    return Q16.from_float(f)
+
+
+# ── Serialization ──────────────────────────────────────────────────────────
+
+def q16_from_bytes(raw_bytes: bytes) -> Q16:
+    return Q16.from_raw(struct.unpack("<i", raw_bytes)[0])
+
+
+def q16_to_bytes(a: Union[Q16, Fraction]) -> bytes:
+    return struct.pack("<i", to_raw(a))
+
+
+# ── Eval witnesses ────────────────────────────────────────────────────────
+
+if __name__ == "__main__":
+    # Mutation exploration: all arithmetic is exact
+    a = Q16.from_float(3.0)
+    b = Q16(1, 3)  # exact 1/3
+
+    c = q16_mul(a, b)  # exact 1.0
+    d = q16_div(a, b)  # exact 9.0
+    e = q16_add(c, d)  # exact 10.0
+
+    print(f"  3.0 × 1/3 = {c.to_float():.6f}  (raw={to_raw(c)})")
+    print(f"  3.0 ÷ 1/3 = {d.to_float():.6f}  (raw={to_raw(d)})")
+    print(f"  1.0 + 9.0 = {e.to_float():.6f}  (raw={to_raw(e)})")
+
+    # Compare with Lean-compatible truncation at boundary
+    a_raw = from_float(3.14)
+    b_raw = from_raw(102893)
+    print(f"  3.14 as Q16: {a_raw}  (raw={to_raw(a_raw)})")
+    print(f"  raw 102893  → {b_raw.to_float():.6f}")