winding_additive
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove that the winding number equals the contour integral of f'/f.
- Does not apply when centers or radii differ.
- Does not establish zero winding for holomorphic functions.
- Does not reference the phi-ladder, J-cost, or forcing chain.
formal statement (Lean)
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 :=
proof body
Term-mode proof.
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. -/