is_closed
plain-language theorem explainer
A lattice path on the integer lattice in D dimensions is closed when its net signed displacement vanishes on every coordinate axis. Researchers deriving topological conservation from lattice world-lines would cite this predicate to classify charge-neutral loops. The definition is a direct universal quantification over the winding number along each axis.
Claim. A finite sequence of steps on the D-dimensional integer lattice is closed if the net signed displacement along each of the D axes is zero.
background
The Winding Charges module derives conservation laws from the combinatorics of lattice paths on the integer lattice. A lattice path is a finite list of steps, each advancing or retreating along one axis. The winding number along an axis sums the signed displacements of those steps, yielding an integer that counts net crossings in that direction.
proof idea
The definition directly equates closedness to the condition that the winding number vanishes on all axes. It applies the winding number summation to each coordinate in turn.
why it matters
This predicate supplies the core property used to prove that empty paths, cancelling pairs, and square loops carry zero net charge. It fills the mechanism left implicit in the topological conservation development, showing that exactly D independent winding numbers exist and remain invariant under local deformations. In the Recognition framework this supports the emergence of three conserved quantities when D equals three.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.