def
definition
specialRelativityDeepCert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.SpecialRelativityDeep on GitHub at line 70.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
67 mass_energy_pos : ∀ r : ℕ, 0 < mass_energy_RS r
68 structural : True -- SR follows from J-cost symmetry
69
70noncomputable def specialRelativityDeepCert : SpecialRelativityDeepCert where
71 jcost_cosh_identity := jcost_cosh_is_gamma_minus_one
72 mass_energy_pos := mass_energy_pos
73 structural := trivial
74
75theorem specialRelativityDeepCert_inhabited : Nonempty SpecialRelativityDeepCert :=
76 ⟨specialRelativityDeepCert⟩
77
78end
79end SpecialRelativityDeep
80end Foundation
81end IndisputableMonolith