zeroFreeCriterion_of_honestPhaseChargeZeroBridge
plain-language theorem explainer
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.
Claim. Given 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.