realizedDefectAnnularExcessBounded_of_costBounded
A uniform bound on the annular cost of any realized defect sampled family yields a uniform bound on its annular excess. Researchers refining the statement of Axiom 2 cite this implication to isolate the regular-part control problem. The proof obtains the cost witness K, invokes nonnegativity of the topological floor at each level, rewrites the charge specification, and closes with linear arithmetic.
claimSuppose $fam$ is a defect sampled family. If there exists a real number $K$ such that the annular cost of $fam.mesh(N)$ is at most $K$ for every natural number $N$, then there exists a real number $K'$ such that the annular excess of $fam.mesh(N)$ is at most $K'$ for every $N$.
background
Defect sampled families consist of a defect sensor, a function assigning an annular mesh to each natural number, and a charge specification ensuring consistency with the sensor. Realized defect annular cost bounded means the annular costs of these meshes admit a uniform real upper bound across all levels. Realized defect annular excess bounded is the parallel statement for the excess obtained by subtracting the topological floor.
proof idea
Term construction obtains the bound K from the hypothesis of cost boundedness. It refines the goal to exhibit the same K for excess boundedness. At an arbitrary level N the definition of annular excess is unfolded, the nonnegativity of the topological floor is invoked, the cost bound is applied, the charge is rewritten from the family specification, and linear arithmetic closes the inequality.
why it matters in Recognition Science
The result is applied in the equivalence theorem that decomposes bounded cost into zero charge together with bounded excess. This isolates the remaining task as a proof of bounded excess for the realized family. In the broader framework it advances the control of annular costs for the defect sampled trace, separating topological from regular contributions in the approach to Axiom 2.
scope and limits
- Does not establish the boundedness of excess for nonzero charge.
- Applies exclusively to realized sampled families rather than arbitrary meshes.
- Supplies no explicit numerical bound.
- Does not construct or guarantee the existence of such families.
formal statement (Lean)
254theorem realizedDefectAnnularExcessBounded_of_costBounded
255 (fam : DefectSampledFamily)
256 (hcost : RealizedDefectAnnularCostBounded fam) :
257 RealizedDefectAnnularExcessBounded fam := by
proof body
Term-mode proof.
258 obtain ⟨K, hK⟩ := hcost
259 refine ⟨K, ?_⟩
260 intro N
261 unfold annularExcess
262 have hfloor : 0 ≤ annularTopologicalFloor N (fam.sensor.charge) :=
263 annularTopologicalFloor_nonneg N fam.sensor.charge
264 have hcostN : annularCost (fam.mesh N) ≤ K := hK N
265 rw [fam.charge_spec N]
266 linarith
267
268/-- If the sensor charge is zero, then bounded excess is equivalent to bounded
269total cost because the topological floor vanishes identically. -/