winding_additive
Lattice path winding numbers add under concatenation: the net signed displacement along any axis of a joined path equals the sum of the displacements from each segment. Researchers deriving topological conservation laws from lattice world-lines cite this to establish charge additivity. The proof is a one-line term simplification that unfolds the sum definition and distributes over list append.
claimLet $p_1,p_2$ be finite sequences of steps on the integer lattice in $D$ dimensions and fix an axis $k$. Let $w_k(p)$ denote the net signed displacement of path $p$ along axis $k$. Then $w_k(p_1++p_2)=w_k(p_1)+w_k(p_2)$.
background
The WindingCharges module supplies the topological mechanism for conservation by treating world-lines as lattice paths on Z^D. LatticePath D is the type of finite lists of LatticeStep D. The winding_number of a path along axis k is defined as the sum of the individual step displacements along k, where each step contributes +1, -1, or 0.
proof idea
The term proof applies simp to the definition of winding_number together with List.map_append and List.sum_append. This replaces the sum over the concatenated list by the sum of the two separate sums.
why it matters in Recognition Science
Additivity supplies the second clause of the winding_charges_certificate, which assembles the integer, additive, and invariant properties of topological charges. It is invoked directly by insert_cancelling_preserves_winding and by winding_surjective_single. In the Recognition framework this step justifies the existence of exactly D independent charges, with the D=3 case recovered from the lattice combinatorics.
scope and limits
- Does not establish invariance of winding numbers under local deformations of paths.
- Does not prove independence of windings along distinct axes.
- Does not derive the specific value D=3 from the forcing chain.
- Does not connect to mass formulas or the phi-ladder.
formal statement (Lean)
141theorem winding_additive {D : ℕ} (p₁ p₂ : LatticePath D) (axis : Fin D) :
142 winding_number (List.append p₁ p₂) axis =
143 winding_number p₁ axis + winding_number p₂ axis := by
proof body
Term-mode proof.
144 simp [winding_number, List.map_append, List.sum_append]
145
146/-- Prepending a step adds its displacement. -/