boundaryZeroFreeCert
plain-language theorem explainer
The certificate packages the established zero-free properties of the Riemann zeta function on the closed and open right half-planes into a reusable structure. Researchers extending the RS zeta program cite it to separate the unconditional boundary results from the conjectural logarithmic strip bridge. The definition is a direct record constructor that supplies the two half-plane fields from the corresponding standard lemmas.
Claim. The boundary zero-free certificate is the structure asserting that for all complex $s$ with real part at least 1, the Riemann zeta function at $s$ is nonzero, and likewise for real part strictly greater than 1.
background
This declaration belongs to the StripZeroFreeRegion module, Phase 5 of the RS-native zeta program. The module records the proven zero-free result on Re(s) >=1 from Mathlib while naming the genuine strip-zero-free theorem still required for RH-quality closure. It packages the strip theorem as the next bridge object rather than asserting it as proved.
proof idea
The definition is a direct record constructor for the BoundaryZeroFreeCert structure. It populates the ge_one field by applying the lemma for the closed half-plane and the gt_one field by applying the lemma for the open half-plane.
why it matters
This supplies the unconditional boundary zero-free region that anchors stripPhase5Cert and stripPhase7Cert. The downstream certificates state that the current unconditional zero-free region available to the RS zeta program is the boundary region Re >=1, with the logarithmic strip as the named bridge. It fills the proved part of Phase 5 before the strip bridge is invoked for deeper progress.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.