birch-swinnerton-dyer-143a1 — BSD for Curve 143a1 — Hasse Infinite HONEST + Bost Bound S₄ •Formally Verified Analytic Rank 1 = Algebraic Rank 1 Lean 4.12
-
Updated
Aug 15, 2026 - Lean
birch-swinnerton-dyer-143a1 — BSD for Curve 143a1 — Hasse Infinite HONEST + Bost Bound S₄ •Formally Verified Analytic Rank 1 = Algebraic Rank 1 Lean 4.12
Route C of 4 — Act III Growth. RH via contradiction: |ζ|≤C(log t)² false via Littlewood 1924 Ω exp(c√(log t/log log t)). Zero repulsion c1=0.209>0.2 β>0.9 closed at p5 → S₄={2,3,19,191} C=11.422>2√13 → GRH → H₄ 12/11 → RH. Lean 4.12 0 sorry. Opera Numerorum with A, B, D 35 brothers desert.
Route B of 4 — Act II Descent. RH via spectral gap X₀(143) λ₁≥975/4096 Kim-Sarnak → Selberg = Bost-Connes C(S₄)=11.422>2√13 → GRH → H₄ 12/11 → RH. 35pp BC6 20450 bytes 0 sorry. Opera Numerorum with A ω²=48/13>0, C Littlewood Ω, D 35 brothers jitter ||p·α₀||<1/p → R=1/2. doi:10.5281/zenodo.21303976
Keystone CLOSED — 143*13=1859 | S14=14 q5=226 q6=165849 cf_bound=82829 | C(S4)=11.422>2√13 h=10 — P5_BSD_RH_closure_CLOSED — Lean 4.12 0 sorry — BSD 143a1 + RH
Bost-Connes spectral analysis for X₀(143): Gate M1 BC6 Weil bound closed via C(S₄)=11.422>2√13 — 16 bricks 0 sorry — Lean 4
Lakatosianisches Forschungsjournal zur Riemannschen Hypothese — Objekt X: spektrale, nichtkommutative und arithmetische Zugaenge. 324 Dokumente, Stand NEU-221d.
Add a description, image, and links to the bost-connes topic page so that developers can more easily learn about it.
To associate your repository with the bost-connes topic, visit your repo's landing page and select "manage topics."