def
definition
planck_to_seconds
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Cosmology.SIConversion on GitHub at line 84.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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
85
86/-- Convert a Hubble parameter from 1/t_P to km/s/Mpc.
87 H₀ [1/t_P] × (t_P [s] / Mpc [m]) × (1 km) = H₀ [km/s/Mpc]. -/
88def hubble_to_kms_mpc (h_planck : ℝ) : ℝ :=
89 h_planck * planck_time_SI⁻¹ * (1000 / Mpc_SI)
90
91/-- Convert seconds to Gyr. -/
92def seconds_to_Gyr (t_s : ℝ) : ℝ := t_s / Gyr_SI
93
94/-- Convert meters to billion light-years (Gly). -/
95def meters_to_Gly (r_m : ℝ) : ℝ := r_m / (ly_SI * 1e9)
96
97/-! ## Part 3: Observed Values for Comparison -/
98
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