DefectBudget
plain-language theorem explainer
DefectBudget packages a real number D with 0 < D ≤ 1 as the total J-cost sum over a configuration. Number theorists replacing the full Riemann Hypothesis axiom with the RS defect-budget argument cite it as the input that forces a weak zero-free region. The declaration is a direct structure definition with three fields enforcing positivity and the unit bound.
Claim. A real number $D$ forms a defect budget when $0 < D$ and $D ≤ 1$, where $D$ equals the sum of individual J-costs over the entries of a configuration.
background
The Weak Zero-Free Region module examines whether the defect-budget bridge can eliminate the full RH axiom. The J-cost functional on the recognition ledger constrains zeta zero distribution, and the required zero-free region is the classical Hadamard-de la Vallée Poussin form σ > 1 − c/log(t). Total defect is defined as the sum of individual J-costs over a finite configuration and is non-negative. The normalized sequence from the Navier-Stokes module supplies a bounded auxiliary object used in related constructions.
proof idea
This is a structure definition. It introduces the type by listing the three fields that record the defect value together with its positivity and upper bound constraints.
why it matters
DefectBudget is the hypothesis passed to defect_implies_zero_free, which extracts the positive constant c to obtain the weak zero-free region. It also appears inside RSChainRequirements and WeakZFRCert. The structure therefore supplies the defect-budget step that lets the RS zeta program rely on the Hadamard-de la Vallée Poussin region rather than the stronger Vinogradov-Korobov bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.