WeakZFRCert
plain-language theorem explainer
The weak zero-free region certificate records a classical nonempty zero-free region together with the implication that every defect budget yields a positive width bound of the form c over log t. Number theorists working on the Recognition Science zeta program would cite this structure when weakening the Riemann Hypothesis axiom to a defect-derived bound. The definition assembles the two fields directly as a record type with no computational content.
Claim. A weak zero-free region certificate consists of a nonempty collection of zero-free regions (each given by a positive decreasing width function for heights $t>1$) together with the property that every defect budget (a positive real bounded by 1) implies the existence of a constant $c>0$ such that the width exceeds $c/Real.log t$ for all $t>1$.
background
The module addresses Q14: whether the defect-budget bridge from the J-cost functional on the recognition ledger can replace the full Riemann Hypothesis axiom. It shows that a normalized positive defect budget forces a zero-free region of Hadamard-de la Vallée Poussin type, namely the strip where the real part exceeds 1 minus c over log t, which suffices for the RS chain but is weaker than the Vinogradov-Korobov bound.
proof idea
The structure is defined directly by its two fields with no lemmas or tactics applied. The first field asserts classical existence of a zero-free region; the second asserts that every defect budget produces a positive constant c satisfying the width lower bound for t greater than 1.
why it matters
This definition supplies the certificate type constructed by the downstream theorem weak_zfr_cert_exists, which instantiates it from rh_axiom_replaceable and defect_implies_zero_free. It fills the Q14 slot in the module by packaging the minimal zero-free region needed for the RS chain, advancing the question of whether the full Riemann Hypothesis axiom can be eliminated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.