`ringRegularErrorBound_of_ringPerturbationControl`

definition

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.DefectSampledTrace
domain: NumberTheory
line: 181 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.NumberTheory.DefectSampledTrace on GitHub at line 181.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 178
 179/-- A perturbation-control package yields the ring-regular-error package needed
 180for bounded annular excess. -/
 181noncomputable def ringRegularErrorBound_of_ringPerturbationControl
 182    (fam : DefectSampledFamily) (hctrl : RingPerturbationControl fam) :
 183    RingRegularErrorBound fam := by
 184  refine
 185    { error := realizedRingPerturbationError fam
 186      ring_estimate := ?_
 187      total_error_bounded := hctrl.total_bounded }
 188  intro N n
 189  have hcharge : ((fam.mesh N).rings n).winding = (fam.mesh N).charge := by
 190    rw [((fam.mesh N).uniform_charge n)]
 191  have hsmall_ring :
 192      ∀ j : Fin (8 * n.val.succ),
 193        |Real.log Constants.phi *
 194            (((fam.mesh N).rings n).increments j -
 195              (-(2 * Real.pi * ((((fam.mesh N).rings n).winding : ℤ) : ℝ)) /
 196                (8 * n.val.succ : ℝ)))| ≤ 1 := by
 197    intro j
 198    have hj := hctrl.small N n j
 199    simpa [hcharge, Nat.succ_eq_add_one] using hj
 200  have hring :=
 201    ringCost_le_topologicalFloor_add_linear_quadratic_error
 202      (Nat.succ_pos n.val) ((fam.mesh N).rings n) hsmall_ring
 203  rw [hcharge] at hring
 204  simpa [realizedRingPerturbationError, add_assoc] using hring
 205
 206/-- Summing the ring-level estimate yields a bound for annular excess.
 207
 208This is the unconditional algebraic step:
 209
 210`ringCost ≤ topologicalFloor + regularError`
 211

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.