Foundation Topological Conservation Noether Not Necessarily Quantized

Noether charges need not be integers

Conservation laws in physics often come from continuous symmetries. Noether's theorem, proved by Emmy Noether in 1915 and published in 1918, states that every differentiable symmetry of a system's action has a corresponding conserved quantity. For example, the symmetry of a system under translation in space leads to conservation of momentum, and symmetry under rotation leads to conservation of angular momentum. These Noether charges, as they are called, take values in the real numbers, so they can be any real number, not just whole numbers.

In the Recognition Science framework, a machine-checked library of formal theorems formalizes this distinction. The framework models a ledger, a discrete record of events, where each configuration is a state and a trajectory is a sequence of states. A charge is a function that assigns a value to each configuration and is conserved along trajectories. The framework defines a topological charge as one whose value is always an integer, and it proves that such a charge is exactly conserved along any trajectory. It also defines a Noether charge as one whose value is a real number and is conserved along trajectories.

The key theorem, named noether_not_necessarily_quantized, proves that there exists a Noether charge whose value at some configuration is not an integer. This is a formal statement that Noether charges, unlike topological charges, are not required to be integers. The theorem does not say that Noether charges are never integers; it only says that they are not necessarily integers. The proof constructs an explicit example of a Noether charge that takes a non-integer value, showing that the real-valued nature of Noether charges is essential.

In Recognition Science, this distinction is central to the framework's account of conservation. The framework proves that topological charges, which arise from linking in three dimensions, are always integers and are conserved unconditionally. It also proves that in three dimensions there are exactly three independent topological charges, which it identifies with electric, baryon, and lepton number. The theorem about Noether charges establishes that a charge arising from a continuous symmetry does not have this integer property, so the framework's topological charges are a distinct and stronger kind of conservation.

What the theorem does not claim is that Noether's theorem is false, or that Noether charges are not conserved. It also does not claim that all conserved quantities in the framework are topological. The theorem is a precise statement about the range of values a Noether charge can take, and it highlights a structural difference between two types of conservation. This difference is what makes the framework's topological conservation a stronger and more rigid form of conservation than the one provided by continuous symmetries.

/-- **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 (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 (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 three_charges_at_D3 : independent_charge_count 3 = 3 := by
  simp [independent_charge_count]

theorem sm_charges_match_D3 :
    Fintype.card SMCharge = independent_charge_count 3 := by
  rw [sm_charge_count, three_charges_at_D3]

What this page does not claim

Noether's theorem is false or that Noether charges are not conserved. All conserved quantities in the framework are topological. The framework's topological charges are the same as the standard model's electric, baryon, and lepton numbers.

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: