realizedRingPerturbationError

formal source

 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
 169are uniformly bounded across refinement depth `N`. This is exactly the remaining
 170analytic input needed after the perturbative `phiCost` reduction. -/
 171structure RingPerturbationControl (fam : DefectSampledFamily) where
 172  small : ∀ N : ℕ, ∀ n : Fin N, ∀ j : Fin (8 * (n.val + 1)),
 173    |Real.log Constants.phi *
 174        (((fam.mesh N).rings n).increments j -
 175          (-(2 * Real.pi * ((fam.mesh N).charge : ℝ)) / (8 * (n.val + 1) : ℝ)))| ≤ 1
 176  total_bounded : ∃ K : ℝ, ∀ N : ℕ,
 177    ∑ n : Fin N, realizedRingPerturbationError fam N n ≤ K
 178
 179/-- A perturbation-control package yields the ring-regular-error package needed
 180for bounded annular excess. -/
 181noncomputable def ringRegularErrorBound_of_ringPerturbationControl