charge_count_is_dimension
plain-language theorem explainer
The declaration establishes that the number of independent winding charges on the lattice equals the spatial dimension D. Researchers deriving conservation laws from topological winding numbers in discrete spacetime models would cite it to equate charge count with dimension without fiat definitions. The proof is a one-line application of the standard cardinality fact for the finite set with D elements.
Claim. For any natural number $D$, the cardinality of the finite set with $D$ elements equals $D$.
background
In the WindingCharges module, world-lines on the lattice are sequences of positions in $Z^D$, with a winding number $w_k$ for each axis $k$ defined as the net signed displacement along that axis. These numbers are preserved under local deformations of paths and under the variational dynamics that updates one tick at a time. The module shows there are exactly $D$ independent charges because each axis contributes one independent winding number, with different axes yielding independent quantities.
proof idea
The proof is a one-line wrapper that applies the library fact Fintype.card_fin D.
why it matters
This result grounds the equality between independent charge count and spatial dimension, directly supporting the module claim that for D=3 the three charges align with three axes, three face-pairs, three colors, and three generations. It fills the combinatorial gap left by the case-based definition in TopologicalConservation and connects to the framework landmark that D=3 spatial dimensions is forced at step T8 of the unified forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.