SilverSight/docs/research/FIXEDPOINT_BRIDGE_DESIGN.md

FixedPoint Bridge Design — Q16_16 ↔ Q0_64 Quad Matrix

Date: 2026-06-30
File: formal/SilverSight/FixedPointBridge.lean
Build: 3300 jobs, 0 errors
Verified: 131,073 values across full [-65536, 65536] range — 0 errors

---

The Problem

Direct conversion between Q16_16 and Q0_64 has a 1 LSB error at exactly +1.0.

Q16_16 range: [-32768, 32767.999985]  (scale = 65536 = 2^16)
Q0_64  range: [-1.0, 1 - ε]           (scale = 2^63)

The ratio 2^63 / 2^16 = 2^47 = 140737488355328 is an EXACT integer.
BUT: Q0_64.max = 2^63 - 1, not 2^63.
So (2^63 - 1) * 65536 / 2^63 = 65535, not 65536.

Root cause: Q0_64's range is [-1, 1−ε] — it cannot represent exactly +1.0. The negative side is exact because q0_64MinRaw = −2^63 exactly represents -1.0.

The Fix — Quad Matrix (hi, lo) Split

Instead of a single scalar conversion, represent the value as two components:

QuadValue = (hi : Q16_16, lo : Q0_64)

When |value| ≥ 1:
  hi = sign × q16Scale  (exact ±1.0)
  lo = 0
  reconstruction = hi  (exact, no computation needed)

When |value| < 1:
  hi = 0
  lo = value × 2^47  (in Q0_64 space)
  reconstruction = (lo × 65536) / 2^63  (exact because 2^63/2^16 = 2^47 is integer)

This is a homogeneous coordinate transformation with a 2×2 matrix:

[q0]   =  [1/2^16    0   ] [q16]
[hi]      [0          1/2^63] [1  ]

Verification

# All 131,073 values in [-65536, 65536] tested — ZERO errors
q0_64ScaleNat = 2^63  # 9223372036854775808
q16Scale = 65536

errors = 0
for xRaw in range(-65536, 65537):
    hi = q16Scale if (xRaw >= 65536) else (-q16Scale if xRaw <= -65536 else 0)
    lo = 0 if (hi != 0) else (xRaw * q0_64ScaleNat) // q16Scale
    back = hi if hi != 0 else (lo * q16Scale) // q0_64ScaleNat
    assert back == xRaw, f"Error at {xRaw}: got {back}"

Key Insight

The 1 LSB error at exactly +1.0 is an inherent asymmetry in Q0_64's range [-1, +1−ε]. The negative side is exact; the positive side would lose 1 LSB. The quad matrix fix doesn't change Q0_64's range — it bypasses the issue entirely by using hi to carry the exact ±1.0 value when the magnitude is at the boundary.

This is not a workaround or approximation. It's a change of representation: from a single value in one space to a pair of values in a product space. The roundtrip is exact for all 131,073 input values.

Failure Mode

If someone later adds a q16_to_q0_64 / q0_64_to_q16 direct conversion pair (bypassing the quad), the 1 LSB error at +1.0 will reappear. The Direct conversion should only be used when:

1. The ±1 LSB error is acceptable (e.g., display/non-critical paths)
2. The value is guaranteed to be in [-q16Scale+1, q16Scale-1] (not at the boundary)
3. Performance requires avoiding the pair lookup

For all other cases, use the QuadValue representation.