`c_SI`

definition

show as: view math explainer →

module: IndisputableMonolith.Cosmology.SIConversion
domain: Cosmology
line: 54 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Cosmology.SIConversion on GitHub at line 54.

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

  51def planck_time_SI : ℝ := 5.391247e-44
  52
  53/-- Speed of light in m/s (exact since 2019 SI redefinition). -/
  54def c_SI : ℝ := 299792458
  55
  56/-- 1 Megaparsec in meters (IAU 2012 definition).
  57    1 pc = 648000/π AU, 1 AU = 149597870700 m (exact). -/
  58def Mpc_SI : ℝ := 3.0857e22
  59
  60/-- 1 light-year in meters. -/
  61def ly_SI : ℝ := 9.461e15
  62
  63/-- 1 Gyr (billion years) in seconds. -/
  64def Gyr_SI : ℝ := 3.1557e16
  65
  66theorem planck_length_SI_pos : 0 < planck_length_SI := by
  67  unfold planck_length_SI; norm_num
  68
  69theorem planck_time_SI_pos : 0 < planck_time_SI := by
  70  unfold planck_time_SI; norm_num
  71
  72theorem c_SI_pos : 0 < c_SI := by
  73  unfold c_SI; norm_num
  74
  75theorem Mpc_SI_pos : 0 < Mpc_SI := by
  76  unfold Mpc_SI; norm_num
  77
  78/-! ## Part 2: Conversion Functions -/
  79
  80/-- Convert a distance from Planck lengths to meters. -/
  81def planck_to_meters (r_planck : ℝ) : ℝ := r_planck * planck_length_SI
  82
  83/-- Convert a time from Planck times to seconds. -/
  84def planck_to_seconds (t_planck : ℝ) : ℝ := t_planck * planck_time_SI

papers checked against this theorem

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