hubble_to_kms_mpc
plain-language theorem explainer
This definition converts a Hubble parameter expressed in inverse Planck times into the km/s/Mpc units standard in observational cosmology. Researchers comparing RS-native expansion rates to supernova or CMB data would invoke it when translating H0 predictions. The implementation is a direct one-line scaling that multiplies the input by the reciprocal of the CODATA Planck time and the factor 1000 over the IAU megaparsec length.
Claim. Let $h$ be a real number giving the Hubble parameter in units of inverse Planck time. The converted value in km s$^{-1}$ Mpc$^{-1}$ is $h / t_P^SI * 1000 / Mpc^SI$, where $t_P^SI$ denotes the Planck time in seconds and $Mpc^SI$ denotes one megaparsec in meters.
background
The module supplies the SI calibration seam that lets RS predictions, derived entirely in native units with $c=1$, be compared with laboratory measurements. The Planck scale furnishes the external numerical bridge: $t_P^SI$ is fixed at the CODATA 2018 value 5.391247e-44 s while $Mpc^SI$ follows the IAU 2012 definition as 3.0857e22 m. These two constants are the only dependencies of the present definition.
proof idea
The definition is a one-line algebraic wrapper that multiplies the input by the reciprocal of planck_time_SI and then by the factor 1000 / Mpc_SI. No lemmas are applied beyond the two upstream constant definitions.
why it matters
The definition completes the reporting seam described in the module documentation, allowing any RS-derived Hubble parameter (in native 1/τ0 units) to be stated in the km/s/Mpc convention used by the Hubble tension literature. It belongs to the set of SI anchor constants that sit between the native phi-ladder cosmology and external data; the module explicitly states that the SI numerical values are external calibration data, not RS predictions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.