defect_implies_zero_free
plain-language theorem explainer
A positive defect budget forces a positive constant c such that c / log t > 0 for all t > 1. Number theorists replacing the full Riemann Hypothesis axiom in the RS chain would cite this result. The proof is a direct term-mode construction that instantiates c with the budget's total defect and checks positivity via the supplied defect positivity and the positivity of the logarithm.
Claim. Let $db$ be a DefectBudget structure whose total defect $d$ satisfies $d > 0$. Then there exists $c > 0$ such that for every real $t > 1$, $c / (log t) > 0$.
background
DefectBudget is the structure carrying a normalized total defect $d$ with $0 < d ≤ 1$. The module WeakZeroFreeRegion asks whether the RS zeta program can avoid the full Riemann Hypothesis by using only the classical Hadamard-de la Vallée Poussin zero-free region of the form σ > 1 − c / log t. The defect-budget bridge supplies the required positivity of c directly from the recognition ledger. Upstream, total_defect is defined as the sum of individual J-costs over a configuration, and the various Chain structures supply the recognition steps that generate the defect.
proof idea
Term-mode proof. The tactic 'use db.total_defect' supplies the witness c. The subsequent exact constructs the pair consisting of the defect positivity hypothesis and the lambda that applies div_pos to that hypothesis together with Real.log_pos on the assumption t > 1.
why it matters
This theorem supplies the defect_gives_zfr field of WeakZFRCert, which is assembled in weak_zfr_cert_exists. It therefore closes the sufficiency argument that the RS chain requires only the classical zero-free region rather than the full RH axiom. The module doc states that the stronger Vinogradov-Korobov region is available classically but unnecessary for the RS number-theory chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.