StripPhase5Cert
plain-language theorem explainer
StripPhase5Cert packages the proven boundary zero-free certificate for the Riemann zeta function on Re(s) ≥ 1 with a named open bridge to the logarithmic strip theorem. Number theorists extending the Recognition Science zeta program toward Riemann Hypothesis closure would cite this structure as the current unconditional foundation. The declaration is a direct structural definition that records the boundary fields and the bridge proposition without additional lemmas or computation.
Claim. A structure consisting of a boundary certificate asserting that the Riemann zeta function satisfies $riemannZeta(s) ≠ 0$ for all $s ∈ ℂ$ with $Re(s) ≥ 1$ (and likewise for $Re(s) > 1$), together with a proposition that holds whenever the logarithmic strip zero-free theorem (defined as the nonemptiness of LogZeroFreeStrip) is available.
background
The StripZeroFreeRegion module implements Phase 5 of the RS-native zeta program by recording the proven Mathlib zero-free results on the line and half-plane Re(s) ≥ 1 while naming the remaining strip theorem as an open bridge object. BoundaryZeroFreeCert is the structure whose fields are ge_one : ∀ s : ℂ, 1 ≤ s.re → riemannZeta s ≠ 0 and gt_one : ∀ s : ℂ, 1 < s.re → riemannZeta s ≠ 0. StripZeroFreeBridge is the definition Nonempty LogZeroFreeStrip that serves as the placeholder whose existence would yield the corresponding zero-free conclusion inside the strip.
proof idea
Direct structural definition that assembles the boundary certificate and the strip bridge proposition; no lemmas or tactics are applied.
why it matters
StripPhase5Cert supplies the current unconditional zero-free region to the RS zeta program and is instantiated by the downstream stripPhase5Cert construction that sets the boundary field to the Mathlib-derived certificate and the bridge to a trivial proposition. It marks the honest Phase 5 state before the logarithmic strip theorem is established, separating proven boundary results from the named bridge required for RH-quality closure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.