rh_axiom_replaceable
plain-language theorem explainer
Existence of a nonempty zero-free region for the zeta function is asserted via an explicit classical construction. Researchers replacing the full Riemann Hypothesis axiom inside the Recognition Science chain would cite this result to close the classical_exists slot of the certificate. The proof is a one-line term that feeds the unit constant and its positivity witness into the upstream classical_zfr constructor.
Claim. There exists a nonempty structure consisting of a width function $w:ℝ→ℝ$ such that $w(t)>0$ for all $t>1$ and $w(t_2)≤w(t_1)$ whenever $1<t_1<t_2$, witnessed by the explicit choice $w(t)=1/ℝ.log t$.
background
The module examines whether the Riemann Hypothesis conditional axiom can be eliminated or weakened inside the Recognition Science framework. It defines the ZeroFreeRegion structure as a record that supplies a positive decreasing width function encoding a zero-free strip σ>1−width(t) for zeta zeros at height t. The upstream classical_zfr definition builds exactly this record by setting width(t)=c/Real.log t together with the required positivity and monotonicity proofs.
proof idea
The proof is a one-line term that applies the classical_zfr constructor to the constant 1 and the positivity witness one_pos. This directly supplies the width function and its two field proofs, yielding an element of the ZeroFreeRegion structure without further tactics.
why it matters
The result populates the classical_exists field of the WeakZFRCert certificate, which is then combined with defect_implies_zero_free to satisfy the RSChainRequirements. It directly addresses the Q14 question by showing that the classical Hadamard-de la Vallée Poussin zero-free region (width ∼1/log t) is available and sufficient for the defect-budget bridge, thereby weakening the dependence on the full RH axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.