zeroFreeCriterion_of_honestPhaseCostBridge
plain-language theorem explainer
This definition assembles a zero-free criterion for the zeta function from any honest-phase bounded annular cost bridge. Analytic number theorists working on axiom-free routes to the Riemann hypothesis would cite it when composing the pure analytic path. The construction is a direct field assignment that pulls the logarithmic derivative bound from carrier estimates, nonvanishing from the carrier function, the phase family from the argument principle, and charge zero from the bridge theorem.
Claim. Given a bridge $hb$ asserting that every honest zeta phase family attached to a witnessed defect sensor has bounded realized annular cost, the zero-free criterion is the structure whose logarithmic derivative is positively bounded on the half-strip $1/2 < Re(s)$, whose carrier is nonvanishing there, whose honest phase family is supplied by the argument principle, and whose charge-zero property follows from the bridge theorem.
background
The AnalyticTrace module assembles an axiom-free interface for the Riemann hypothesis by packaging carrier estimates, phase families, and charge-zero results. The HonestPhaseCostBridge structure requires that for any witnessed defect sensor and matching zeta phase family data the realized defect annular cost remains bounded. The ZeroFreeCriterion structure collects four fields: a positive bound on the carrier logarithmic derivative for $1/2 < Re(s)$, nonvanishing of the carrier in that region, existence of an honest phase family for any nonzero-charge sensor, and a charge-zero conclusion drawn from the honest phase data.
proof idea
The definition constructs the ZeroFreeCriterion structure by direct field assignment. It sets the logarithmic derivative bound to the positive carrier derivative estimate, the nonvanishing field to the carrier nonvanishing statement, the honest phase family to the argument principle family, and the charge-zero field to the theorem that extracts charge zero from the supplied cost bridge.
why it matters
This definition completes the pure analytic route by turning any honest-phase cost bridge into a full zero-free criterion, which is then invoked by the direct RH theorem that derives a contradiction from nonzero charge. It sits alongside the ontology route that uses the Euler boundary bridge assumption and supports the module's goal of replacing former axioms with proved winding and floor-coverage statements. In the Recognition framework it supplies the analytic counterpart to the eight-tick and cost-based foundations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.