genuineZetaDerivedPhaseData

formal source

 417this construction passes through `charge_additive` to combine:
 418- pole factor: charge = -order, phase = order * θ
 419- regular factor: charge = 0, phase = genuine covering-space lift -/
 420private noncomputable def genuineZetaDerivedPhaseData
 421    (qlf : QuantitativeLocalFactorization) (n : ℕ) (hn : 0 < n) :
 422    ContinuousPhaseData :=
 423  let hnR : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn
 424  let hd : (0 : ℝ) < ↑n + 1 := by linarith
 425  let hgt1 : (1 : ℝ) < ↑n + 1 := by linarith
 426  let hr : 0 < qlf.radius / (↑n + 1) := div_pos qlf.radius_pos hd
 427  let hrw : qlf.radius / (↑n + 1) < qlf.radius :=
 428    div_lt_self qlf.radius_pos hgt1
 429  let rfp := regularFactorPhaseFromWitness qlf.toLocalMeromorphicWitness
 430    (qlf.radius / (↑n + 1)) hr hrw qlf.logDerivBound qlf.logDerivBound_pos
 431  { center := qlf.center
 432    radius := qlf.radius / (↑n + 1)
 433    radius_pos := hr
 434    phase := fun θ => (qlf.order : ℝ) * θ + rfp.phase θ
 435    phase_continuous := by
 436      exact (continuous_const.mul continuous_id).add rfp.phase_continuous
 437    charge := -qlf.order
 438    phase_winding := by
 439      simp only [add_sub_add_comm]
 440      have hw_pole : (qlf.order : ℝ) * (2 * π) - (qlf.order : ℝ) * 0 =
 441          -(2 * π * ((-qlf.order : ℤ) : ℝ)) := by
 442        simp [Int.cast_neg]; ring
 443      have hw_reg := rfp.toContinuousPhaseData.phase_winding
 444      rw [rfp.charge_zero] at hw_reg
 445      simp at hw_reg
 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) :