def
definition
specialRelativityCert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.SpecialRelativityFromRS on GitHub at line 47.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
44 motion_positive : ∀ {r : ℝ}, 0 < r → r ≠ 1 → 0 < Jcost r
45 symmetric : ∀ {r : ℝ}, 0 < r → Jcost r = Jcost r⁻¹
46
47def specialRelativityCert : SpecialRelativityCert where
48 five_effects := srEffectCount
49 rest_zero := rest_frame
50 motion_positive := motion_cost
51 symmetric := sr_symmetry
52
53end IndisputableMonolith.Physics.SpecialRelativityFromRS