honestPhaseAdmissible_iff_charge_zero
plain-language theorem explainer
Honest phase admissibility for zeta phase family data holds exactly when the sensor charge is zero. Analysts working on Route C of the analytic Riemann hypothesis would cite this equivalence to reduce admissibility to a charge check. The term proof is a direct biconditional constructor that applies the forward charge-zero lemma and the reverse of the bounded-cost equivalence.
Claim. For zeta phase family data $zfd$, the predicate that its realized sampled family has bounded total annular J-cost holds if and only if the charge of its sensor is zero.
background
Route C narrows the analytic RH target to honest zeta-derived phase data. This module defines the admissibility predicate for that data and proves equivalence to the charge-zero conclusion needed by AnalyticTrace.ZeroFreeCriterion. Honest phase data is admissible when its realized sampled family has finite recognition budget, i.e., bounded total annular J-cost. Upstream results supply the eight-tick phase definition (periodic with period $2π$) and the active edge count $A=1$ per fundamental tick that support phase-family constructions.
proof idea
The term-mode proof opens with constructor to split the biconditional. The forward direction applies the sibling lemma charge_zero_of_honestPhaseAdmissible. The reverse direction applies the mpr of the sibling equivalence honestPhaseFamily_cost_bounded_iff_charge_zero to build the finite-recognition-budget structure.
why it matters
The result feeds admissibilityBridge_of_chargeZeroBridge and witnessedHonestPhaseAdmissibilityBridge_of_rh. It supplies the charge-zero step required by the zero-free criterion for honest phase data. In the Recognition framework it closes the link from bounded J-cost to the analytic trace, consistent with the recognition composition law and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.