total_conservation
plain-language theorem explainer
Recognition Science counts five conservation laws by adding two non-spacetime laws to the three spacetime symmetries. A physicist verifying Noether correspondences in the framework would cite this result to confirm the total matches D + 2. The proof proceeds by a direct decide tactic on the numerical equality after substituting the definition of spacetimeConserved.
Claim. The total number of conservation laws satisfies $3 + 2 = 5$, where the three denotes the spacetime symmetry conserved quantities.
background
The Conservation Laws from RS module applies Noether's theorem to Recognition Science symmetries, listing five canonical conservation laws (energy, momentum, angular momentum, electric charge, baryon number) that equal configDim D = 5. spacetimeConserved is defined as the natural number 3, representing the three spacetime symmetry conserved quantities equal to D = 3. The upstream definition states: 'Three spacetime symmetry conserved quantities = D = 3.'
proof idea
The proof is a one-line wrapper that applies the decide tactic to verify the arithmetic equality after substituting the definition of spacetimeConserved as 3.
why it matters
This theorem supplies the total_five field inside the ConservationCert definition, closing the count of five laws. It aligns with the module's statement that three laws arise from spacetime symmetries while two others complete the set, supporting the framework landmark D = 3 spatial dimensions and the total of five conservation laws.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.