H_late_exp
plain-language theorem explainer
H_late_exp supplies the observed late-universe Hubble constant 73.04 as the benchmark for the dual-metric ratio test in Recognition Science cosmology. Researchers comparing early and late expansion rates cite this value to quantify agreement between the geometric prediction 67.4 times 13/12 and data. The entry is a direct numerical definition requiring no lemmas or tactics.
Claim. The experimentally measured late-universe Hubble constant is defined as $H_ {late}^{exp} := 73.04$.
background
The Cosmology.HubbleTension module formalizes the Hubble tension via the dual-metric hypothesis, where the ratio of late to early Hubble constants equals 13/12. This ratio arises from the static ledger of 12 edges versus the dynamic ledger of 12 edges plus one time dimension. The module draws constants from AlphaDerivation and geometry from CKMGeometry to anchor the numerical predictions.
proof idea
This declaration is a direct definition that binds H_late_exp to the real number 73.04. No lemmas are applied and no tactics are invoked.
why it matters
H_late_exp anchors the verification in hubble_ratio_match, which proves the geometric prediction matches observation to within 0.05 percent, and supports the T13Cert structure that records the geometric origin of the tension. It closes the link from the forcing chain (T7 eight-tick octave, T8 D=3) to the measured expansion rate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.