Foundation Topological Conservation Topological Conservation Certificate

The conservation certificate

In physics, a conservation law says some quantity stays the same as a system evolves. The standard route to such laws, due to Emmy Noether in 1918, ties each one to a continuous symmetry of the theory: time symmetry gives energy, space symmetry gives momentum. The Recognition Science framework takes a different route. Its central claim is that conservation comes from topology, from the way curves link around each other in three-dimensional space, not from symmetry. The declaration topological_conservation_certificate is the machine-checked theorem that bundles this claim into one formal statement.

The certificate assembles seven results. First, in three dimensions the framework's ledger, a discrete record of recognition events, supports exactly three independent charges, and in any other dimension it supports none. Second, those three charges match the three axes of the rotation group Q₃, one-to-one. Third, the framework names them electric, baryon, and lepton charge, matching the three conserved quantities of the Standard Model of particle physics. Fourth, every topological charge takes integer values, and fifth, its value is exactly conserved along every trajectory the dynamics allows. Sixth, a Noether-style charge, one defined by continuous symmetry, need not take integer values; the framework proves a counterexample exists. Finally, the certificate records that the charge count equals the number of face pairs of a cube, a purely combinatorial fact.

The certificate is honest about its limits. It proves a formal correspondence between the framework's definitions and the number three, but it does not prove that the Standard Model's electric, baryon, and lepton charges are the framework's charges. The names are an identification, a modeling choice, not a derived result. The certificate also does not prove that conservation in nature actually arises from linking; it proves that within the framework's definitions, a topological charge is conserved. The bridge from the framework's recognition events to physical space and physical particles remains open.

What the certificate does establish is internal consistency. The framework claims conservation laws come from topology, and the certificate shows that claim holds together: charges are integer-valued, conserved, and only exist in three dimensions, all from the same definitions. It also draws a sharp contrast with the Noether picture, since the framework proves its own charges are quantized while symmetry-based charges need not be. That contrast is the payoff: if conservation is topological, quantization is not an accident but a necessity.

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

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

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

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

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

What this page does not claim

The certificate does not prove that the Standard Model's electric, baryon, and lepton charges are the framework's charges. The certificate does not prove that conservation in nature arises from linking rather than from symmetry. The certificate does not establish the physical bridge from recognition events to three-dimensional space.

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: