Foundation Topological Conservation Charge To Axis Surjective

Three charges, three axes

In the Recognition Science framework, a ledger is a discrete record of events, and a recognition is a cost that the framework proves must take a specific form. The declaration charge_to_axis_surjective is a small but exact piece of that framework: it proves that the three conserved charges the framework recognizes, electric, baryon, and lepton, cover all three spatial axes. In plain terms, every one of the three axes has a charge assigned to it, and no axis is left empty.

The proof is a theorem in the framework's machine-checked library of formal theorems. It states that the function sending each charge to an axis is surjective, meaning its image is the whole set of three axes. Combined with the companion result that the same function is injective, no two charges share an axis, the framework derives a bijection: exactly three charges correspond exactly to three axes. The framework also proves that this count is special to three dimensions: at any other dimension the number of independent charges is zero, and the existence of any such charge is equivalent to the dimension being three.

This result belongs to a larger claim in the framework: conservation laws arise from topology, from the way curves link in three-dimensional space, rather than from continuous symmetries as in the classical Noether approach. The framework defines a topological charge as an integer-valued quantity that stays constant along any allowed trajectory. Because linking numbers cannot change under continuous deformation, the framework derives that these charges are exactly conserved, unconditionally, with no symmetry assumption. The three charges are then identified with the three axes of space, giving the bijection that charge_to_axis_surjective completes.

What this declaration does not claim is just as important. It does not prove that electric, baryon, or lepton charge actually exists in the physical world; that would require identifying the framework's abstract charges with measured particles. It does not prove that conservation laws in general must be topological, only that within this framework a topological charge is exactly conserved. And it does not prove that the number three is forced by physics; the framework's own documents note that the bridge from recognition to physical linking remains open. The declaration is a precise statement inside a formal system, not a claim about experiment.

theorem charge_to_axis_surjective : Function.Surjective charge_to_axis := by
  intro ⟨n, hn⟩; interval_cases n
  · exact ⟨.electric, rfl⟩
  · exact ⟨.baryon, rfl⟩
  · exact ⟨.lepton, rfl⟩

theorem charge_to_axis_bijective : Function.Bijective charge_to_axis :=
  ⟨charge_to_axis_injective, charge_to_axis_surjective⟩

/-- Linking-based charges exist iff D = 3. -/
theorem linking_iff_D3 (D : ℕ) :
    0 < independent_charge_count D ↔ D = 3 := by
  simp [independent_charge_count]; split <;> omega

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

/-- Conservation is unconditional — no symmetry assumption needed. -/
theorem conservation_is_unconditional {N : ℕ} (Q : TopologicalCharge N)
    (c next : Configuration N) (h : IsVariationalSuccessor c next) :
    Q.value next = Q.value c :=
  Q.conserved c next h

What this page does not claim

This declaration does not prove that electric, baryon, or lepton charge exists in the physical world. This declaration does not prove that all conservation laws must be topological. This declaration does not prove that the number three is forced by physics.

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: