Foundation Winding Charges Three Independent Winding Charges

Three conserved quantities

A conserved quantity is a number attached to a system that does not change as the system evolves. In classical physics, examples include energy, momentum, and electric charge. The Recognition Science framework derives its own conserved quantities from a discrete model of paths on a lattice, a mathematical grid of points. The declaration three_independent_winding_charges proves that in three dimensions, exactly three such quantities exist, and they are independent of one another.

The framework models a world-line as a sequence of steps on a D-dimensional lattice, where each step moves along one axis or stays put. For each axis, the winding number is the net signed displacement: the number of steps in the positive direction minus the number in the negative direction. This is an integer by construction. The declaration proves three facts about these winding numbers in three dimensions: they are pairwise distinguishable, each can take any integer value, and there are exactly three of them. The proof is a theorem in the framework's machine-checked library of formal theorems.

The framework identifies these three winding numbers with electric charge, baryon number, and lepton number. This identification is a modeling choice, not a derivation. The framework proves that winding numbers are conserved under local deformations of a path, which it takes as the mechanism behind conservation laws. The declaration itself does not prove that these winding numbers correspond to the actual physical charges; that correspondence is a separate hypothesis.

The declaration also unifies several occurrences of the number three in the framework: the number of winding charges, the number of face-pairs, the number of colors, and the number of standard model charges all equal three. This unification is a theorem, but it is a statement about the framework's definitions, not about the physical world. The framework's library proves that the count of independent winding charges equals the dimension D for any positive D, and that for D equals three, this count is three.

What the declaration does not claim is that the physical universe has exactly three conserved charges of these types. It establishes a mathematical result about a lattice model. The step from the model to physical reality is a separate question, and the framework does not prove that the identification with electric charge, baryon number, and lepton number is correct. The declaration also does not claim that winding numbers are the only conserved quantities in the framework; other topological charges may exist.

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

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

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

/-- All the "3"s are the same "3". -/
theorem all_threes_unified :
    -- Number of winding charges
    Fintype.card (Fin 3) = 3 ∧
    -- Number of face-pairs
    ParticleGenerations.face_pairs 3 = 3 ∧
    -- Number of colors
    QuarkColors.N_colors 3 = 3 ∧
    -- Number of SM charges
    Fintype.card SMCharge = 3 ∧
    -- Topological charge count
    independent_charge_count 3 = 3 := by
  exact ⟨Fintype.card_fin 3, rfl, rfl, sm_charge_count, three_charges_at_D3⟩

What this page does not claim

The declaration does not prove that the physical universe has exactly three conserved charges of these types. The identification of winding numbers with electric charge, baryon number, and lepton number is a modeling choice, not a derivation. The declaration does not claim that winding numbers are the only conserved quantities in the framework.

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: