obs_H0_late
plain-language theorem explainer
This definition supplies the numerical value of the late-universe Hubble parameter in km/s/Mpc taken from the SH0ES 2022 measurement. Cosmologists converting RS-native predictions to SI observables would reference it when calibrating expansion-rate comparisons. The entry is a direct constant assignment with no further computation or derivation.
Claim. The observed late-universe Hubble constant is defined as $H_0 = 73.04$ in units of km s$^{-1}$ Mpc$^{-1}$.
background
The module establishes an SI calibration seam that converts RS-native units (where $c = 1$, Planck length equals $1/√π$) into meters, seconds, and km/s/Mpc. It anchors all cosmological observables to the external CODATA value of the Planck length, treating SI numbers as calibration constants rather than RS predictions. The ratios of observables to Planck units carry the theoretical content; the absolute SI values serve only as the reporting bridge.
proof idea
Direct constant definition that assigns the SH0ES 2022 central value with no lemmas or tactics applied.
why it matters
It supplies the observational anchor required for any RS-to-SI conversion of the Hubble parameter, allowing direct numerical comparison between native-unit cosmology and late-universe data. The entry sits inside the broader SI seam described in the module documentation and supports downstream expressions of age, distance, and expansion observables.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.