Foundation Topological Conservation Topological Charge Quantized

Topological charge quantization

In mathematics and physics, a topological invariant is a property of a geometric object that remains unchanged under continuous deformations, like stretching or bending, but not tearing. For example, the number of holes in a doughnut is a topological invariant: a coffee cup and a doughnut both have one hole, so they are topologically equivalent. In the Recognition Science (RS) framework, this idea is applied to the ledger, a discrete record of recognition events, where the state of a system at any moment is called a configuration.

Within this framework, the declaration topological_charge_quantized establishes a fundamental property of a specific kind of charge. A topological charge is defined as a function that assigns an integer value to every configuration, and this value is conserved, meaning it stays the same when the system moves from one configuration to the next. The theorem proves that for any such charge and any configuration, there exists an integer that equals the charge's value. This means the charge is always quantized, taking only whole-number values like -2, 0, or 7, never fractional ones.

The proof of this theorem is almost immediate from the definition. Since a topological charge's value is defined to be an integer, the theorem simply states that this value is, in fact, an integer. The real substance lies in the structure that defines a topological charge: it is a function from configurations to the integers that is conserved under the framework's variational dynamics, the rules that describe how a system evolves from one tick to the next. This structure is what makes the conservation law unconditional, as shown by the related theorem conservation_is_unconditional.

This approach contrasts with conservation laws derived from continuous symmetries, as in Noether's theorem. In RS, a Noether charge is defined similarly, but its value is a real number, not an integer. The framework proves that Noether charges are not necessarily quantized, meaning they can take any real value. This distinction is a core part of the framework's claim that conservation laws arise from topology, not symmetry.

In Recognition Science, this theorem is part of a larger argument. The framework models three independent charges at dimension three, which it associates with electric, baryon, and lepton number. The theorem topological_charge_quantized is a foundational piece, establishing that these charges, if they are topological, must be integer-valued. This is a necessary condition for the framework's model of particle physics, but it does not, by itself, prove that these specific charges exist or that they match the measured values of the standard model.

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

/-- A **topological charge** on an N-entry ledger is an integer-valued function
    of the configuration that is invariant under the variational dynamics.

    Integer-valuedness is the formal content of "charge quantization."
    It is structural (the codomain is ℤ), not imposed. -/
structure TopologicalCharge (N : ℕ) where
  value : Configuration N → ℤ
  conserved : ∀ (c next : Configuration N),
    IsVariationalSuccessor c next → value next = value c

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

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

What this page does not claim

This theorem does not prove that the electric, baryon, or lepton charges exist as physical observables. It does not claim that any specific physical charge, such as electric charge, is quantized in the real world. The theorem does not establish that all conservation laws in physics are topological in origin.

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: