From 4e50dbba6de6e5ea3ba95d2dc54c05dd688a5bd2 Mon Sep 17 00:00:00 2001 From: allaun Date: Tue, 23 Jun 2026 05:59:53 -0500 Subject: [PATCH] =?UTF-8?q?fix:=20close=20bms=5Fimplies=5Fsieve=20sorry=20?= =?UTF-8?q?=E2=80=94=20979-case=20enumeration=20via=20native=5Fdecide?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The BMS region (x ∈ [2,90], m ∈ [3,13]) is finite. interval_cases x <;> interval_cases m <;> native_decide verifies all 979 cases computationally. Formula-first: the formula was verified by adversarial review before the proof was written. --- formal/PVGS_DQ_Bridge/section2_hermite_sieve.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/formal/PVGS_DQ_Bridge/section2_hermite_sieve.lean b/formal/PVGS_DQ_Bridge/section2_hermite_sieve.lean index 36358e00..dfe5ab1a 100644 --- a/formal/PVGS_DQ_Bridge/section2_hermite_sieve.lean +++ b/formal/PVGS_DQ_Bridge/section2_hermite_sieve.lean @@ -229,7 +229,7 @@ theorem bms_implies_sieve (x m : ℕ) (hx : x ≥ 2) (hm : m ≥ 3) -- For each pair, the diagonal H-KdF polynomial evaluates to zero by -- construction from the PVGS generating function. -- PROOF: finite enumeration via interval_cases + native_decide. - sorry + interval_cases x <;> interval_cases m <;> native_decide -- --------------------------------------------------------------------------- -- §2e SIEVE CONDITION DISCRIMINATES REPNIT COLLISIONS