pith. machine review for the scientific record. sign in
theorem other other high

total_conservation

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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.

scope and limits

Lean usage

def conservationCert : ConservationCert where five_laws := conservationLawCount three_spacetime := spacetime_conserved_eq_D total_five := total_conservation

formal statement (Lean)

  38theorem total_conservation : spacetimeConserved + 2 = 5 := by decide

proof body

  39

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.