realizedDefectCostBounded_of_charge_zero_and_excessBounded
plain-language theorem explainer
When a defect sensor carries zero charge, any uniform bound on annular excess for its realized sampled family immediately yields a uniform bound on total annular cost. Analysts refining the statement of Axiom 2 cite the result to reduce cost control to excess control alone after the topological floor is removed. The short tactic proof extracts the excess constant, rewrites the floor term to zero via the charge hypothesis, and substitutes the family charge specification to equate excess with cost.
Claim. Let $F$ be a realized sampled family of annular meshes attached to a defect sensor. If the sensor charge of $F$ is zero and there exists a real constant $K$ such that the annular excess of each mesh in $F$ is at most $K$, then there exists a real constant $K'$ such that the annular cost of each mesh in $F$ is at most $K'$.
background
DefectSampledFamily is a structure pairing a defect sensor with a sequence of realized annular meshes whose charges match the sensor charge at every depth. RealizedDefectAnnularCostBounded asserts a uniform upper bound on annularCost across all refinement depths, while RealizedDefectAnnularExcessBounded asserts the same bound on annularExcess, the remainder after subtracting the topological floor fixed by the charge sector. annularTopologicalFloor N 0 = 0 supplies the key identity that the floor vanishes for zero charge.
proof idea
The proof extracts the bound constant K from the excess hypothesis. It rewrites annularTopologicalFloor N (fam.sensor.charge) to zero using the zero-charge lemma. After unfolding annularExcess and substituting the charge specification from the family, the excess inequality is shown to be identical to the required cost inequality, which is discharged by simpa.
why it matters
The result feeds the equivalence realizedDefectCostBounded_iff_charge_zero_and_excessBounded and the honest-phase cost bridge used in HonestPhaseCostBridge_of_rh. It isolates the remaining task of proving bounded excess for the canonical phase-sampled family, which is the quantitatively plausible part of the defect-cost story once the topological floor is removed. In the Recognition framework this supports the refined Axiom 2 by showing that zero-charge families with controlled regular remainder have bounded cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.