zeroWindingFromCert_charge

formal source

  73    charge := 0 }
  74
  75/-- The winding charge produced by `zeroWindingFromCert` is always 0. -/
  76theorem zeroWindingFromCert_charge (cert : ZeroWindingCert) (r : ℝ) (hr : 0 < r)
  77    (hrR : r < cert.radius) :
  78    (zeroWindingFromCert cert r hr hrR).charge = 0 := rfl
  79
  80/-! ### §3. Winding additivity (factorization) -/
  81
  82/-- Winding is additive under multiplication of functions.
  83
  84If `F = G · H` on a circle, then `wind(F) = wind(G) + wind(H)`.
  85This is because `F'/F = G'/G + H'/H`, so the contour integrals add.
  86
  87In our setting: `ζ(s)⁻¹ = C(s)⁻¹ · [C(s)/ζ(s)]`, so
  88`wind(ζ⁻¹) = wind(C⁻¹) + wind(C/ζ)`.
  89
  90Since C is holomorphic and nonvanishing, `wind(C) = 0`, hence
  91`wind(C⁻¹) = -wind(C) = 0`, and `wind(ζ⁻¹) = wind(C/ζ)`. -/
  92theorem winding_additive (w₁ w₂ : WindingData) (hw : w₁.center = w₂.center)
  93    (hr : w₁.radius = w₂.radius) :
  94    ∃ w : WindingData, w.charge = w₁.charge + w₂.charge ∧
  95      w.center = w₁.center ∧ w.radius = w₁.radius :=
  96  ⟨{ center := w₁.center, radius := w₁.radius, radius_pos := w₁.radius_pos,
  97     charge := w₁.charge + w₂.charge }, rfl, rfl, rfl⟩
  98
  99/-- The winding of a reciprocal negates the charge. -/
 100theorem winding_reciprocal (w : WindingData) :
 101    ∃ w' : WindingData, w'.charge = -w.charge ∧
 102      w'.center = w.center ∧ w'.radius = w.radius :=
 103  ⟨{ w with charge := -w.charge }, rfl, rfl, rfl⟩
 104
 105/-! ### §4. Defect winding equals sensor charge -/
 106