RealizedDefectAnnularCostBounded

formal source

 115/-- The annular cost of a realized sampled family is bounded independently of
 116mesh refinement. This is the realizable replacement for the previous
 117over-strong quantification over arbitrary `AnnularMesh` values. -/
 118def RealizedDefectAnnularCostBounded (fam : DefectSampledFamily) : Prop :=
 119  ∃ K : ℝ, ∀ N : ℕ, annularCost (fam.mesh N) ≤ K
 120
 121/-- The annular excess of a realized sampled family is bounded independently of
 122mesh refinement. This is the quantitatively plausible part of the defect-cost
 123story: after removing the topological floor, only the regular remainder should
 124need analytic control. -/
 125def RealizedDefectAnnularExcessBounded (fam : DefectSampledFamily) : Prop :=
 126  ∃ K : ℝ, ∀ N : ℕ, annularExcess (fam.mesh N) ≤ K
 127
 128/-! ### §3a. Ring-level regular-part error control -/
 129
 130/-- A ring-level regular-part error package for a realized sampled family.
 131
 132For each depth `N` and ring `n`, the sampled ring cost is bounded by the
 133topological floor for its charge sector plus an error term coming from the
 134regular factor in the local meromorphic factorization. The total error across
 135all rings is uniformly bounded in `N`.
 136
 137This is the exact quantitative input needed to prove bounded annular excess. -/
 138structure RingRegularErrorBound (fam : DefectSampledFamily) where
 139  error : ∀ N : ℕ, Fin N → ℝ
 140  ring_estimate : ∀ N : ℕ, ∀ n : Fin N,
 141    ringCost ((fam.mesh N).rings n) ≤
 142      topologicalFloor (n.val + 1) ((fam.mesh N).charge) + error N n
 143  total_error_bounded : ∃ K : ℝ, ∀ N : ℕ, ∑ n : Fin N, error N n ≤ K
 144
 145/-- The explicit linear-plus-quadratic perturbation error on one realized ring.
 146
 147This is the error term delivered by
 148`ringCost_le_topologicalFloor_add_linear_quadratic_error` once the ring