conservationCert
plain-language theorem explainer
The declaration supplies a concrete certificate that the Recognition Science framework yields precisely five conservation laws, three arising from spacetime symmetries. A physicist modeling Noether correspondences in discrete recognition models would cite this to anchor the count as D + 2. The construction is a direct record instantiation that assembles the cardinality theorem, the spacetime equality, and the total sum theorem.
Claim. Let $C$ be the set of conservation laws. The certificate asserts that the cardinality of $C$ equals 5, that the number of spacetime-conserved quantities equals 3, and that spacetime-conserved plus 2 equals 5.
background
In the Conservation Laws from RS module the framework derives conservation laws from symmetries in the style of Noether's theorem. The structure ConservationCert packages three assertions: the total number of laws is five, three come from spacetime, and the arithmetic closes as 3 + 2 = 5. ConservationLaw enumerates the five laws (energy, momentum, angular momentum, electric charge, baryon number) while spacetimeConserved counts those tied to the D = 3 spatial dimensions. Upstream, conservationLawCount proves the cardinality is 5 by decision, spacetime_conserved_eq_D equates it to 3 by reflexivity, and total_conservation confirms the sum as D + 2.
proof idea
The definition constructs the ConservationCert record by direct field assignment: conservationLawCount supplies the five_laws field, spacetime_conserved_eq_D supplies three_spacetime, and total_conservation supplies total_five. Each step is a one-line reference to the corresponding theorem.
why it matters
This definition completes the packaging of the conservation law count in the RS foundation, directly supporting the claim that five laws match configDim D = 5. It ties into the forcing chain step T8 that fixes D = 3 spatial dimensions and the overall five-law structure. The parent structure ConservationCert serves as the interface for any later physics derivations, though the dependency graph shows no immediate downstream users.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.