boundaryZeroFreeCert
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not establish zero-freeness for any point with real part less than 1.
- Does not prove the existence or constants of the logarithmic zero-free strip.
- Does not invoke or depend on the Riemann hypothesis.
- Does not address the critical strip zero-free bridge.
formal statement (Lean)
46def boundaryZeroFreeCert : BoundaryZeroFreeCert where
47 ge_one := fun _ hs => riemannZeta_ne_zero_re_ge_one hs
proof body
Definition body.
48 gt_one := fun _ hs => riemannZeta_ne_zero_re_gt_one hs
49
50/-! ## 2. The true strip target -/
51
52/-- A logarithmic zero-free strip with constants `c` and `T`.
53
54For `|Im(s)| ≥ T`, the region
55`Re(s) > 1 - c / log(|Im(s)|)` is zero-free. This is the classical
56Hadamard-de la Vallée-Poussin shape, stated as the exact bridge needed by
57the RS program. -/