classical_zfr_suffices
plain-language theorem explainer
Classical zero-free regions suffice for the Recognition Science chain. Researchers replacing the Riemann Hypothesis axiom with a proved theorem would cite this result to confirm that a defect-budget argument needs only the 1896 Hadamard-de la Vallée Poussin strip. The proof is a one-line term construction that instantiates the classical_zfr definition at c=1 to witness an inhabited ZeroFreeRegion structure.
Claim. There exists a positive real number $c$ such that the type of zero-free regions is inhabited, where a zero-free region is a structure consisting of a width function $w(t)$ satisfying $w(t)>0$ for all $t>1$ and $w(t_2)≤w(t_1)$ whenever $t_1<t_2$.
background
ZeroFreeRegion is the structure whose fields are a width function from height to strip width, a positivity proof for $t>1$, and a monotonicity proof. The sibling definition classical_zfr builds an explicit instance by setting width $t = c / log t$ and discharging the two field proofs by division and logarithm properties. The module setting is the defect-budget bridge: the J-cost functional on the recognition ledger forces a zero-free strip of the form $σ>1-c/log t$, which is weaker than the Vinogradov-Korobov region yet strong enough for the RS chain.
proof idea
The proof is a term-mode one-liner. It applies the tactic use to supply the witness pair (1, one_pos) and then invokes the constructor of the existential with the term classical_zfr 1 one_pos, which directly produces an element of ZeroFreeRegion.
why it matters
This theorem demonstrates that the classical Hadamard-de la Vallée Poussin zero-free region already meets the RS requirement, so the RH_conditional_axiom can be replaced by a proved statement. It sits immediately upstream of rh_axiom_replaceable and closes the gap between 1896 number theory and the forcing chain (T0-T8) without introducing new axioms. The module comment records the explicit comparison: the weaker classical strip is sufficient while the full RH remains an overkill conjecture.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.