honestPhaseFamily_cost_bounded_iff_charge_zero
plain-language theorem explainer
The equivalence establishes that for zeta-derived phase family data the realized annular cost of the attached sampled defect family is bounded precisely when the sensor charge vanishes. Route C analysts tracking the analytic route to the Riemann hypothesis would cite this to separate the already-settled excess control from the remaining charge-zero upgrade. The proof is a direct biconditional split that invokes the one-way charge extraction from bounded cost together with the cost-boundedness theorem that uses zero charge plus excess bounded.
Claim. For zeta phase family data $z$, the annular cost of the realized sampled defect family attached to $z$ is bounded independently of mesh refinement if and only if the defect sensor charge of $z$ vanishes.
background
The Honest Phase Budget Bridge module supplies the quantitative perturbation control needed to convert an honest phase family into bounded annular excess data on the sampled side. A ZetaPhaseFamilyData packages a DefectPhaseFamily (phase samples drawn from the Weierstrass factorization of the reciprocal zeta function near a hypothetical zero) together with a DefectSensor that records charge and real-part location. RealizedDefectAnnularCostBounded asserts the existence of a uniform real $K$ such that annularCost on every mesh refinement stays at most $K$. Upstream results include honestPhaseFamily_excess_bounded (which already secures bounded excess for these data) and realizedDefectCostBounded_of_charge_zero_and_excessBounded (which converts zero charge plus bounded excess into bounded total cost).
proof idea
The tactic proof opens with constructor to split the biconditional. The forward direction applies honestPhaseFamily_charge_zero_of_costBounded directly to the given bounded-cost hypothesis. The reverse direction first uses simpa to align the charge field across the toSampledFamily projection, then calls realizedDefectCostBounded_of_charge_zero_and_excessBounded with the zero-charge fact and the excess-boundedness supplied by honestPhaseFamily_excess_bounded.
why it matters
This equivalence is invoked by honestPhase_routeC_bottleneck to record the exact Route C analytic bottleneck (bounded excess is already proved; the missing step is the upgrade to zero charge) and by honestPhaseAdmissible_iff_charge_zero to close the admissibility characterization. Within the Recognition framework it isolates the remaining open upgrade after the perturbation witness, the J-uniqueness fixed point, and the eight-tick octave structures have been secured.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.