DefectBudget
plain-language theorem explainer
DefectBudget is the record structure that packages a positive total defect bounded above by 1 in normalized units. Researchers working on the Recognition Science zeta program cite it when they need to pass a J-cost sum into the defect-implies-zero-free implication. The declaration is a direct three-field structure with no computational content.
Claim. A defect budget consists of a real number $d$ together with proofs that $0 < d$ and $d ≤ 1$.
background
The WeakZeroFreeRegion module examines whether the defect-budget bridge can replace the full Riemann Hypothesis axiom. It recalls that the J-cost functional on the recognition ledger forces a zero-free region of the form σ > 1 − c/log(t), which is the classical Hadamard–de la Vallée Poussin region and is weaker than the Vinogradov–Korobov bound but sufficient for the RS chain. total_defect is the sum of individual J-costs over a configuration, while the normalized sequence from RunningMaxNormalization supplies the uniform bound of 1 used in the third field.
proof idea
This is a structure definition; the three fields are introduced directly with no lemmas or tactics applied.
why it matters
DefectBudget is referenced by defect_implies_zero_free (which extracts the constant c = total_defect), by RSChainRequirements (as one of its four components), and by WeakZFRCert (to witness that a defect budget yields the required zero-free region). It therefore supplies the concrete object that lets the RS chain operate with only the classical zero-free region rather than the full RH axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.