defectPhasePureIncrement

formal source

 149
 150/-- The uniform pure winding increment on the `n`th sampled ring for a defect
 151phase family of fixed charge. -/
 152noncomputable def defectPhasePureIncrement (dpf : DefectPhaseFamily) (n : ℕ) : ℝ :=
 153  -(2 * Real.pi * (dpf.sensor.charge : ℝ)) / (8 * n : ℝ)
 154
 155/-- Quantitative perturbation data for the regular factor in a defect phase
 156family.
 157
 158This structure captures exactly the data needed downstream to build the
 159`RingPerturbationControl` witness for the canonical sampled family:
 160
 1611. each sampled increment splits as the pure winding increment plus a regular
 162   perturbation `ε`;
 1632. every `ε` stays in the unit perturbative regime for the proved
 164   `phiCost` bound; and
 1653. the total linear and quadratic perturbation budgets are uniformly bounded in
 166   the refinement depth `N`. -/
 167structure DefectPhasePerturbationWitness (dpf : DefectPhaseFamily) where
 168  epsilon : (n : ℕ) → 0 < n → Fin (8 * n) → ℝ
 169  increment_eq : ∀ n hn j,
 170    (dpf.phaseAtLevel n hn).sampleIncrements n j =
 171      defectPhasePureIncrement dpf n + epsilon n hn j
 172  small : ∀ n hn j,
 173    |Real.log Constants.phi * epsilon n hn j| ≤ 1
 174  linear_term_bounded : ∃ K : ℝ, ∀ N : ℕ,
 175    ∑ n : Fin N,
 176      phiCostLinearCoeff |defectPhasePureIncrement dpf (n.val + 1)| *
 177        ∑ j : Fin (8 * (n.val + 1)),
 178          |epsilon (n.val + 1) (Nat.succ_pos n.val) j| ≤ K
 179  quadratic_term_bounded : ∃ K : ℝ, ∀ N : ℕ,
 180    ∑ n : Fin N,
 181      phiCostQuadraticCoeff |defectPhasePureIncrement dpf (n.val + 1)| *
 182        ∑ j : Fin (8 * (n.val + 1)),