ZeroFreeRegion
plain-language theorem explainer
A zero-free region is specified by a positive decreasing width function for the zero-free strip as a function of imaginary height. Number theorists working within the Recognition Science framework to weaken the Riemann Hypothesis axiom would cite this definition. It is introduced directly as a structure with three fields for the width map and its positivity and decreasing properties.
Claim. A zero-free region consists of a map $w : (1,∞) → ℝ$ giving the width of the zero-free strip at height $t$, satisfying $w(t) > 0$ for all $t > 1$ and $w(t_2) ≤ w(t_1)$ whenever $1 < t_1 < t_2$.
background
The Weak Zero-Free Region module examines whether the full Riemann Hypothesis axiom can be eliminated in Recognition Science. It relies on the defect-budget bridge in which the J-cost functional on the recognition ledger constrains zeta-zero distribution, forcing a region of the form σ > 1 − c/log(t). This matches the classical Hadamard-de la Vallée Poussin zero-free region and is weaker than the Vinogradov-Korobov bound quoted in the module documentation.
proof idea
The declaration is a structure definition that packages the width function together with its positivity and monotonicity axioms. No lemmas or tactics are invoked; the three fields directly encode the required analytic properties of the strip width.
why it matters
This structure supplies the interface type for classical_zfr, which constructs an explicit instance with width(t) = c / log(t), and for rh_axiom_replaceable, which shows Nonempty ZeroFreeRegion. It thereby allows the RS chain requirements (zero-free region plus prime-counting and defect-budget conditions) to be met without assuming the full Riemann Hypothesis. The construction directly addresses the Q14 question of replacing the RH conditional axiom via the defect-budget mechanism.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.