RingRegularErrorBound

formal source

 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)),
 156        |((fam.mesh N).rings n).increments j - u| +
 157    phiCostQuadraticCoeff |u| *
 158      ∑ j : Fin (8 * (n.val + 1)),
 159        (((fam.mesh N).rings n).increments j - u) ^ 2
 160
 161/-- Quantitative perturbation control for a realized sampled family.
 162
 163The `small` field says each sampled increment stays within the unit-scale
 164perturbative regime of `phiCost` once expressed as
 165
 166`Δ_j = (pure winding increment) + ε_j`.
 167
 168The `total_bounded` field says the resulting linear-plus-quadratic error sums