HonestPhaseAdmissibilityBridge
plain-language theorem explainer
A global admissibility bridge asserts that every honest zeta phase family datum satisfies the finite recognition budget condition of bounded annular J-cost. Analysts working on the analytic Riemann hypothesis via Recognition Science Route C cite this structure to obtain the charge-zero bridge required by AnalyticTrace. The declaration is a single-field structure definition with no computational content or proof obligations.
Claim. A structure $B$ is a global admissibility bridge when, for every zeta phase family datum $zfd$, the corresponding honest phase data is admissible, i.e., its realized sampled family has bounded total annular $J$-cost.
background
The Honest Phase Admissibility module implements Route C, which narrows the analytic RH target to honest zeta-derived phase data. The sibling predicate HonestPhaseAdmissible requires finiteRecognitionBudget, defined as RealizedDefectAnnularCostBounded on the sampled family obtained from zfd.phaseFamily.toSampledFamily. The module proves this predicate is equivalent to the charge-zero conclusion needed by AnalyticTrace.ZeroFreeCriterion.
proof idea
This is a structure definition with one field that universally quantifies the HonestPhaseAdmissible predicate over all ZetaPhaseFamilyData. No tactics or lemmas are applied; the declaration simply packages the admissibility assertion for later conversion to charge-zero form.
why it matters
The structure supplies the global bridge that converts directly to HonestPhaseChargeZeroBridge via chargeZeroBridge_of_admissibilityBridge, which in turn yields the ZeroFreeCriterion and the analytic RH core theorem direct_rh_from_honestPhaseAdmissibility. It completes the equivalence honestPhaseAdmissibilityBridge_iff_chargeZeroBridge and closes the Route C link from bounded J-cost to zero-free results in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.