IndisputableMonolith.Foundation.WindingCharges
Defines lattice steps and paths on ℤ^D and the integer winding number of a path, with elementary additivity and cancellation lemmas. Supplies the discrete topological charge used when RS treats conservation as linking rather than Noether symmetry. Downstream mass and Yang–Mills modules import this as the geometric source of torsion and gap structure. The development is definitional plus short inductive identities on path concatenation.
claimOn the integer lattice $\mathbb{Z}^D$, a lattice step is a move of $+1$ or $-1$ along a single coordinate axis, or a stay. A lattice path is a finite sequence of steps. The winding number of a path is the net integer displacement obtained by summing signed steps; it is additive under concatenation, vanishes on the empty path and on pure stays, and cancels on opposite steps along the same axis.
background
Recognition Science forces spatial dimension $D = 3$ (DimensionForcing, T8) and then argues that conservation laws come from topology—linking in three dimensions—rather than continuous symmetries (TopologicalConservation). That story needs a concrete discrete charge on the ledger lattice before one can talk about linking, colour, or generation torsion.
This module introduces that charge. A single step on $\mathbb{Z}^D$ moves $\pm 1$ along one axis or stays put. Paths are finite sequences of steps; the winding number is the net signed displacement. Sibling lemmas record the elementary calculus: empty path and stays contribute zero, opposite steps on the same axis cancel, orthogonal steps do not interfere, and winding is additive under concatenation.
The surrounding foundation stack (initial condition, variational ledger update, quark colours) is imported so winding can sit inside the same $D$-forced, ledger-driven setting rather than as an ad hoc topological add-on.
proof idea
This is primarily a definition module. LatticeStep and LatticePath fix the discrete geometry; step_displacement and winding_number turn a path into an integer net charge. The named lemmas (winding_empty, winding_stay, winding_plus_self, winding_minus_self, winding_orthogonal, winding_additive, winding_cons, is_cancelling_pair) are short inductive or case-split identities on path structure: they unfold the recursive definition of winding under cons and verify cancellation and axis-independence. No deep analytic input is required beyond integer arithmetic and the forced ambient dimension from upstream.
why it matters in Recognition Science
Winding is the discrete stand-in for topological charge once RS has replaced Noether conservation by linking in $D = 3$. GenerationTorsionBridge and TorsionForcing import the module to derive the charged-generation torsion set ${0, 11, 17}$ from $Q_3$ cube geometry, the eight-tick cycle, and the $\varphi$-ladder through the Recognition Composition Law. YangMillsMassGap uses the same geometric charge language when it claims a mass gap from the $J$-cost alone (registry QG-005). Without a formal winding calculus, those later uniqueness and gap arguments would have no lattice-level charge to project or cancel.
scope and limits
- Does not prove $D = 3$; that is assumed from DimensionForcing.
- Does not derive linking invariants or Gauss linking numbers in continuum $\mathbb{R}^3$.
- Does not compute generation torsion $\{0,11,17\}$; downstream mass modules do.
- Does not address continuous gauge fields or continuum Yang–Mills dynamics.
- Does not claim Noether charges; conservation here is purely topological/winding.
used by (3)
depends on (5)
declarations in this module (35)
-
inductive
LatticeStep -
def
LatticePath -
def
step_displacement -
def
winding_number -
theorem
winding_empty -
theorem
winding_plus_self -
theorem
winding_minus_self -
theorem
winding_orthogonal -
theorem
winding_stay -
theorem
winding_additive -
theorem
winding_cons -
def
is_cancelling_pair -
theorem
cancelling_pair_zero_displacement -
theorem
insert_cancelling_preserves_winding -
theorem
remove_cancelling_preserves_winding -
theorem
winding_numbers_independent -
theorem
winding_surjective_single -
def
winding_charge -
theorem
D_independent_charges -
theorem
three_independent_winding_charges -
structure
WindingLabel -
def
winding_label_is_topological -
theorem
winding_gives_three_charges -
theorem
charge_count_is_dimension -
theorem
all_threes_unified -
def
is_closed -
theorem
empty_is_closed -
theorem
cancelling_pair_closed -
def
square_loop -
theorem
square_loop_closed -
theorem
square_loop_trivial_when_equal -
def
independent_loop_count -
theorem
three_independent_loops_D3 -
theorem
loops_eq_face_pairs_D3 -
theorem
winding_charges_certificate