 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

papers checked against this theorem

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