def
definition
spacetimeConserved
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.ConservationLawsFromRS on GitHub at line 34.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
31theorem conservationLawCount : Fintype.card ConservationLaw = 5 := by decide
32
33/-- Three spacetime symmetry conserved quantities = D = 3. -/
34def spacetimeConserved : ℕ := 3
35theorem spacetime_conserved_eq_D : spacetimeConserved = 3 := rfl
36
37/-- Total conservation laws: 3 + 2 = 5 = D + 2. -/
38theorem total_conservation : spacetimeConserved + 2 = 5 := by decide
39
40structure ConservationCert where
41 five_laws : Fintype.card ConservationLaw = 5
42 three_spacetime : spacetimeConserved = 3
43 total_five : spacetimeConserved + 2 = 5
44
45def conservationCert : ConservationCert where
46 five_laws := conservationLawCount
47 three_spacetime := spacetime_conserved_eq_D
48 total_five := total_conservation
49
50end IndisputableMonolith.Physics.ConservationLawsFromRS