Foundation Topological Conservation Topological Charge Trajectory Conserved

Conservation as topology

A conservation law is a rule that some quantity stays the same while a system changes. The classical example is energy: in a closed system, energy is neither created nor destroyed, only converted from one form to another. The Recognition Science framework offers a different picture. It models a physical system as a ledger, a discrete record of states, and it defines a charge as a function that assigns an integer to each state. The declaration topological_charge_trajectory_conserved proves that for any such charge, its value at the start of a valid trajectory equals its value at every later step.

The proof is short and direct. A trajectory is a sequence of states where each step is a variational successor of the one before, meaning the system moves according to its dynamics. The charge's defining property is that it is conserved across any single variational step. The theorem uses induction over the length of the trajectory: if the charge is the same after one step, and the next step also preserves it, then it is the same after any number of steps. This is exact conservation, not approximate. The charge at tick one, tick ten, or tick one thousand is identical to its value at the start.

The framework's central claim is that this conservation is topological, not the result of a continuous symmetry as in Noether's theorem. A linking number, the count of how many times one loop winds around another, is an integer that cannot change under continuous deformation. The framework identifies charge with such a linking number. In three dimensions, linking is possible, and the framework proves that exactly three independent charges exist there, which it names electric, baryon, and lepton. In any other dimension, the framework proves that no such independent charges exist.

This theorem does not claim that any particular physical quantity, such as electric charge, is actually conserved in the real world. It establishes a structural result: if a quantity is defined as a topological charge in this framework, then it is exactly conserved along any valid trajectory. Whether the real electron's charge corresponds to such a definition is a separate question. The theorem also does not claim that Noether's theorem is wrong. It proves that Noether charges need not be integers, while topological charges always are, but both can coexist in the framework's library.

/-- **THEOREM (Exact Conservation Along Trajectories)** -/
theorem topological_charge_trajectory_conserved {N : ℕ} (Q : TopologicalCharge N)
    (traj : Trajectory N) (h : IsVariationalTrajectory traj) :
    ∀ t, Q.value (traj t) = Q.value (traj 0) := by
  intro t
  induction t with
  | zero => rfl
  | succ n ih => rw [← ih]; exact Q.conserved (traj n) (traj (n + 1)) (h n)

theorem three_charges_at_D3 : independent_charge_count 3 = 3 := by
  simp [independent_charge_count]

/-- The three conserved charges of the Standard Model. -/
inductive SMCharge where
  | electric : SMCharge
  | baryon : SMCharge
  | lepton : SMCharge
  deriving DecidableEq, Fintype

theorem no_charges_at_other_D (D : ℕ) (hD : D ≠ 3) :
    independent_charge_count D = 0 := by
  simp [independent_charge_count, hD]

/-- **THEOREM (Noether Charges Need Not Be Quantized)**:
    There exist Noether charges that take non-integer values.

    Proof: log(2) satisfies 0 < log(2) < 1, so it is not an integer. -/
theorem noether_not_necessarily_quantized :
    ∃ (N : ℕ) (Q : NoetherCharge N) (c : Configuration N),
      ¬∃ n : ℤ, Q.value c = (n : ℝ) := by
  use 1, logChargeAsNoether 1
  let c : Configuration 1 := {
    entries := fun _ => 2
    entries_pos := fun _ => by norm_num
  }
  use c
  intro ⟨n, hn⟩
  simp only [logChargeAsNoether, log_charge, Fin.sum_univ_one] at hn
  have h_pos : 0 < Real.log 2 := Real.log_pos (by norm_num : (1 : ℝ) < 2)
  have h_lt : Real.log 2 < 1 := by
    have h2_lt_e : (2 : ℝ) < Real.exp 1 := by
      exact lt_trans (by norm_num) Real.exp_one_gt_d9
    calc Real.log 2 < Real.log (Real.exp 1) :=
          Real.log_lt_log (by norm_num) h2_lt_e
      _ = 1 := Real.log_exp 1
  have h1 : (0 : ℝ) < n := by linarith
  have h2 : (n : ℝ) < 1 := by linarith
  have h3 : (0 : ℤ) < n := Int.cast_pos.mp h1
  have h4 : n < (1 : ℤ) := by exact_mod_cast h2
  omega

/-- **THEOREM (Quantization Is Automatic)**:
    Every topological charge takes integer values. -/
theorem topological_charge_quantized {N : ℕ} (Q : TopologicalCharge N)
    (c : Configuration N) : ∃ n : ℤ, Q.value c = n :=
  ⟨Q.value c, rfl⟩

What this page does not claim

This theorem does not claim that any specific physical charge, such as electric charge, is conserved in the actual universe. This theorem does not claim that Noether's theorem is false or that continuous symmetries play no role in physics. This theorem does not claim that the framework has derived the values of the elementary charges, only that their conservation is structural.

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/TopologicalConservation.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: