winding_additive
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.