pureDefectPhaseData

formal source

 123  charge_uniform : ∀ n hn, (phaseAtLevel n hn).charge = sensor.charge
 124
 125/-- A constant-radius phase package carrying the prescribed defect charge. -/
 126noncomputable def pureDefectPhaseData (sensor : DefectSensor) :
 127    (n : ℕ) → 0 < n → ContinuousPhaseData :=
 128  fun n hn =>
 129    { center := (sensor.realPart : ℂ)
 130      radius := 1
 131      radius_pos := by norm_num
 132      phase := fun θ => (-(sensor.charge : ℤ) : ℝ) * θ
 133      phase_continuous := by
 134        continuity
 135      charge := sensor.charge
 136      phase_winding := by
 137        simp [sub_eq_add_neg]
 138        ring }
 139
 140/-- A defect phase family with the correct charge but no regular perturbation. -/
 141noncomputable def trivialDefectPhaseFamily (sensor : DefectSensor) : DefectPhaseFamily where
 142  sensor := sensor
 143  witnessRadius := 1
 144  witnessRadius_pos := by norm_num
 145  phaseAtLevel := pureDefectPhaseData sensor
 146  charge_uniform := by
 147    intro n hn
 148    rfl
 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.