insert_cancelling_preserves_winding
plain-language theorem explainer
Inserting a cancelling pair of opposite steps along one axis into a lattice path leaves the winding number unchanged along every axis. Researchers deriving topological conservation from lattice paths cite this to justify invariance under local deformations. The proof applies additivity of winding numbers three times to isolate the inserted pair, invokes its zero net displacement, and finishes with arithmetic simplification.
Claim. Let $D$ be a natural number, $p_1,p_2$ lattice paths in dimension $D$, $s_1,s_2$ steps that form a cancelling pair, and $k$ an axis. Then the winding number of the path obtained by appending $s_1,s_2$ between $p_1$ and $p_2$ equals the winding number of the path $p_1$ appended with $p_2$, both taken along axis $k$.
background
A lattice path in dimension $D$ is a finite list of steps on the integer lattice, where each step is a plus or minus move along one coordinate axis or a stay. The winding number along axis $k$ is the net signed count of steps along that axis. The WindingCharges module derives conservation laws from these winding numbers by showing they are invariant under local deformations that insert or remove cancelling pairs. This supplies the topological mechanism left implicit in TopologicalConservation. The result rests on the upstream theorem that winding numbers add under path concatenation and on the lemma that any cancelling pair has zero total displacement along every axis.
proof idea
The term proof rewrites the winding number of the extended path via the additivity theorem applied three times, reducing the claim to equality of the original winding number plus the winding contribution of the inserted pair. It then calls the zero-displacement lemma on the cancelling pair to obtain a zero contribution along the chosen axis and concludes by omega arithmetic.
why it matters
This invariance under insertion of cancelling pairs is one of the four properties listed in the winding_charges_certificate theorem, which assembles integer quantization, additivity, topological protection, and independence of exactly $D$ charges. The certificate in turn grounds the derivation that conservation laws arise from lattice-path winding numbers. It directly supports the claim that variational dynamics preserves charges because the dynamics updates paths by local deformations. The result closes one link in the F-013 chain from lattice combinatorics to the $D=3$ independent charges of Recognition Science.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.