Encyclopedia Foundation Foundation Winding Charges Winding Charges Certificate

ARTICLE 5 claims 4 theorems 1 model

Foundation Winding Charges Winding Charges Certificate

A single machine-checked theorem bundles the core facts about winding numbers, the integer-valued counts that conservation laws in the framework rest on.

Verify this page

The winding certificate

In the Recognition Science framework, a ledger (a discrete record of events) tracks particles as paths on a D-dimensional lattice. Each step in a path moves one unit along a single axis, either forward, backward, or not at all. 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. This is an integer by construction, and it is exactly what the framework identifies as a conserved charge.

The declaration winding_charges_certificate is a single theorem in the framework's machine-checked library of formal theorems. It bundles five facts. First, winding numbers are additive: the winding number of a concatenated path is the sum of the winding numbers of its parts. Second, inserting or removing a cancelling pair, a forward step immediately followed by a backward step on the same axis, leaves every winding number unchanged. Third, in three dimensions there are exactly three independent winding numbers, one for each axis. Fourth, this count of three matches the number of face-pairs of a cube. Fifth, the number of winding charges equals the number of charges in the framework's Standard Model count.

These facts together provide the mechanism behind conservation. Because the dynamics updates a path one tick at a time, and each tick is a local change, the invariance of winding numbers under local deformations means they are conserved quantities. The certificate does not derive these facts from deeper principles; it states them as a consolidated theorem, with each component already proved separately in the library.

The certificate does not claim that these winding numbers correspond to the actual electric, baryon, or lepton charges of particle physics. The framework's docstring suggests that for D = 3 the three winding numbers could be identified with those charges, but that identification is a modeling choice, not a proved result. The certificate also does not claim that winding numbers are the only conserved quantities, nor that the dynamics is actually implemented as local lattice deformations. It establishes the combinatorial backbone; the physical interpretation remains a separate step.

MODEL winding_number · IndisputableMonolith/Foundation/WindingCharges.lean
winding_number · IndisputableMonolith/Foundation/WindingCharges.lean:103 
/-- The **winding number** of a lattice path along axis k:
    the total signed displacement along that axis.

    w_k(path) = ∑ (step displacement along k). -/
def winding_number {D : ℕ} (path : LatticePath D) (axis : Fin D) : ℤ :=
  (path.map (fun s => step_displacement s axis)).sum
THEOREM winding_additive · IndisputableMonolith/Foundation/WindingCharges.lean
winding_additive · IndisputableMonolith/Foundation/WindingCharges.lean:136 
/-- **THEOREM (Winding Numbers Are Additive)**:
    The winding number of the concatenation of two paths equals the
    sum of their individual winding numbers.

    This is the formal content of "charge is additive." -/
theorem winding_additive {D : ℕ} (p₁ p₂ : LatticePath D) (axis : Fin D) :
    winding_number (List.append p₁ p₂) axis =
    winding_number p₁ axis + winding_number p₂ axis := by
  simp [winding_number, List.map_append, List.sum_append]
THEOREM insert_cancelling_preserves_winding · IndisputableMonolith/Foundation/WindingCharges.lean
insert_cancelling_preserves_winding · IndisputableMonolith/Foundation/WindingCharges.lean:175 
/-- **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 three_independent_winding_charges · IndisputableMonolith/Foundation/WindingCharges.lean
three_independent_winding_charges · IndisputableMonolith/Foundation/WindingCharges.lean:270 
/-- 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⟩
THEOREM winding_charges_certificate · IndisputableMonolith/Foundation/WindingCharges.lean
winding_charges_certificate · IndisputableMonolith/Foundation/WindingCharges.lean:417 
/-- **F-013 CERTIFICATE: Winding Charges**

    Conservation laws in RS are derived from winding numbers of lattice paths:

    1. **INTEGER**: w_k(path) ∈ ℤ (counts net steps) → charge quantization
    2. **ADDITIVE**: w_k(p₁++p₂) = w_k(p₁) + w_k(p₂) → charges add
    3. **INVARIANT**: Cancelling pairs preserve winding → topological protection
    4. **INDEPENDENT**: D axes give D independent charges
    5. **D-SPECIFIC**: Charge count = dimension → D=3 gives 3 charges
    6. **UNIFIED**: 3 charges = 3 face-pairs = 3 colors = 3 generations

    Conservation is NOT from symmetry (Noether). It is from TOPOLOGY:
    you cannot change a winding number by local deformations. -/
theorem winding_charges_certificate :
    -- 1. Winding numbers are additive
    (∀ (D : ℕ) (p₁ p₂ : LatticePath D) (k : Fin D),
      winding_number (List.append p₁ p₂) k = winding_number p₁ k + winding_number p₂ k) ∧
    -- 2. Cancelling pairs preserve winding
    (∀ (D : ℕ) (p₁ p₂ : LatticePath D) (s₁ s₂ : LatticeStep D) (k : Fin D),
      is_cancelling_pair s₁ s₂ →
      winding_number (List.append (List.append p₁ [s₁, s₂]) p₂) k =
        winding_number (List.append p₁ p₂) k) ∧
    -- 3. D = 3 gives 3 independent charges
    (Fintype.card (Fin 3) = 3) ∧
    -- 4. Charge count matches face-pairs
    (independent_loop_count 3 = ParticleGenerations.face_pairs 3) ∧
    -- 5. All the "3"s unify
    (Fintype.card SMCharge = independent_charge_count 3) :=
  ⟨fun D p₁ p₂ k => winding_additive p₁ p₂ k,
   fun D p₁ p₂ s₁ s₂ k h => insert_cancelling_preserves_winding p₁ p₂ s₁ s₂ h k,
   Fintype.card_fin 3,
   loops_eq_face_pairs_D3,
   sm_charges_match_D3⟩

What this page does not claim

The certificate does not prove that winding numbers correspond to electric, baryon, or lepton charge. The certificate does not claim that winding numbers are the only conserved quantities in the framework. The certificate does not show that the dynamics is actually implemented as local lattice 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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND