zeroFreeCriterion_of_honestPhaseAdmissibility
plain-language theorem explainer
A global honest-phase admissibility bridge for all zeta phase family data yields the zero-free criterion structure required by the analytic trace. Researchers deriving the Riemann hypothesis via Recognition Science Route C would cite this to connect phase admissibility to the absence of zeros in the critical strip. The definition is a one-line composition that converts the input bridge to a charge-zero bridge and then invokes the zero-free criterion constructor.
Claim. Let $B$ be a global admissibility bridge asserting that every honest zeta phase family datum satisfies the admissibility predicate. Then $B$ determines a zero-free criterion whose components are boundedness of the logarithmic derivative on the strip $1/2 < Re(s) < 1$, non-vanishing of the carrier function on that strip, and the associated honest phase family data.
background
The Honest Phase Admissibility module implements Route C, which narrows the analytic Riemann hypothesis target to honest zeta-derived phase data. The central structure HonestPhaseAdmissibilityBridge is a record requiring that for every zeta phase family datum the phase is admissible; its doc-comment states that this bridge supplies the direct charge-zero bridge used in AnalyticTrace. The target ZeroFreeCriterion from AnalyticTrace packages witnessed zeta-inverse defect data in the strip together with analytic estimates that force the corresponding defect charge to vanish.
proof idea
The definition is a one-line wrapper that first applies chargeZeroBridge_of_admissibilityBridge to the input HonestPhaseAdmissibilityBridge and then feeds the resulting charge-zero bridge into zeroFreeCriterion_of_honestPhaseChargeZeroBridge.
why it matters
This definition supplies the ZeroFreeCriterion instance required by the downstream theorem direct_rh_from_honestPhaseAdmissibility, whose doc-comment states that a global honest-phase admissibility bridge proves the analytic RH core. It closes the bridge from phase admissibility to the zero-free property inside the Recognition Science analytic route, consistent with the eight-tick phase structure and the charge-zero requirement of the analytic trace.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.