spacetime_conserved_eq_D
plain-language theorem explainer
The theorem fixes the count of conserved quantities from spacetime symmetries at exactly three. A physicist deriving Noether correspondences in Recognition Science would cite this to anchor the spatial dimension at D = 3. The proof is a direct reflexivity step on the constant definition of the spacetime conserved count.
Claim. The number of conserved quantities arising from spacetime symmetries equals three: $3$.
background
The module derives conservation laws from RS via Noether's theorem, linking each symmetry to a conserved quantity. Spacetime symmetries produce momentum, angular momentum, and energy, for a total of three. The upstream definition states: 'Three spacetime symmetry conserved quantities = D = 3.' The local setting records five canonical laws equal to configDim D = 5, with three originating from spacetime.
proof idea
This is a one-line wrapper that applies reflexivity to the definition of the spacetime conserved count.
why it matters
The equality populates the three_spacetime field inside the conservation certificate, verifying that three spacetime laws plus two others sum to five. It directly supports framework landmark T8, which forces D = 3 spatial dimensions, and closes the count of spacetime-derived conservations in the RS Noether correspondence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.