module module high

`IndisputableMonolith.Foundation.WindingCharges`

WindingCharges defines lattice steps on the integer lattice in D dimensions together with winding numbers and their additive properties. These objects model topological charges that arise from linking rather than continuous symmetries. The module is referenced in derivations of quark color and the Yang-Mills mass gap. Content consists solely of definitions and elementary lemmas.

claimA lattice step on the $D$-dimensional lattice is a vector $s$ in $Z^D$ with at most one nonzero coordinate equal to $+1$ or $-1$ (or the zero vector). Winding number is the integer invariant associated to closed lattice paths built from such steps.

background

The module sits inside the Recognition Science foundation layer after DimensionForcing has established $D=3$ and TopologicalConservation has shown that conservation laws follow from linking numbers on the lattice. VariationalDynamics supplies the update rule for the recognition ledger while QuarkColors and InitialCondition provide the surrounding context for color charge and low-entropy initial data. LatticeStep is the primitive displacement; LatticePath is a finite sequence of such steps; winding_number counts net encirclements.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The definitions supply the discrete topological charges required by the Yang-Mills mass gap argument in Unification.YangMillsMassGap. They close the link between the J-cost functional and the emergence of $N_c=3$ color charge from the same lattice structure that forces $D=3$. The module therefore completes the foundation chain from variational dynamics to topological conservation.

scope and limits

Does not treat continuous manifolds or differential forms.
Does not derive numerical values for the mass gap.
Does not incorporate gauge field operators or path integrals.
Does not prove that winding numbers are the only possible charges.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Unification.YangMillsMassGap module_import

depends on (5)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.DimensionForcing module_import
IndisputableMonolith.Foundation.InitialCondition module_import
IndisputableMonolith.Foundation.QuarkColors module_import
IndisputableMonolith.Foundation.TopologicalConservation module_import
IndisputableMonolith.Foundation.VariationalDynamics module_import

declarations in this module (35)

inductive LatticeStep L84
def LatticePath L91
def step_displacement L95
def winding_number L107
theorem winding_empty L111
theorem winding_plus_self L115
theorem winding_minus_self L120
theorem winding_orthogonal L125
theorem winding_stay L130
theorem winding_additive L141
theorem winding_cons L147
def is_cancelling_pair L159
theorem cancelling_pair_zero_displacement L164
theorem insert_cancelling_preserves_winding L178
theorem remove_cancelling_preserves_winding L191
theorem winding_numbers_independent L205
theorem winding_surjective_single L212
def winding_charge L239
theorem D_independent_charges L252
theorem three_independent_winding_charges L271
structure WindingLabel L298
def winding_label_is_topological L303
theorem winding_gives_three_charges L314
theorem charge_count_is_dimension L326
theorem all_threes_unified L330
def is_closed L347
theorem empty_is_closed L351
theorem cancelling_pair_closed L355
def square_loop L374
theorem square_loop_closed L377
theorem square_loop_trivial_when_equal L386
def independent_loop_count L402
theorem three_independent_loops_D3 L404
theorem loops_eq_face_pairs_D3 L411
theorem winding_charges_certificate L430