SilverSight/formal
allaun fec200205e feat(rrc): port ReceiptDensity, PolyFactorIdentity, EntropyCandidates and add Q16_16 roundtrip test
Ports three Research Stack RRC gates into formal/SilverSight/RRC/ using the existing CoreFormalism braid and Q16_16 surfaces.

Adds a Lean ↔ C ↔ Python Q16_16 roundtrip test:

  - c/q16_canonical.c: canonical saturating Q16_16 C library

  - exe/Q16_16Roundtrip.lean: Lake extern_lib linked executable

  - tests/test_q16_roundtrip.py: Python ↔ C harness (revived from quarantine)

Updates lakefile.lean with q16-roundtrip executable and extern_lib q16_canonical.

Build: lake build SilverSightRRC 3006 jobs, 0 errors; q16-roundtrip 5949 jobs, 0 errors
2026-06-21 10:39:18 -05:00
..
BindingSite Initial SilverSight: deterministic equation search via Fisher geometry 2026-06-21 18:02:05 +08:00
CoreFormalism feat(rrc): bare-minimum RRC refactor into SilverSight 2026-06-21 09:08:48 -05:00
PVGS_DQ_Bridge Fix: resolve sorrys across PVGS, UniversalEncoding, ChiralitySpace, QAOA 2026-06-21 05:35:53 -05:00
RRCLib feat(rrc): bare-minimum RRC refactor into SilverSight 2026-06-21 09:08:48 -05:00
SilverSight feat(rrc): port ReceiptDensity, PolyFactorIdentity, EntropyCandidates and add Q16_16 roundtrip test 2026-06-21 10:39:18 -05:00
UniversalEncoding Fix: resolve sorrys across PVGS, UniversalEncoding, ChiralitySpace, QAOA 2026-06-21 05:35:53 -05:00