 446      rw [hw_pole, hw_reg, add_zero] }
 447
 448/-- The genuine phase data has the correct charge. -/
 449private theorem genuineZetaDerivedPhaseData_charge
 450    (qlf : QuantitativeLocalFactorization) (n : ℕ) (hn : 0 < n) :
 451    (genuineZetaDerivedPhaseData qlf n hn).charge = -qlf.order := by
 452  rfl
 453
 454/-- Build a `RegularFactorPhase` from a `QuantitativeLocalFactorization`
 455at a given level. This is the genuine Lipschitz-controlled phase of the
 456regular factor on the `n`th circle. -/
 457noncomputable def qlf_regularFactorPhase
 458    (qlf : QuantitativeLocalFactorization) (n : ℕ) (hn : 0 < n) :
 459    RegularFactorPhase := by
 460  have hnR : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn
 461  have hd : (0 : ℝ) < ↑n + 1 := by linarith
 462  have hgt1 : (1 : ℝ) < ↑n + 1 := by linarith
 463  exact regularFactorPhaseFromWitness qlf.toLocalMeromorphicWitness
 464    (qlf.radius / (↑n + 1)) (div_pos qlf.radius_pos hd) (div_lt_self qlf.radius_pos hgt1)
 465    qlf.logDerivBound qlf.logDerivBound_pos
 466
 467/-- A defect phase family using genuine regular-factor phase data.
 468Each level carries non-trivial perturbation from the regular factor's
 469Lipschitz-controlled phase, unlike the synthetic `zetaDerivedPhaseFamily`
 470which has identically zero perturbation. -/
 471noncomputable def genuineZetaDerivedPhaseFamily
 472    (sensor : DefectSensor)
 473    (qlf : QuantitativeLocalFactorization)
 474    (horder : qlf.order = -sensor.charge) : DefectPhaseFamily where
 475  sensor := sensor
 476  witnessRadius := qlf.radius
 477  witnessRadius_pos := qlf.radius_pos
 478  phaseAtLevel n hn := genuineZetaDerivedPhaseData qlf n hn
 479  charge_uniform n hn := by

papers checked against this theorem

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