RealizedDefectAnnularExcessBounded

formal source

 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
 149increments are written as the pure winding increment plus a regular
 150perturbation. -/
 151noncomputable def realizedRingPerturbationError (fam : DefectSampledFamily)
 152    (N : ℕ) (n : Fin N) : ℝ :=
 153  let u : ℝ := -(2 * Real.pi * ((fam.mesh N).charge : ℝ)) / (8 * (n.val + 1) : ℝ)
 154  phiCostLinearCoeff |u| *
 155      ∑ j : Fin (8 * (n.val + 1)),