IndisputableMonolith.Foundation.WindingCharges
Foundation.WindingCharges defines lattice steps and winding numbers on ℤ^D. These objects formalize topological charges arising from path linking rather than Noether symmetries. The module supplies the discrete structures needed for conservation laws in D=3 and is imported by the Yang-Mills mass-gap unification.
claimA lattice step on $\mathbb{Z}^D$ is a map that changes exactly one coordinate by $\pm 1$ or leaves the point fixed. A lattice path is a finite sequence of such steps. The winding number of a closed path around a linking cycle counts the signed crossings in each coordinate plane.
background
The module sits inside the Foundation layer and imports DimensionForcing (D=3 forced), TopologicalConservation (charges from linking), VariationalDynamics (ledger update rule), InitialCondition (low-entropy start), and QuarkColors (N_c=3). Its central definitions are LatticeStep (a single move or stay on the integer lattice) and LatticePath together with the winding_number function that extracts integer charges from closed paths. These objects realize the claim that conservation arises from topology in three dimensions rather than continuous symmetry.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the discrete topological objects required by TopologicalConservation and is imported directly by Unification.YangMillsMassGap. It therefore contributes the lattice-level charge definitions that allow the J-cost functional to produce the mass gap without invoking gauge symmetry.
scope and limits
- Does not derive D=3 or the linking argument.
- Does not prove any conservation theorem.
- Does not contain the mass-gap statement.
- Does not address continuous symmetries or Noether's theorem.
used by (1)
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