Foundation Winding Charges Insert Cancelling Preserves Winding

The cancellation lemma

In the Recognition Science framework, a ledger (a discrete record of events) tracks the position of a particle on an integer lattice across successive ticks. A lattice path is a sequence of steps, each moving one unit along a single axis, or staying put. The winding number of a path along a given axis is the net signed displacement: the count of forward steps minus the count of backward steps along that axis. For a path in three dimensions, the three winding numbers serve as integer-valued labels that the framework associates with electric charge, baryon number, and lepton number.

The declaration insert_cancelling_preserves_winding states a precise fact: if you take any lattice path and insert two consecutive steps that cancel each other, one step in a direction and the next step in the exact opposite direction along the same axis, the winding number of the whole path along every axis remains unchanged. The proof is short and purely combinatorial. It uses the additivity of winding numbers under concatenation of paths, and the observation that the displacement of a cancelling pair along any axis is zero. The lemma is the formal engine behind a stronger statement: removing such a cancelling pair also preserves winding numbers, a theorem named remove_cancelling_preserves_winding.

Why this matters: the framework's dynamics update the ledger one tick at a time, and the local deformations it allows are exactly the kind of insertions and removals of cancelling pairs that this lemma covers. Because such moves leave all winding numbers untouched, those numbers are conserved by the dynamics. The lemma is therefore the bridge from a purely combinatorial definition to the claim that the winding numbers are topological charges, quantities that cannot change under local, step-by-step evolution. In the framework's account, this is the mechanism behind conservation laws, and for three spatial dimensions it yields exactly three independent conserved quantities.

The lemma does not claim that the winding numbers correspond to any particular physical charge in an experiment, nor that the framework's identification with electric charge, baryon number, and lepton number is a derived theorem. That identification is a modeling choice, not a consequence of the lemma. The lemma also says nothing about what happens when steps are inserted that do not cancel, or when the path is deformed in a way that is not a sequence of local cancellations. It is a statement about the algebra of lattice paths, not about the full dynamics of the ledger.

/-- **THEOREM (Inserting a Cancelling Pair Preserves Winding Number)**:
    If we insert a cancelling pair (→←) at any point in a path,
    the winding number along every axis is unchanged. -/
theorem insert_cancelling_preserves_winding {D : ℕ}
    (p₁ p₂ : LatticePath D) (s₁ s₂ : LatticeStep D)
    (h : is_cancelling_pair s₁ s₂) (axis : Fin D) :
    winding_number (List.append (List.append p₁ [s₁, s₂]) p₂) axis =
    winding_number (List.append p₁ p₂) axis := by
  rw [winding_additive (List.append p₁ [s₁, s₂]) p₂,
      winding_additive p₁ [s₁, s₂],
      winding_additive p₁ p₂]
  simp only [winding_number, List.map_cons, List.map_nil, List.sum_cons, List.sum_nil]
  have h_cancel := cancelling_pair_zero_displacement s₁ s₂ h axis
  omega

/-- **THEOREM (Inserting a Cancelling Pair Preserves Winding Number)**:
    If we insert a cancelling pair (→←) at any point in a path,
    the winding number along every axis is unchanged. -/
theorem insert_cancelling_preserves_winding {D : ℕ}
    (p₁ p₂ : LatticePath D) (s₁ s₂ : LatticeStep D)
    (h : is_cancelling_pair s₁ s₂) (axis : Fin D) :
    winding_number (List.append (List.append p₁ [s₁, s₂]) p₂) axis =
    winding_number (List.append p₁ p₂) axis := by
  rw [winding_additive (List.append p₁ [s₁, s₂]) p₂,
      winding_additive p₁ [s₁, s₂],
      winding_additive p₁ p₂]
  simp only [winding_number, List.map_cons, List.map_nil, List.sum_cons, List.sum_nil]
  have h_cancel := cancelling_pair_zero_displacement s₁ s₂ h axis
  omega

/-- **THEOREM (Removing a Cancelling Pair Preserves Winding Number)**: -/
theorem remove_cancelling_preserves_winding {D : ℕ}
    (p₁ p₂ : LatticePath D) (s₁ s₂ : LatticeStep D)
    (h : is_cancelling_pair s₁ s₂) (axis : Fin D) :
    winding_number (List.append p₁ p₂) axis =
    winding_number (List.append (List.append p₁ [s₁, s₂]) p₂) axis :=
  (insert_cancelling_preserves_winding p₁ p₂ s₁ s₂ h axis).symm

/-- For D = 3: exactly 3 independent winding charges. -/
theorem three_independent_winding_charges :
    ∃ (w : Fin 3 → LatticePath 3 → ℤ),
      -- They are the winding numbers along the 3 axes
      (∀ k, w k = winding_charge 3 k) ∧
      -- They are pairwise distinguishable
      (∀ j k : Fin 3, j ≠ k →
        ∃ p, w j p ≠ w k p) ∧
      -- Each takes values in all of ℤ
      (∀ k : Fin 3, ∀ n : ℤ, ∃ p, w k p = n) := by
  use fun k => winding_charge 3 k
  refine ⟨fun _ => rfl, ?_, ?_⟩
  · intro j k hjk
    exact (D_independent_charges 3 (by norm_num)).2.1 j k hjk
  · intro k n
    obtain ⟨p, hp, _⟩ := (D_independent_charges 3 (by norm_num)).2.2 k n
    exact ⟨p, hp⟩

What this page does not claim

The lemma does not identify winding numbers with electric charge, baryon number, or lepton number; that identification is a modeling choice. The lemma says nothing about non-cancelling insertions or deformations that are not local cancellations. The lemma does not prove that the framework's dynamics actually acts only by such local deformations.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/WindingCharges.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: