zeroFreeCriterion_of_honestPhaseChargeZeroBridge
Researchers pursuing the pure analytic route to the Riemann hypothesis cite this definition to obtain a complete ZeroFreeCriterion from any direct honest-phase charge-zero bridge. It assembles the criterion by delegating its four fields to carrier derivative bounds, nonvanishing results, the honest argument principle, and the dedicated charge-zero discharge theorem. The construction is a direct definition that requires no additional proof steps.
claimGiven a direct charge-zero bridge $hb$ for honest zeta phase data, the zero-free criterion is the structure with logarithmic derivative bounded on the strip by the positive carrier derivative bound, carrier nonvanishing on the strip, honest phase family supplied by the argument principle, and charge-zero property discharged by the dedicated theorem applied to $hb$.
background
The Analytic Trace module builds an axiom-free interface for the Riemann hypothesis. It replaces earlier axioms with proved results including contour winding from holomorphy and the floor-coverage equivalence to charge zero. Two routes to RH remain: the ontology route via an external bridge hypothesis, and the pure analytic route that targets a ZeroFreeCriterion from honest phase data.
proof idea
This is a direct definition that constructs the ZeroFreeCriterion by explicit field assignment. It sets the log-derivative bound to the lambda expression using carrierDerivBound_pos, the nonvanishing field to the lambda using carrier_nonvanishing, the phase family to honest_argument_principle_phase_family, and the charge-zero field to the application of charge_zero_of_honest_phase_of_chargeZeroBridge to the input bridge.
why it matters in Recognition Science
This declaration supplies the ZeroFreeCriterion required by direct_rh_from_honestPhaseChargeZeroBridge, which then concludes that no nonzero-charge sensor exists and thereby proves the analytic RH core. It supports the pure analytic route in the module and connects honest phase data directly to the charge-zero conclusion. It participates in the elimination of former axioms within the analytic trace infrastructure.
scope and limits
- Does not prove existence of any honest phase charge zero bridge.
- Does not derive the Riemann hypothesis without an additional bridge hypothesis.
- Does not address the ontology route via external bridge assumptions.
- Does not bound total annular cost, only the charge component.
- Does not apply outside witnessed defect sensors in the analytic trace setting.
formal statement (Lean)
225noncomputable def zeroFreeCriterion_of_honestPhaseChargeZeroBridge
226 (hb : HonestPhaseChargeZeroBridge) :
227 ZeroFreeCriterion where
228 logDeriv_bounded_on_strip := fun _ hσ => carrierDerivBound_pos hσ
proof body
Definition body.
229 carrier_nonvanishing_on_strip := fun _ hσ => carrier_nonvanishing hσ
230 honest_phase_family := honest_argument_principle_phase_family
231 charge_zero_of_honest_phase :=
232 charge_zero_of_honest_phase_of_chargeZeroBridge hb
233
234/-- Any direct honest-phase charge-zero bridge proves the analytic RH core. -/