HubbleTensionCert
plain-language theorem explainer
The HubbleTensionCert structure records that the RS-predicted late-to-early H0 ratio band (1.075, 1.091) is non-degenerate, contains the empirical central value 1.083, and that no measurement can be both consistent with the band and a falsifier below it. Cosmologists testing BIT-Z-aging explanations of the Hubble tension would cite this certificate when confirming data compatibility. The declaration is a direct structural bundling of the three supporting results band_nontrivial, empiricalCentral_in_band, and consistency_excludes_falsification.
Claim. Let $L = 1.075$, $U = 1.091$, and $C = 1.083$ be the RS-predicted lower bound, upper bound, and empirical central value of the late-to-early Hubble ratio. HubbleTensionCert asserts $L < U$, $L < C$ and $C < U$, and that for every real $h_0$ it is impossible for both $L < h_0 < U$ and $h_0 < L - (U - L)$ to hold simultaneously.
background
Recognition Science derives a predictive band for the late-to-early Hubble constant ratio from cosmic Z-aging on the BIT kernel, giving the interval (1.075, 1.091) that contains the observed central value 1.083. The module defines IsConsistentWithRS h0 to mean the ratio lies strictly inside this band and IsFalsifier h0 to mean the ratio lies below the lower bound by more than the full band width, acting as a rough 2σ proxy for falsification. The upstream lemmas establish non-degeneracy of the band, containment of the empirical central, and mutual exclusion of the two predicates.
proof idea
The declaration is a structure definition whose three fields are supplied directly by the supporting results: band_nontrivial for the inequality between bounds, empiricalCentral_in_band for containment of the central value, and consistency_excludes_falsification for the universal exclusion statement. No further reduction or tactic sequence is applied beyond referencing these lemmas.
why it matters
HubbleTensionCert is the central structural record of the RS Hubble band and is instantiated by hubbleTensionCert in the same module as well as in HubbleTensionFromBIT and HubbleTensionPipelineFromZAging. It is consumed by hubble_tension_cert in Gravity.HubbleTension. Within the Recognition framework it formalizes the phi-rational shift prediction near 1 + 1/(2 phi^2) and supplies the falsifier predicate that would refute the BIT-Z-aging account under future joint constraints.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.