Foundation Winding Charges Cancelling Pair Zero Displacement

A step and its mirror

In the Recognition Science framework, a ledger (a discrete record of events) tracks a point moving on an integer lattice, one unit per tick along a single axis. A path is a list of such steps. The declaration cancelling_pair_zero_displacement proves a small, exact fact: if two consecutive steps are a plus step and a minus step along the same axis, in either order, then their combined displacement along that axis is zero. The proof is a direct computation on the definition of a step's displacement; it is a theorem in the machine-checked library of formal theorems, not a physical postulate.

The statement matters because it is the seed of a conservation law. The framework defines a winding number for a path as the net signed count of steps along a given axis: plus steps add one, minus steps subtract one, and a stay contributes nothing. A cancelling pair, a plus and a minus on the same axis, contributes zero to that count. The theorem insert_cancelling_preserves_winding extends this: inserting such a pair anywhere in a path leaves every winding number unchanged. Since the framework's variational dynamics updates a path one tick at a time, these local insertions and removals are exactly the allowed moves, so winding numbers are invariant under the dynamics. The cancelling pair is the elementary move that makes the conservation exact.

The theorem is deliberately narrow. It says nothing about which axis a step moves along, only that a plus and a minus on the same axis cancel. It does not claim that any two steps cancel, nor that a plus on one axis cancels a minus on another. It does not assert that the empty path is the only closed path; a square loop, for instance, is closed but is not a cancelling pair. The declaration is a lemma about the definition of displacement, not a statement about physics. Its role is to be the atomic fact that the framework later assembles into the claim that there are exactly D independent winding charges in D dimensions, and for D = 3, three such charges.

What the theorem changes is the picture of conservation. A conservation law in this account is not a separate axiom; it is a consequence of the combinatorics of steps. The cancelling pair is the reason a charge can be moved, deformed, or reordered along a path without changing its value. The framework's library proves the full chain: winding numbers are integers, they add under concatenation, they are invariant under local deformations, and in three dimensions they give three independent charges. The single cancelling pair is the load-bearing brick in that wall.

/-- A cancelling pair has zero total displacement along every axis. -/
theorem cancelling_pair_zero_displacement {D : ℕ} (s₁ s₂ : LatticeStep D)
    (h : is_cancelling_pair s₁ s₂) (axis : Fin D) :
    step_displacement s₁ axis + step_displacement s₂ axis = 0 := by
  rcases h with ⟨a, h₁, h₂⟩ | ⟨a, h₁, h₂⟩
  · subst h₁; subst h₂
    simp [step_displacement]
    split <;> simp
  · subst h₁; subst h₂
    simp [step_displacement]
    split <;> simp

/-- **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

/-- Winding number of a stay step is 0. -/
theorem winding_stay {D : ℕ} (axis : Fin D) :
    winding_number [LatticeStep.stay] axis = 0 := by
  simp [winding_number, step_displacement]

What this page does not claim

The theorem does not claim that any two steps cancel, only a plus and a minus on the same axis. It does not assert that the empty path is the only closed path. It does not by itself establish the number of independent charges in any dimension.

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: