admissibilityBridge_of_chargeZeroBridge
plain-language theorem explainer
Definition that converts a direct charge-zero bridge for honest zeta phase data into a global admissibility bridge. Analysts pursuing the analytic route to the Riemann hypothesis cite it when equating bounded-cost and zero-charge formulations of phase data. It is realized as a one-line wrapper that invokes the right-to-left direction of the equivalence between honest-phase admissibility and zero sensor charge.
Claim. Given a structure $hb$ asserting that the sensor charge vanishes for every honest zeta phase family datum $zfd$, the structure asserting that every such $zfd$ satisfies the honest-phase admissibility predicate is obtained by applying the right-to-left direction of the equivalence between admissibility and zero charge.
background
In the Honest Phase Admissibility module, Route C restricts the analytic Riemann hypothesis target to honest zeta-derived phase data. The structure HonestPhaseAdmissibilityBridge requires that every ZetaPhaseFamilyData satisfies the HonestPhaseAdmissible predicate. The upstream HonestPhaseChargeZeroBridge requires only that the sensor charge is zero for each such datum. The equivalence theorem honestPhaseAdmissible_iff_charge_zero states that HonestPhaseAdmissible zfd holds if and only if the charge is zero, with the reverse direction relying on a prior bounded-excess result for honest phase data.
proof idea
This definition is a one-line wrapper. It populates the admissible field of the output structure by applying the right-to-left implication of honestPhaseAdmissible_iff_charge_zero to the charge-zero witness supplied by the input bridge hb.
why it matters
This definition completes one direction of the equivalence between the admissibility bridge and the charge-zero bridge, as stated in the downstream theorem honestPhaseAdmissibilityBridge_iff_chargeZeroBridge. It supports the analytic trace route by providing the direct charge-zero conclusion needed for the ZeroFreeCriterion in AnalyticTrace. Within the Recognition framework it advances the narrowing of the Riemann hypothesis target to honest phase data without invoking total cost bounds directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.