`DefectPhaseFamily`

definition

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.MeromorphicCircleOrder
domain: NumberTheory
line: 118 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.NumberTheory.MeromorphicCircleOrder on GitHub at line 118.

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

 115
 116/-! ### §3. Defect sensor phase families -/
 117
 118structure DefectPhaseFamily where
 119  sensor : DefectSensor
 120  witnessRadius : ℝ
 121  witnessRadius_pos : 0 < witnessRadius
 122  phaseAtLevel : (n : ℕ) → 0 < n → ContinuousPhaseData
 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

papers checked against this theorem

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