zeroWindingFromCert_charge
zeroWindingFromCert_charge shows that the integer charge extracted from any zero-winding certificate is identically zero inside the certified radius. Researchers modeling holomorphic carriers in the Recognition Science contour analysis cite it to separate carrier and defect contributions before applying cost bounds. The proof is a one-line reflexivity that unfolds the definition of zeroWindingFromCert.
claimLet cert be a zero-winding certificate with radius R. For any real r satisfying 0 < r < R, the charge component of the winding data returned by zeroWindingFromCert(cert, r) equals zero.
background
The ContourWinding module defines WindingData as a record containing a center, radius, and integer winding charge. zeroWindingFromCert constructs such data from a ZeroWindingCert that certifies a function is holomorphic and nonvanishing inside the disk. The module's local setting is zero-holonomy: holomorphic nonvanishing functions have vanishing contour winding around every interior circle, proved via the Cauchy integral theorem applied to f'/f.
proof idea
The declaration is a term-mode proof consisting of a single reflexivity. It holds because zeroWindingFromCert is defined to return data whose charge field is exactly zero.
why it matters in Recognition Science
The result is invoked by carrier_trace_charge_zero to establish that the sampled carrier trace carries zero charge. This zero-charge property bounds the annular excess cost and forces the defect index m to vanish in the factorization argument. It supplies the zero-holonomy step required for the additive winding decomposition that links to the Recognition Composition Law and the J-cost functional equation.
scope and limits
- Does not compute winding numbers for functions possessing zeros or poles inside the contour.
- Does not extend the zero-charge guarantee beyond the radius certified by the input certificate.
- Does not derive explicit numerical values for the winding charge of defect terms.
- Does not address the connection to the phi-ladder or mass formulas.
Lean usage
theorem carrier_trace_charge_zero (cert : ZeroWindingCert) (n : ℕ) (r : ℝ) (hr : 0 < r) (hrR : r < cert.radius) : (zeroWindingFromCert cert r hr hrR).charge = 0 := zeroWindingFromCert_charge cert r hr hrRformal statement (Lean)
76theorem zeroWindingFromCert_charge (cert : ZeroWindingCert) (r : ℝ) (hr : 0 < r)
77 (hrR : r < cert.radius) :
78 (zeroWindingFromCert cert r hr hrR).charge = 0 := rfl
proof body
Term-mode proof.
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/ζ)`. -/