honestPhaseFamily_charge_zero_of_costBounded
plain-language theorem explainer
If zeta phase family data has bounded realized annular defect cost on its sampled family, the attached sensor charge vanishes. Analysts bridging phase families to defect budgets cite this to reduce charge-zero targets to cost bounds. The proof is a one-line wrapper applying the realized defect cost bounded iff charge zero and excess bounded lemma then projecting the first component.
Claim. If the sampled family of the phase family in zeta phase family data $zfd$ realizes bounded annular defect cost, then the charge of the sensor in $zfd$ is zero.
background
The Honest Phase Budget Bridge module supplies perturbation witnesses that convert honest phase families into bounded annular excess data on the sampled side, beyond completed xi symmetry. ZetaPhaseFamilyData packages a phase family together with its sensor; RealizedDefectAnnularCostBounded asserts that the total cost of the sampled family is finite. Upstream, phase denotes the eight-tick values $k pi/4$ for $k=0..7$, while cost denotes the J-cost of a recognition event.
proof idea
The proof forms hzero by applying the mp direction of realizedDefectCostBounded_iff_charge_zero_and_excessBounded to the sampled family and the given cost bound. It then uses simpa with the toSampledFamily and family_sensor projections to extract the charge-zero part of hzero.
why it matters
This theorem is invoked directly by charge_zero_of_honestPhaseAdmissible to conclude zero charge for admissible honest phase data and by the equivalence honestPhaseFamily_cost_bounded_iff_charge_zero. It isolates the remaining bounded-cost upgrade required by the analytic route, as stated in the module documentation on turning honest phase families into bounded annular data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.