IndisputableMonolith.NumberTheory.WeakZeroFreeRegion
This module sets up the weak zero-free region machinery for the RS-native zeta function as a precursor to stronger results. Number theorists extending the Recognition Science zeta program cite it when moving from the classical half-plane result to strip-level control. The module consists of definitions and certificates built directly on the RS time quantum, with no internal proofs.
claimThe module defines the weak zero-free region certificate asserting no zeros of the zeta function in a classical region near Re(s) = 1, together with the existence statement for such a certificate in RS-native units.
background
The module belongs to the NumberTheory section of the Recognition Science development and imports only Mathlib together with the Constants module. The upstream Constants module supplies the fundamental RS time quantum τ₀ = 1 tick, which fixes the native scale for all subsequent zeta-function statements. Sibling definitions in the same module introduce supporting objects such as ZeroFreeRegion, DefectBudget, and classical_zfr that encode the initial zero-free control before any strengthening.
proof idea
This is a definition module, no proofs. It organizes the weak zero-free region through a sequence of declarations (ZeroFreeRegion, classical_zfr, WeakZFRCert, weak_zfr_cert_exists) that import the RS time quantum and prepare the interface for the strip-level result.
why it matters in Recognition Science
The module supplies the weak zero-free region layer that is imported by StripZeroFreeRegion, the Phase 5 module of the RS-native zeta program. That downstream module records the proven Mathlib zero-free result on the half-plane Re(s) ≥ 1 and uses the weak certificate as its starting point before any further refinement.
scope and limits
- Does not prove any zero-free theorem inside the module itself.
- Does not supply explicit numerical constants or phi-ladder bounds.
- Does not address zeros off the critical line or the full Riemann hypothesis.
- Does not connect to mass formulas or the forcing chain T0-T8.