conservationLawCount
plain-language theorem explainer
Recognition Science admits exactly five conservation laws. A physicist applying Noether's theorem to RS symmetries would cite this cardinality to confirm the match with configuration dimension five. The proof is a direct decision on the finite inductive type listing energy, momentum, angular momentum, electric charge, and baryon number.
Claim. The finite type of conservation laws has cardinality $5$, consisting of energy, momentum, angular momentum, electric charge, and baryon number.
background
The module derives conservation laws from RS symmetries via Noether's theorem. It lists five quantities: energy from time translation, momentum and angular momentum from spatial translations and rotations (corresponding to D = 3), electric charge as recognition charge conservation with σ = 0, and baryon number. The local inductive type ConservationLaw enumerates these five cases and derives a Fintype instance. Upstream, the Ledger module defines a general ConservationLaw structure as a named charge assignment closed under interactions.
proof idea
The proof applies the decide tactic to the Fintype.card computation on the inductive type, which has five constructors and thus cardinality five.
why it matters
This theorem supplies the five_laws component of conservationCert. It confirms that the total number of conservation laws equals five, with three originating from spacetime symmetries. This aligns with the framework's derivation of D = 3 spatial dimensions and the five canonical laws including charge conservation as σ = 0.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.