defect_winding_eq_charge
plain-language theorem explainer
The charge of the winding data built from a defect sensor on a circle of positive radius equals the sensor's intrinsic charge. Number theorists working on contour integrals and holonomy in Recognition Science cite this to equate discrete defect charges with continuous winding numbers. The equality holds by direct reflexivity on the definition of the winding data constructor.
Claim. Let $S$ be a defect sensor and let $r > 0$. The charge component of the winding data constructed from $S$ at radius $r$ equals the charge of $S$.
background
The Contour Winding module defines WindingData as a package containing a center, radius, and integer winding charge. It introduces defectWindingData to build such data from a DefectSensor, and zeroWindingFromCert to produce zero-winding data from a ZeroWindingCert. The local setting uses the Cauchy integral theorem on $f'/f$ for zero-free holomorphic functions to obtain zero winding on interior circles, with the discrete-to-continuous link handled via sampled traces.
proof idea
The proof is a one-line term that applies reflexivity directly to the definition of defectWindingData.
why it matters
This result supplies the direct identification of winding charge with sensor charge, closing the link needed for the factorization contradiction section that follows. It supports the module's zero-holonomy theorems and feeds the cost-covering bridge by ensuring that zero-winding carriers produce zero excess charge. The equality anchors the defect functional (equal to J on positive arguments) within the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.