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
..
PVGS_DQ_Bridge_fixed.lean	fix: eliminate all 4 PVGS sorry proofs — sorry-free compilation	2026-07-01 22:47:19 +00:00
pvgs_receipt_hash.py	Initial SilverSight: deterministic equation search via Fisher geometry	2026-06-21 18:02:05 +08:00
section1_pvgs_params.lean	Initial SilverSight: deterministic equation search via Fisher geometry	2026-06-21 18:02:05 +08:00
section2_hermite_sieve.lean	fix: eliminate all 4 PVGS sorry proofs — sorry-free compilation	2026-07-01 22:47:19 +00:00
section3_variety_isomorphism.lean	fix: eliminate all 4 PVGS sorry proofs — sorry-free compilation	2026-07-01 22:47:19 +00:00
section4_rrc_kernel.lean	fix: Hkdf formula now uses (α*β)^(m+n+1) denominator; zero sorries	2026-06-23 11:42:16 -05:00
section5_quantum_sensing.lean	docs: fix documentation gaps + add pure math description	2026-06-23 05:21:58 -05:00
section6_effective_bounds.lean	chore(quality): native_decide migration, docs, and phi pipeline cleanup	2026-06-27 01:56:54 -05:00
section7_master_receipt.lean	Initial SilverSight: deterministic equation search via Fisher geometry	2026-06-21 18:02:05 +08:00