WindingLabel
plain-language theorem explainer
WindingLabel equips an N-entry ledger with an integer-valued map from configurations to integers that can become a topological charge once invariance under variational steps is shown. Researchers deriving conservation laws from lattice path winding numbers on Z^D would cite this structure when building explicit charge assignments. The declaration is a pure structure definition that introduces the label field with no proof obligations or computational content.
Claim. A winding label on an $N$-entry ledger is a function $w : C_N → ℤ$, where $C_N$ denotes the space of configurations consisting of $N$ positive real entries.
background
Configurations are structures of $N$ positive real entries, as introduced in InitialCondition.Configuration. TopologicalCharge from TopologicalConservation is an integer-valued function on configurations that is invariant under IsVariationalSuccessor steps. The WindingCharges module supplies the missing mechanism: conservation arises because winding numbers of lattice paths on Z^D are preserved by local deformations that the variational dynamics employs. Each axis contributes one independent winding number, yielding exactly D independent charges.
proof idea
This is a structure definition that directly records the label field. No lemmas or tactics are applied; the declaration packages the map for later use in winding_label_is_topological.
why it matters
The structure supplies the concrete carrier for winding-based charges that feeds winding_label_is_topological, which constructs a TopologicalCharge instance. It realizes the F-013 derivation of independent_charge_count from lattice combinatorics and connects to the D=3 result in the unified forcing chain. The definition closes the gap between the abstract TopologicalCharge interface and explicit path-winding assignments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.