direct_rh_from_honestPhaseAdmissibility
plain-language theorem explainer
A global honest-phase admissibility bridge for all zeta phase family data implies that no witnessed defect sensor can carry non-zero charge. Analysts reducing the Riemann hypothesis to phase admissibility under Route C would cite this result. The proof is a one-line term wrapper that feeds the zero-free criterion extracted from the bridge into rh_from_zero_free_criterion.
Claim. Let $hb$ be a structure asserting that every zeta phase family datum is honest-phase admissible. Then for every witnessed defect sensor, its charge equals zero.
background
The module narrows the analytic Riemann hypothesis target to honest zeta-derived phase data via Route C. It defines an admissibility predicate for that data and establishes equivalence to the charge-zero conclusion required by AnalyticTrace.ZeroFreeCriterion. HonestPhaseAdmissibilityBridge is the structure supplying the universal quantification over ZetaPhaseFamilyData that yields the direct charge-zero bridge for AnalyticTrace.
proof idea
The proof is a one-line term-mode wrapper. It applies rh_from_zero_free_criterion to the zero-free criterion produced by zeroFreeCriterion_of_honestPhaseAdmissibility on the supplied bridge hb.
why it matters
This theorem supplies the direct analytic RH core from the honest-phase admissibility bridge. It realizes the Route C narrowing in the Recognition framework, linking to the eight-tick phase structure and the charge-zero requirement of the zero-free criterion. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.