winding_gives_three_charges
plain-language theorem explainer
In three dimensions the cardinality of the finite set with three elements equals the number of independent topological charges obtained from winding numbers on the integer lattice. Researchers deriving conservation laws from lattice-path topology in Recognition Science would cite this result to equate charge count with spatial dimension. The proof is a one-line simplification that unfolds the definition of independent_charge_count together with the standard cardinality of Fin 3.
Claim. In three spatial dimensions the cardinality of the finite set with three elements equals the number of independent topological charges arising from winding numbers on the lattice.
background
The module derives conservation laws from the combinatorics of lattice paths on ℤ^D. For each axis k the winding number of a path is the net signed displacement: w_k = (# of +k steps) − (# of −k steps). Local deformations preserve all winding numbers, so they are invariants of the variational dynamics. The upstream definition independent_charge_count D (from TopologicalConservation) returns 3 precisely when D = 3; the present theorem shows this count is forced by the lattice rather than imposed by fiat. Dimension is the natural-number type supplied by DimensionForcing, and Charge is the real-valued type from RSNativeUnits.
proof idea
One-line wrapper that applies the simp tactic to the pair independent_charge_count and Fintype.card_fin, reducing both sides to the numeral 3.
why it matters
The declaration supplies the missing derivation that the number of independent charges equals the spatial dimension D. It therefore feeds the parent claim in TopologicalConservation that independent_charge_count 3 = 3 and supports the framework landmark that all occurrences of the integer 3 (charges, colors, generations, axes) trace to dim(ℤ^3) = 3. The module doc-comment states explicitly that this count is a theorem about ℤ^D rather than a definition by fiat.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.