def
definition
def or abbrev
mkSharedCirclePair
show as:
view Lean formalization →
formal statement (Lean)
154noncomputable def mkSharedCirclePair
155 (sensor : DefectSensor)
156 (qlf : QuantitativeLocalFactorization)
157 (horder : qlf.order = -sensor.charge) :
158 SharedCircleFamilyPair where
159 sensor := sensor
proof body
Definition body.
160 carrierPhaseFamily := {
161 sensor := { charge := 0, realPart := sensor.realPart, in_strip := sensor.in_strip }
162 witnessRadius := qlf.radius
163 witnessRadius_pos := qlf.radius_pos
164 phaseAtLevel := fun n hn => by
165 have hnR : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn
166 have hd : (0 : ℝ) < ↑n + 1 := by linarith
167 have hgt1 : (1 : ℝ) < ↑n + 1 := by linarith
168 let rfp := regularFactorPhaseFromWitness qlf.toLocalMeromorphicWitness
169 (qlf.radius / (↑n + 1)) (div_pos qlf.radius_pos hd) (div_lt_self qlf.radius_pos hgt1)
170 qlf.logDerivBound qlf.logDerivBound_pos
171 exact rfp.toContinuousPhaseData
172 charge_uniform := fun n hn => by
173 simp only
174 have hnR : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn
175 have hd : (0 : ℝ) < ↑n + 1 := by linarith
176 have hgt1 : (1 : ℝ) < ↑n + 1 := by linarith
177 exact (regularFactorPhaseFromWitness qlf.toLocalMeromorphicWitness
178 (qlf.radius / (↑n + 1)) (div_pos qlf.radius_pos hd) (div_lt_self qlf.radius_pos hgt1)
179 qlf.logDerivBound qlf.logDerivBound_pos).charge_zero
180 }
181 defectPhaseFamily := genuineZetaDerivedPhaseFamily sensor qlf horder
182 carrier_sensor_charge_zero := rfl
183 defect_sensor_eq := rfl
184 shared_radius := rfl
185
186/-- The shared-circle pair's carrier has bounded excess because the regular
187factor phase is Lipschitz-controlled.
188
189The carrier family has charge 0, so `defectPhasePureIncrement = 0`:
190- `small`: via `epsilon_log_phi_small` (same underlying `RegularFactorPhase`)
191- `linear_term_bounded`: trivially 0 since `phiCostLinearCoeff(0) = 0`
192- `quadratic_term_bounded`: `phiCostQuadraticCoeff(0) = κ` times convergent `∑ ε²` -/