stripPhase7Cert
plain-language theorem explainer
stripPhase7Cert assembles the honest phase-7 snapshot of zero-free progress for the Riemann zeta function. It certifies the boundary region Re(s) >= 1 via Mathlib non-vanishing lemmas, names the log-strip and critical-strip bridges as open targets, and records that the critical-strip bridge follows from the Riemann hypothesis. The definition is a direct record that pulls the boundary certificate and the known RH implication without introducing new proofs.
Claim. The phase-7 certificate consists of the boundary zero-free certificate (asserting non-vanishing for Re(s) >= 1), the named targets log-strip bridge and critical-strip bridge, and the implication that the Riemann hypothesis yields the critical-strip zero-free bridge.
background
The StripZeroFreeRegion module records proven zero-free results on Re(s) >= 1 while naming the remaining strip theorem required for RH-quality closure. It does not assert the full strip result as proved; instead it packages the dependency as a bridge object. BoundaryZeroFreeCert is the structure that holds the two Mathlib facts riemannZeta_ne_zero_re_ge_one and riemannZeta_ne_zero_re_gt_one. The companion theorem criticalStripZeroFreeBridge_of_riemannHypothesis shows that RiemannHypothesis directly produces CriticalStripZeroFreeBridge.
proof idea
The definition builds the StripPhase7Cert instance by assigning boundary to the already-constructed boundaryZeroFreeCert, setting the two bridge-named fields to trivial, and populating the RH-implication field with the theorem criticalStripZeroFreeBridge_of_riemannHypothesis.
why it matters
This declaration supplies the current honest state for phase 7 of the RS-native zeta program, linking the established boundary non-vanishing to the Riemann hypothesis as the remaining gate for the critical strip. It documents the precise dependency that must be discharged before the strip result can be used downstream in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.