spacetimeConserved
Recognition Science counts three conserved quantities arising from spacetime symmetries, matching the spatial dimension D. Researchers separating spacetime contributions from the five total conservation laws reference this value when applying Noether's theorem in the RS setting. The declaration is a direct constant definition with no lemmas or reduction steps.
claimThe number of conserved quantities arising from spacetime symmetries is defined to be three: $3$.
background
The Conservation Laws from RS module applies Noether's theorem to link symmetries with conservation laws. It identifies five canonical laws (energy, momentum, angular momentum, electric charge, baryon number) whose total equals D + 2, where D denotes the spatial dimension. Three of these laws originate from spacetime symmetries: momentum from translation invariance, angular momentum from rotation invariance, and energy from time translation invariance. The module notes that σ = 0 supplies the RS form of charge conservation while J decreases globally.
proof idea
This is a direct definition that assigns the constant 3 to the spacetime symmetry count. No lemmas are invoked and no tactics are executed; the value is fixed for use in downstream certification structures.
why it matters in Recognition Science
The definition supplies the spacetime contribution required by ConservationCert, where five_laws equals 5 and three_spacetime equals 3, which immediately yields the total_conservation theorem spacetimeConserved + 2 = 5. It implements the T8 step of the forcing chain that fixes D = 3 spatial dimensions and aligns the eight-tick octave with the observed count of spacetime-derived laws.
scope and limits
- Does not derive the three spacetime symmetries from the recognition functional equation.
- Does not name the specific conserved quantities (energy, momentum, angular momentum).
- Does not address the two non-spacetime laws or their relation to σ = 0.
- Does not connect the count to J-cost, defectDist, or the phi-ladder.
Lean usage
theorem spacetime_conserved_eq_D : spacetimeConserved = 3 := rflformal statement (Lean)
34def spacetimeConserved : ℕ := 3