chargeZeroBridge_of_admissibilityBridge
plain-language theorem explainer
This definition constructs a direct charge-zero bridge for honest zeta phase data from a global admissibility bridge. Researchers on the analytic route to the Riemann hypothesis cite it to discharge the charge-zero field in the ZeroFreeCriterion. It is realized as a one-line wrapper that applies the charge-zero extraction lemma to the admissible predicate supplied by the input bridge.
Claim. Let $B$ be a global admissibility bridge asserting that every zeta phase family datum $zfd$ is honest-phase admissible. Then the induced charge-zero bridge $C$ satisfies that for every such $zfd$, the sensor charge of $zfd$ equals zero, obtained by applying the extraction that admissibility implies charge zero to the witness $B.admissible(zfd)$.
background
The module defines predicates and bridges that narrow the analytic RH target to honest zeta-derived phase data. HonestPhaseAdmissibilityBridge is the structure with field admissible : ∀ zfd : ZetaPhaseFamilyData, HonestPhaseAdmissible zfd. HonestPhaseChargeZeroBridge from AnalyticTrace is the structure with field charge_zero_of_honest_phase : ∀ zfd : ZetaPhaseFamilyData, zfd.sensor.charge = 0. The module proves these two structures are equivalent, so that the admissibility predicate supplies exactly the charge-zero conclusion required by AnalyticTrace.ZeroFreeCriterion.
proof idea
The definition is a one-line wrapper that constructs HonestPhaseChargeZeroBridge by setting its charge_zero_of_honest_phase field to the function sending zfd to charge_zero_of_honestPhaseAdmissible zfd (hb.admissible zfd).
why it matters
This supplies the forward map in the equivalence theorem honestPhaseAdmissibilityBridge_iff_chargeZeroBridge, which in turn feeds the definition zeroFreeCriterion_of_honestPhaseAdmissibility. It therefore discharges the charge-zero requirement of AnalyticTrace.ZeroFreeCriterion without needing bounded total cost. In the Recognition Science framework this step supports the analytic route by converting the admissibility predicate into the direct charge-zero bridge used downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.