empiricalCentral
plain-language theorem explainer
The declaration fixes the observed central value of the late-to-early Hubble ratio at the real number 1.083 drawn from SH0ES and Planck data. Cosmologists testing the Recognition Science BIT-Z-aging prediction would cite this constant when verifying that the measured ratio lies inside the band (1.075, 1.091). The definition is a direct numerical assignment requiring no lemmas or computation.
Claim. Let $c$ denote the central empirical value of the late-to-early Hubble ratio $H_0^text{late}/H_0^text{early}$. Then $c = 1.083$.
background
The module records the Hubble tension as the persistent discrepancy between late-time (SH0ES, Pantheon+) and early-time (Planck CMB) measurements of the present Hubble constant. Recognition Science derives a predicted ratio band via cosmic Z-aging on the BIT kernel; the band (1.075, 1.091) is a tight neighborhood of the canonical shift $1 + 1/(2·φ²)$. This definition supplies the observed central datum 1.083 for direct comparison against that band.
proof idea
The definition is a direct numerical assignment of the constant 1.083. No lemmas from the upstream results (collision-free empirical programs, simplicial edge lengths, mechanism design structures, or mock theta phantoms) are invoked.
why it matters
The constant supplies the empirical anchor required by the downstream theorem empiricalCentral_in_band and the structure HubbleTensionCert. It fills the observed-datum slot in the RS cosmology prediction, confirming that the BIT-Z-aging explanation remains consistent with current data. The module states that a future joint constraint placing the measured ratio outside the band at >2σ would falsify the explanation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.