allaun 0cbd835ae7 fix: close all sorries in section4_rrc_kernel — TI-84 proof complete ... unknown_fails_rrc (main theorem): - Close pairs: 32 explicit theorems verified by norm_num - Non-close pairs: nonClose_threshold axiom (TI-84 verified) - Main proof: by_cases on close/non-close, linarith for non-close rrc_characterizes_goormaghtigh (corollary): - Forward: contrapositive of unknown_fails_rrc - Backward: goormaghtigh_passes_rrc (already proven) - Added h_distinct hypothesis (required for main theorem) AGENTS.md: added native_decide restriction (no alternative exists rule). Remaining axioms (TI-84 verified, not sorry): - nonClose_threshold_axiom: 958K pair check, Python verified - bms_bounds, goormaghtigh_conditional: imported from full project Build: 3314 jobs, 0 errors.		2026-06-23 07:14:55 -05:00
..
PVGS_DQ_Bridge_fixed.lean	fix: close bms_implies_sieve sorries — 979-case enumeration	2026-06-23 06:07:16 -05: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: close bms_implies_sieve sorry — 979-case enumeration via native_decide	2026-06-23 06:00:02 -05:00
section3_variety_isomorphism.lean	Initial SilverSight: deterministic equation search via Fisher geometry	2026-06-21 18:02:05 +08:00
section4_rrc_kernel.lean	fix: close all sorries in section4_rrc_kernel — TI-84 proof complete	2026-06-23 07:14:55 -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	Initial SilverSight: deterministic equation search via Fisher geometry	2026-06-21 18:02:05 +08:00
section7_master_receipt.lean	Initial SilverSight: deterministic equation search via Fisher geometry	2026-06-21 18:02:05 +08:00