zetaDerivedPhaseFamily

formal source

 345on circles of decreasing radius `r₀/(n+1)` around the factorization center.
 346The charge on each circle equals `-order`, which for `zetaReciprocal` at a
 347zero of ζ with multiplicity `m` gives charge `m = sensor.charge`. -/
 348noncomputable def zetaDerivedPhaseFamily
 349    (sensor : DefectSensor)
 350    (qlf : QuantitativeLocalFactorization)
 351    (horder : qlf.order = -sensor.charge) : DefectPhaseFamily where
 352  sensor := sensor
 353  witnessRadius := qlf.radius
 354  witnessRadius_pos := qlf.radius_pos
 355  phaseAtLevel n hn := zetaDerivedPhaseData qlf n hn
 356  charge_uniform n hn := by
 357    have := zetaDerivedPhaseData_charge qlf n hn
 358    rw [this, horder, neg_neg]
 359
 360@[simp] theorem zetaDerivedPhaseFamily_sensor
 361    (sensor : DefectSensor) (qlf : QuantitativeLocalFactorization)
 362    (horder : qlf.order = -sensor.charge) :
 363    (zetaDerivedPhaseFamily sensor qlf horder).sensor = sensor := rfl
 364
 365/-- The current `zetaDerivedPhaseFamily` carries a zero-perturbation witness:
 366its sampled increments are exactly the pure winding increments. -/
 367noncomputable def zetaDerivedPhasePerturbationWitness
 368    (sensor : DefectSensor)
 369    (qlf : QuantitativeLocalFactorization)
 370    (horder : qlf.order = -sensor.charge) :
 371    DefectPhasePerturbationWitness (zetaDerivedPhaseFamily sensor qlf horder) where
 372  epsilon := fun _ _ _ => 0
 373  increment_eq := by
 374    intro n hn j
 375    have hnR : (8 * (n : ℝ)) ≠ 0 := by
 376      have hnR' : 0 < (n : ℝ) := by
 377        exact_mod_cast hn
 378      nlinarith