winding_additive
plain-language theorem explainer
Winding charges add when two WindingData records share the same center and radius. Researchers deriving conservation laws from contour integrals or lattice paths in Recognition Science cite this for charge additivity. The proof is a direct term construction that assembles a fresh WindingData record with the summed charge field and reflexivity proofs for the shared center and radius.
Claim. Let $w_1$ and $w_2$ be winding data (each a triple of complex center, positive real radius, and integer charge) satisfying $w_1.center = w_2.center$ and $w_1.radius = w_2.radius$. Then there exists winding data $w$ such that the charge of $w$ equals the sum of the charges of $w_1$ and $w_2$, while $w$ retains the same center and radius.
background
WindingData packages a complex center, positive radius, and integer charge; it is the continuous object whose sampled counterpart is the annular ring trace. The ContourWinding module uses the Cauchy integral theorem on $f'/f$ to show that holomorphic nonvanishing functions have zero winding around interior circles. The doc comment notes that winding is additive under function multiplication because the logarithmic derivative splits, so the contour integrals add.
proof idea
The proof is a one-line term that builds the record {center := w₁.center, radius := w₁.radius, radius_pos := w₁.radius_pos, charge := w₁.charge + w₂.charge} and supplies rfl for each equality.
why it matters
This supplies the additivity step inside the winding charges certificate, which lists integer quantization, additivity under concatenation, invariance under cancelling pairs, and independence across dimensions. It feeds insert_cancelling_preserves_winding and winding_surjective_single in the WindingCharges module. The result closes the structural half of the contour-to-lattice bridge that supports topological protection of charges in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.