realizedDefectCostBounded_of_charge_zero_and_excessBounded
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove that excess is bounded for any concrete family.
- Does not apply to arbitrary annular meshes outside realized sampled families.
- Does not address analytic control of the regular-part error term.
- Does not quantify cost bounds that depend on mesh depth.
formal statement (Lean)
270theorem realizedDefectCostBounded_of_charge_zero_and_excessBounded
271 (fam : DefectSampledFamily)
272 (hzero : fam.sensor.charge = 0)
273 (hexcess : RealizedDefectAnnularExcessBounded fam) :
274 RealizedDefectAnnularCostBounded fam := by
proof body
Tactic-mode proof.
275 obtain ⟨K, hK⟩ := hexcess
276 refine ⟨K, ?_⟩
277 intro N
278 have hfloor : annularTopologicalFloor N (fam.sensor.charge) = 0 := by
279 rw [hzero, annularTopologicalFloor_zero]
280 have hexN : annularExcess (fam.mesh N) ≤ K := hK N
281 unfold annularExcess at hexN
282 rw [fam.charge_spec N, hfloor] at hexN
283 simpa using hexN
284
285/-- For a realized sampled family, bounded total cost is exactly the conjunction
286of:
2871. zero charge, and
2882. bounded excess above the topological floor.
289
290This theorem isolates the remaining mathematical task cleanly: after the
291realized-family refactor, the analytically natural target is no longer a bound
292on arbitrary meshes, but a proof that the realized family has bounded excess
293and hence can only occur with zero charge. -/