empty_is_closed
plain-language theorem explainer
Empty lattice paths on Z^D have vanishing winding numbers along every axis and therefore satisfy the closed-path condition. Researchers deriving topological conservation from lattice combinatorics in Recognition Science cite this base case when establishing invariance under variational updates. The argument reduces directly to the zero-winding theorem for the empty sequence applied axis by axis.
Claim. For any natural number $D$, the empty sequence on the integer lattice in $D$ dimensions has winding number zero along each coordinate axis $k=1,2,3$, hence its total displacement vanishes in every direction.
background
The Winding Charges module supplies the topological mechanism for conservation laws left implicit in TopologicalConservation. Lattice paths are finite sequences of axis-aligned steps on Z^D; the winding number along axis k counts net signed steps along that axis. A path is closed precisely when every winding number is zero, which is preserved under the local deformations that implement variational dynamics.
proof idea
The proof is a one-line term-mode wrapper. It applies the upstream theorem that the empty path has winding number zero, instantiated at an arbitrary axis k, to discharge the universal quantifier in the closed-path definition.
why it matters
This supplies the base case for the closed-path predicate inside the F-013 derivation of exactly D independent topological charges from lattice-path combinatorics. When D=3 the construction yields the three independent winding numbers that realize the spatial dimension forced by the eight-tick octave. The result sits at the foundation of the winding-charge account of conservation and has no listed downstream uses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.