From d709136e17f70657c770eb2dd6c84672ddca3609 Mon Sep 17 00:00:00 2001 From: allaun Date: Tue, 7 Jul 2026 09:33:27 -0500 Subject: [PATCH] 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 | 193 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 193 insertions(+) create mode 100644 python/q16_fraction.py diff --git a/python/q16_fraction.py b/python/q16_fraction.py new file mode 100644 index 00000000..73368a63 --- /dev/null +++ b/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(" bytes: + return struct.pack("