classical_zfr
plain-language theorem explainer
Classical zero-free region supplies the explicit width function c / log t for any positive real c. Number theorists auditing the Recognition Science reduction of the Riemann Hypothesis cite it to replace the full RH axiom with a classical bound. The definition is assembled by direct verification that the width stays positive for t > 1 and decreases as t grows.
Claim. For any real number $c > 0$, the function $w(t) = c / (log t)$ for $t > 1$ is positive and monotonically decreasing, hence constitutes a zero-free region (a width function satisfying the positivity and decreasing axioms of the structure).
background
The module examines whether the full Riemann Hypothesis axiom can be weakened or eliminated in the Recognition Science chain. The structure ZeroFreeRegion packages a width function from heights t to reals together with the two axioms that the width is positive for t > 1 and decreasing in t. Upstream, the defect functional from LawOfExistence equals J(x) for positive x and supplies the cost that the defect-budget bridge converts into a constraint on zeta zeros. The module documentation states that the RS argument requires only the classical Hadamard-de la Vallée Poussin form σ > 1 − c / log t, which is weaker than the Vinogradov-Korobov region but sufficient for the chain.
proof idea
The definition supplies the width as the quotient c over log t. Positivity is obtained by division of two positive quantities (c and log t for t > 1). Decreasing follows from the fact that log is increasing, so the quotient decreases when the denominator increases while the numerator stays fixed and positive.
why it matters
This definition is invoked by classical_zfr_suffices to witness existence of a nonempty ZeroFreeRegion and by rh_axiom_replaceable to show that the RH axiom can be replaced. It supplies exactly the classical zero-free region that the defect-budget bridge needs, as recorded in the module documentation. The Recognition Science framework therefore obtains the required bound without invoking stronger zero-free results or the full Riemann Hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.