BoundaryZeroFreeCert
plain-language theorem explainer
BoundaryZeroFreeCert packages the established zero-free statements for the Riemann zeta function on the closed and open right half-planes into a single reusable structure. Number theorists working inside the Recognition Science zeta program cite it when assembling Phase 5 and Phase 7 certificates. The declaration is a plain structure that directly records two universal non-vanishing assertions already available from Mathlib.
Claim. Let $s$ be a complex number and let $Z(s)$ denote the Riemann zeta function. The boundary zero-free certificate is the structure whose fields assert $Z(s) neq 0$ whenever $operatorname{Re}(s) geq 1$ and $Z(s) neq 0$ whenever $operatorname{Re}(s) > 1$.
background
The module records the proven Mathlib zero-free result on the line and half-plane Re(s) >= 1 as part of Phase 5 of the RS-native zeta program. It distinguishes this completed boundary from the still-open strip-zero-free theorem required for RH-quality closure. The two fields of the structure are exactly the statements riemannZeta_ne_zero_re_ge_one and riemannZeta_ne_zero_re_gt_one, which supply the non-vanishing of the zeta function under the respective real-part inequalities.
proof idea
The declaration is a structure definition with no proof body. It simply declares the two fields, each a universal quantifier over complex s that packages the corresponding Mathlib non-vanishing lemma.
why it matters
The structure supplies the proved boundary component required by the Phase 5 certificate and the Phase 7 state record. It marks the completed part of the RS-native zeta analysis while leaving the critical-strip bridge as a named open target. In the broader framework the certificate anchors the number-theoretic input before any further Recognition Composition Law steps are applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.