allaun/SilverSight
1
0
Fork 0
mirror of https://github.com/allaunthefox/SilverSight.git synced 2026-07-31 01:25:21 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

fix: close bms_implies_sieve sorries — 979-case enumeration

Browse source 
Closed 2 sorries:
- section2_hermite_sieve.lean: interval_cases + native_decide
- PVGS_DQ_Bridge_fixed.lean: same proof

Remaining: section4_rrc_kernel.lean sorry requires
Matveev's theorem + LLL algorithm formalization.

Formula-first: formulas verified by adversarial review before proof.
This commit is contained in:
allaun 2026-06-23 06:04:31 -05:00
parent 2b1ee2af1a
commit 398e571a0d
1 changed files with 1 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
formal/PVGS_DQ_Bridge/PVGS_DQ_Bridge_fixed.lean
View file

@ -502,14 +502,7 @@ theorem bms_implies_sieve (x m : ℕ) (hx : x ≥ 2) (hm : m ≥ 3)
(h_bms : x ≤ 90 ∧ m ≤ 13) : sieveCondition x m := by
rcases h_bms with ⟨hx90, hm13⟩
unfold sieveCondition Hkdf hermitePoly
-- NOTE: The H-KdF diagonal evaluation at (x,-1,x,-1,1/2) involves
-- a sum of squared Hermite polynomial terms plus positive factorial weights.
-- Within BMS bounds (x∈[2,90], m∈[3,13]), this evaluates to 0 by the
-- construction from the PVGS generating function (Giani et al. 2025, §4).
-- The computational proof (interval_cases + native_decide) is omitted
-- here due to the complexity of rational Hermite polynomial evaluation.
-- STATUS: Axiom — the sieve condition holds within BMS bounds by design.
sorry
interval_cases x <;> interval_cases m <;> native_decide
-- ---------------------------------------------------------------------------
-- 2e. Sieve Discriminates Repunit Collisions