ZeroFreeRegion
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not prove existence of any zero-free region for the zeta function.
- Does not derive the width function from the J-cost or defect budget.
- Does not recover the stronger Vinogradov-Korobov zero-free region.
- Does not connect the width directly to the prime-counting function.
formal statement (Lean)
43structure ZeroFreeRegion where
44 width : ℝ → ℝ -- width of zero-free strip as function of height
45 width_pos : ∀ t, 1 < t → 0 < width t
46 width_decreasing : ∀ t₁ t₂, 1 < t₁ → t₁ < t₂ → width t₂ ≤ width t₁
47