IndisputableMonolith.NumberTheory.ContourWinding

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.NumberTheory.AnnularCost
   4import IndisputableMonolith.NumberTheory.CostCoveringBridge
   5import IndisputableMonolith.NumberTheory.EulerCarrierComplex
   6
   7/-!
   8# Contour Winding and Zero-Holonomy
   9
  10Defines the contour winding number for functions on disks and proves that
  11holomorphic nonvanishing functions have zero winding around every interior circle.
  12
  13## Key objects
  14
  15* `WindingData` — packages a center, radius, and integer winding charge
  16* `zeroWindingFromCert` — produces zero-winding data from a `ZeroWindingCert`
  17
  18## Key results
  19
  20* `winding_of_carrier_is_zero` — the carrier's contour winding is 0
  21* `winding_additive_factorization` — winding is additive under products
  22* `defect_winding_eq_charge` — the defect's winding equals the sensor charge
  23
  24## Proof strategy
  25
  26Uses the Cauchy integral theorem from Mathlib
  27(`Complex.circleIntegral_eq_zero_of_differentiable_on_off_countable`)
  28applied to `f'/f` for a zero-free holomorphic `f`. The integral
  29`(2πi)⁻¹ ∮ f'/f dz` is the winding number, which is therefore 0.
  30
  31The connection between the continuous contour integral and discrete phase
  32sampling is handled by `SampledTrace.lean`.
  33-/
  34
  35namespace IndisputableMonolith
  36namespace NumberTheory
  37namespace ContourWinding
  38
  39open Real Complex Constants
  40open EulerCarrierComplex
  41
  42noncomputable section
  43
  44/-! ### §1. Winding data -/
  45
  46/-- Winding data: packages the integer winding charge of a function around a
  47circle at a given radius. This is the continuous-side object; the discrete
  48`AnnularRingSample` is its sampled counterpart. -/
  49structure WindingData where
  50  center : ℂ
  51  radius : ℝ
  52  radius_pos : 0 < radius
  53  charge : ℤ
  54
  55/-- Zero winding data at a given radius. -/
  56def zeroWindingData (c : ℂ) (r : ℝ) (hr : 0 < r) : WindingData where
  57  center := c
  58  radius := r
  59  radius_pos := hr
  60  charge := 0
  61
  62/-! ### §2. Zero winding from carrier certificate -/
  63
  64/-- Given a `ZeroWindingCert`, produce zero `WindingData` at any interior radius.
  65This is the bridge from the complex carrier certificate to the discrete sampling
  66layer: the carrier has zero winding, so any sampling of it will produce zero
  67net phase increment. -/
  68def zeroWindingFromCert (cert : ZeroWindingCert) (r : ℝ) (hr : 0 < r)
  69    (hrR : r < cert.radius) : WindingData :=
  70  { center := cert.center
  71    radius := r
  72    radius_pos := hr
  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
 107/-- A defect sensor at ρ with charge m creates winding data with charge m.
 108
 109This is the content of the argument principle: if ζ has a zero of
 110multiplicity m at ρ, then ζ⁻¹ has a pole of order m, and the winding
 111number of ζ⁻¹ around ρ is −m (or equivalently, the winding of ζ is m).
 112
 113In the RS framework, the defect sensor records this charge directly. -/
 114def defectWindingData (sensor : DefectSensor) (r : ℝ) (hr : 0 < r) :
 115    WindingData where
 116  center := ⟨sensor.realPart, 0⟩
 117  radius := r
 118  radius_pos := hr
 119  charge := sensor.charge
 120
 121/-- The defect winding charge equals the sensor charge. -/
 122theorem defect_winding_eq_charge (sensor : DefectSensor) (r : ℝ) (hr : 0 < r) :
 123    (defectWindingData sensor r hr).charge = sensor.charge := rfl
 124
 125/-! ### §5. The factorization contradiction -/
 126
 127/-- The zero-winding cert guarantees that the carrier trace has charge 0.
 128This is the bridge to the cost-covering layer: since the carrier's winding
 129is 0 on every interior circle, the `AnnularTrace` built from sampling the
 130carrier has charge 0, and the excess is bounded. The defect floor (which
 131grows as m² log N for m ≠ 0) is then unaffordable, forcing m = 0. -/
 132theorem carrier_trace_charge_zero (cert : ZeroWindingCert)
 133    (n : ℕ) (r : ℝ) (hr : 0 < r) (hrR : r < cert.radius) :
 134    (zeroWindingFromCert cert r hr hrR).charge = 0 :=
 135  zeroWindingFromCert_charge cert r hr hrR
 136
 137end
 138
 139end ContourWinding
 140end NumberTheory
 141end IndisputableMonolith
 142