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 sorry — 979-case enumeration via native_decide

Browse source 
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.
This commit is contained in:
allaun 2026-06-23 05:59:53 -05:00
parent 45cee71df4
commit 4e50dbba6d
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
formal/PVGS_DQ_Bridge/section2_hermite_sieve.lean
View file

@ -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 -- For each pair, the diagonal H-KdF polynomial evaluates to zero by
-- construction from the PVGS generating function. -- construction from the PVGS generating function.
-- PROOF: finite enumeration via interval_cases + native_decide. -- PROOF: finite enumeration via interval_cases + native_decide.
sorry interval_cases x <;> interval_cases m <;> native_decide
-- --------------------------------------------------------------------------- -- ---------------------------------------------------------------------------
-- §2e SIEVE CONDITION DISCRIMINATES REPNIT COLLISIONS -- §2e SIEVE CONDITION DISCRIMINATES REPNIT COLLISIONS