weak_zfr_cert_exists
plain-language theorem explainer
The theorem establishes existence of a WeakZFRCert that packages a classical zero-free region for the zeta function together with the implication that any defect budget forces a positive c satisfying c over log t greater than zero for t greater than one. Number theorists working on the Recognition Science zeta program would cite it to replace the full Riemann Hypothesis axiom with the weaker defect-budget condition. The proof is a direct term construction that supplies the two fields of the certificate from upstream results.
Claim. There exists a certificate structure consisting of a nonempty classical zero-free region for the Riemann zeta function together with the property that every defect budget yields some positive real constant c such that c divided by the natural logarithm of t is positive for all real t greater than 1.
background
The Weak Zero-Free Region module examines whether the Recognition Science zeta program can avoid the full Riemann Hypothesis axiom. It relies on the defect-budget bridge in which the J-cost functional on the recognition ledger constrains the distribution of zeta zeros. The module states that the RS chain requires only the classical Hadamard-de la Vallée Poussin zero-free region of the form sigma greater than 1 minus c over log t, which is weaker than the Vinogradov-Korobov region but sufficient for the chain. WeakZFRCert is the structure that records both the classical existence and the defect implication. Upstream, defect_implies_zero_free proves that any DefectBudget supplies the required c via its total_defect, while rh_axiom_replaceable supplies the classical nonempty ZeroFreeRegion.
proof idea
The proof is a one-line term-mode construction of the WeakZFRCert structure. It populates the classical_exists field directly with the result of rh_axiom_replaceable and the defect_gives_zfr field directly with the result of defect_implies_zero_free.
why it matters
This theorem shows that the defect-budget condition suffices to obtain the zero-free region needed by the RS chain, thereby making the full RH axiom replaceable. It closes the local argument in the Weak Zero-Free Region module and supports downstream requirements for the Recognition Science mass formula and constants. The module explicitly notes that the classical Hadamard-de la Vallée Poussin region meets the RS needs, removing the need for a stronger conditional axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.