structure
definition
ConservationCert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.ConservationLawsFromRS on GitHub at line 40.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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