stripPhase5Cert
plain-language theorem explainer
The declaration records the current unconditional zero-free region for the zeta function in the Recognition Science program by packaging the proven boundary result on Re(s) ≥ 1 with a trivial placeholder for the logarithmic strip bridge. Number theorists working on the RS-native zeta program would cite it as the honest Phase 5 state before any full strip theorem. The construction is a direct record definition that sets the bridge component to a constant true proposition.
Claim. Let $B$ be the boundary zero-free certificate asserting that the Riemann zeta function satisfies $B(s) : Re(s) ≥ 1 ⇒ ζ(s) ≠ 0$. The Phase 5 certificate is the structure whose boundary field equals $B$ and whose strip bridge field is the constant proposition true.
background
The module StripZeroFreeRegion implements Phase 5 of the RS-native zeta program. It records the proven Mathlib zero-free result on the line and half-plane Re(s) ≥ 1 while naming the genuine strip-zero-free theorem still required for RH-quality closure. The local setting treats the boundary certificate as already available and the logarithmic strip as an open bridge object. StripPhase5Cert is the structure that packages exactly one proven boundary certificate together with a named implication from the strip bridge to the desired zero-free conclusion. Upstream, the zeta abbreviation from ArithmeticFunctions supplies the arithmetic zeta function, while boundaryZeroFreeCert supplies the concrete boundary result on Re(s) ≥ 1.
proof idea
The definition is a one-line record constructor. It assigns the boundary field directly to the sibling boundaryZeroFreeCert and sets the strip_bridge field to the constant function that returns True for any input.
why it matters
This declaration marks the current unconditional zero-free region available to the RS zeta program and serves as the honest input state for any later bridge that would close the logarithmic strip. It aligns with the Recognition Science framework's zeta program in NumberTheory, which ultimately supports derivation of constants such as alpha inverse inside (137.030, 137.039) and the phi-ladder mass formula. The module doc explicitly states that the full strip theorem remains unproved and is packaged only as the next bridge object.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.