Foundation Topological Conservation

Topological Conservation

In Recognition Science, conserved quantities are not imposed by symmetry but are forced by the topology of the ledger. The module topological conservation formalizes the claim that conservation laws arise from linking in three dimensions, not from continuous symmetries as in Noether's theorem. The central objects are topological charges, which are integer-valued functions on configurations that remain unchanged under the variational dynamics of the ledger.

The module proves that topological charges are quantized: every charge takes an integer value on any configuration. It also proves that along any variational trajectory, the charge at any tick equals the charge at the initial tick, so conservation is exact and unconditional. These results are theorems in Lean 4, with no axioms beyond the kernel's standard three.

The module establishes that in exactly three dimensions, there are exactly three independent charges, and it identifies them with electric charge, baryon number, and lepton number. A bijection maps these three charges to the three axes of the configuration space. In any other dimension, the count of independent charges is zero. The theorem linking_iff_D3 states that a positive number of independent charges exists if and only if the dimension is three.

The module also contrasts topological conservation with Noether conservation. It proves that Noether charges, which arise from continuous symmetries, need not be integer-valued. The distinction is structural: topological charges are integer-valued and impossible to violate, while Noether charges are real-valued and can be broken by symmetry breaking.

THEOREM topological_charge_quantized · IndisputableMonolith/Foundation/TopologicalConservation.lean

THEOREM topological_charge_trajectory_conserved · IndisputableMonolith/Foundation/TopologicalConservation.lean

THEOREM three_charges_at_D3 · IndisputableMonolith/Foundation/TopologicalConservation.lean

THEOREM linking_iff_D3 · IndisputableMonolith/Foundation/TopologicalConservation.lean

THEOREM noether_not_necessarily_quantized · IndisputableMonolith/Foundation/TopologicalConservation.lean

What this page does not claim

This answer does not claim that the physical recognition-to-linking bridge is formalized; that bridge remains open. This answer does not claim that Noether's theorem is false; it claims only that Noether charges need not be integer-valued. This answer does not claim that the identification of the three charges with electric charge, baryon number, and lepton number is a theorem; it is a definitional choice in the module.

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: