def
definition
trivialDefectPhaseFamily
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.NumberTheory.MeromorphicCircleOrder on GitHub at line 141.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
of -
phase -
defect -
of -
of -
for -
of -
uniform -
winding -
DefectSensor -
DefectPhaseFamily -
DefectPhaseFamily -
pureDefectPhaseData -
phase
used by
formal source
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.
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