hubbleRatioLower
plain-language theorem explainer
The definition supplies the numerical lower edge 1.075 of the RS-predicted interval for the late-to-early Hubble ratio. Cosmologists testing the BIT-Z-aging account of the Hubble tension cite this constant when verifying whether a new H0 measurement lies inside the band. The value enters by direct real-number assignment with no computation or lemma application.
Claim. The RS-predicted lower bound on the late-to-early Hubble constant ratio is $1.075$.
background
The module records the Hubble tension as the persistent discrepancy between late-time (SH0ES, Pantheon+) and early-time (Planck) H0 measurements. RS derives the late-to-early ratio from cosmic Z-aging on the BIT kernel, producing the closed interval whose lower endpoint is the constant defined here and whose upper endpoint is 1.091; the empirical central value 1.083 lies inside this interval. The band is described as a tight neighborhood of the canonical RS shift $1 + 1/(2·φ²)$.
proof idea
The declaration is a direct definition that assigns the real number 1.075 to the lower-bound constant.
why it matters
This constant forms the lower edge of the band that appears in the HubbleTensionCert structure and in the supporting theorems band_nontrivial, empiricalCentral_in_band, and consistency_excludes_falsification. It supplies the concrete numerical anchor for the falsifier predicate IsFalsifier and for the consistency check IsConsistentWithRS. The construction closes the predictive band required by the BIT-Z-aging explanation of the Hubble tension.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.