`obs_radius_m`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Cosmology.SIConversion on GitHub at line 102.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  99/-- Observed comoving radius of the observable universe (meters).
 100    Source: Planck 2018 ΛCDM fit.
 101    46.5 Gly ≈ 4.40 × 10²⁶ m. -/
 102def obs_radius_m : ℝ := 4.40e26
 103
 104/-- Observed age of the universe (seconds).
 105    13.787 ± 0.020 Gyr (Planck 2018). -/
 106def obs_age_s : ℝ := 4.354e17
 107
 108/-- Observed age in Gyr. -/
 109def obs_age_Gyr : ℝ := 13.787
 110
 111/-- Early-universe Hubble measurement (km/s/Mpc).
 112    Planck 2018: 67.36 ± 0.54. -/
 113def obs_H0_early : ℝ := 67.36
 114
 115/-- Late-universe Hubble measurement (km/s/Mpc).
 116    SH0ES 2022 (Riess et al.): 73.04 ± 1.04. -/
 117def obs_H0_late : ℝ := 73.04
 118
 119/-! ## Part 4: SI Certificate -/
 120
 121structure SICalibrationCert where
 122  planck_length_positive : 0 < planck_length_SI
 123  planck_time_positive : 0 < planck_time_SI
 124  consistency : planck_length_SI / c_SI < planck_time_SI * 1.01
 125  consistency2 : planck_time_SI * 0.99 < planck_length_SI / c_SI
 126
 127theorem si_calibration_cert : SICalibrationCert where
 128  planck_length_positive := planck_length_SI_pos
 129  planck_time_positive := planck_time_SI_pos
 130  consistency := by unfold planck_length_SI c_SI planck_time_SI; norm_num
 131  consistency2 := by unfold planck_length_SI c_SI planck_time_SI; norm_num
 132

papers checked against this theorem

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