`SpecialRelativityDeepCert`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.SpecialRelativityDeep
domain: Foundation
line: 65 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.SpecialRelativityDeep on GitHub at line 65.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  62  unfold mass_energy_RS
  63  exact mul_pos (pow_pos phi_pos r) (zpow_pos phi_pos (-5))
  64
  65structure SpecialRelativityDeepCert where
  66  jcost_cosh_identity : ∀ θ : ℝ, Jcost (Real.cosh θ) = Real.cosh θ - 1
  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.