winding_charge
winding_charge assigns to each lattice path in D dimensions the integer winding number along a chosen axis k. Researchers deriving topological conservation from lattice combinatorics cite this when establishing that the charges are independent and determine the full winding vector. The definition is realized as a one-line wrapper delegating directly to the winding_number computation on paths.
claimLet $D$ be a natural number and $k$ an index in the set with $D$ elements. For a lattice path $p$ consisting of unit steps on the integer lattice in $D$ dimensions, the winding charge along axis $k$ is the net signed displacement $w_k(p)$ given by the difference between positive and negative steps along that axis.
background
Lattice paths are finite sequences of steps on the integer lattice in dimension $D$, where each step displaces the position by one unit along a single coordinate axis or leaves it unchanged. The winding number along axis $k$ extracts the net crossings: the count of positive steps minus the count of negative steps along that axis. This module supplies the explicit mechanism for topological charges that TopologicalConservation left implicit, showing that local deformations of paths preserve all winding numbers because the variational dynamics update one tick at a time via such deformations.
proof idea
The definition is a one-line wrapper that applies the winding_number function to the given path and axis index $k$.
why it matters in Recognition Science
This definition is invoked by the downstream theorems D_independent_charges and three_independent_winding_charges, which prove there are exactly $D$ independent winding-number charges and the special case of three for $D=3$. It fills the combinatorial gap in the derivation of conservation laws from lattice paths, connecting directly to the framework requirement of $D=3$ spatial dimensions and the eight-tick octave structure. The construction shows the charges arise from path combinatorics without extra postulates.
scope and limits
- Does not prove invariance of the charges under the full variational dynamics.
- Does not evaluate winding numbers on any concrete path.
- Does not identify the charges with physical particles or fields.
- Does not derive the value of $D$ from the forcing chain.
formal statement (Lean)
239def winding_charge (D : ℕ) (k : Fin D) : LatticePath D → ℤ :=
proof body
Definition body.
240 fun p => winding_number p k
241
242/-- **THEOREM (D Independent Charges)**:
243 There are exactly D independent winding-number charges.
244
245 "Independent" means:
246 1. Each charge is a distinct ℤ-valued function (they disagree on some path)
247 2. No charge is a ℤ-linear combination of the others
248 3. Together they determine the full winding-number vector
249
250 Proof: For distinct axes j ≠ k, the path [plus k] has
251 winding_charge k = 1 but winding_charge j = 0. -/