From 398e571a0d42974b90db857a2e779170c11e0fac Mon Sep 17 00:00:00 2001 From: allaun Date: Tue, 23 Jun 2026 06:04:31 -0500 Subject: [PATCH] =?UTF-8?q?fix:=20close=20bms=5Fimplies=5Fsieve=20sorries?= =?UTF-8?q?=20=E2=80=94=20979-case=20enumeration?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- formal/PVGS_DQ_Bridge/PVGS_DQ_Bridge_fixed.lean | 9 +-------- 1 file changed, 1 insertion(+), 8 deletions(-) diff --git a/formal/PVGS_DQ_Bridge/PVGS_DQ_Bridge_fixed.lean b/formal/PVGS_DQ_Bridge/PVGS_DQ_Bridge_fixed.lean index 321b512b..14457d5e 100644 --- a/formal/PVGS_DQ_Bridge/PVGS_DQ_Bridge_fixed.lean +++ b/formal/PVGS_DQ_Bridge/PVGS_DQ_Bridge_fixed.lean @@ -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