charge_zero_of_honestPhaseAdmissible
plain-language theorem explainer
Admissible honest phase data for a zeta phase family has zero sensor charge. Analysts targeting the Riemann hypothesis via Route C would cite this to equate bounded annular J-cost with charge cancellation. The proof is a one-line wrapper that feeds the finiteRecognitionBudget field directly into the prior bounded-cost charge-zero theorem.
Claim. Let $zfd$ be zeta phase family data. If the realized sampled family of $zfd$ has bounded total annular J-cost, then the charge recorded by $zfd$.sensor equals zero.
background
The module narrows the analytic RH target to honest zeta-derived phase data. HonestPhaseAdmissible $zfd$ is the predicate that the realized sampled family extracted from $zfd$.phaseFamily satisfies RealizedDefectAnnularCostBounded, i.e., the total annular J-cost remains finite. This predicate sits inside the eight-tick phase structure whose phases are $kπ/4$ for $k=0,…,7$ and whose reversal map on Fin 8 is an involution.
proof idea
The proof is a one-line wrapper that applies honestPhaseFamily_charge_zero_of_costBounded to the supplied $zfd$ and the finiteRecognitionBudget field extracted from the HonestPhaseAdmissible hypothesis.
why it matters
The result supplies the charge-zero direction needed by chargeZeroBridge_of_admissibilityBridge and by honestPhaseAdmissible_iff_charge_zero. It is invoked inside witnessed_rh_from_honestPhaseAdmissibility to reach the witnessed RH core. In the Recognition framework it closes the link from finite recognition budget to zero charge inside the eight-tick octave, directly supporting the zero-free criterion of AnalyticTrace.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.