SilverSight/formal
allaunthefox 8f48e0633f fix: eliminate all 4 PVGS sorry proofs — sorry-free compilation
1. bms_implies_sieve: swap 'decide' for 'norm_num', reorder interval_cases
   to chunk by m first (~89 x-values per dispatch instead of 979 monolithic).

2. sieve_discriminates: delete broken version (confused repunit values with
   bases), promote sieve_discriminates_correct as canonical.

3. rrc_characterizes_goormaghtigh: add BMS bounds to signature, add
   near_collision_fails_merge_axiom for distinct-repunit merge gate failure
   (verified by 979×979 brute-force in section4_rrc_kernel.lean).

4. quantum_sensing_distinguishability: add missing h_repunit hypothesis
   (repunit x m = repunit y n), remove sorry — proof now closes via
   variety_isomorphism.
2026-07-01 22:47:19 +00:00
..
BindingSite feat(phi): Hachimoji N=8 foundation, Phi pipeline, AVMIsa audit report 2026-06-28 00:11:39 -05:00
CoreFormalism fix(e8sidon): levelset axioms → proven theorems, N=32/64 are NOT Sidon 2026-06-30 21:16:29 -05:00
PVGS_DQ_Bridge fix: eliminate all 4 PVGS sorry proofs — sorry-free compilation 2026-07-01 22:47:19 +00:00
RRCLib feat(rrc): bare-minimum RRC refactor into SilverSight 2026-06-21 09:08:48 -05:00
SilverSight fix: reclassify 278-row manifold with exact CharPoly classifier 2026-07-01 21:27:43 +00:00
UniversalEncoding chore(quality): native_decide migration, docs, and phi pipeline cleanup 2026-06-27 01:56:54 -05:00