IsConsistentWithRS
plain-language theorem explainer
The predicate holds exactly when a measured late-to-early Hubble ratio lies strictly inside the interval (1.075, 1.091). Cosmologists testing whether fresh H0 data remains compatible with the BIT-Z-aging account would cite this predicate. It is realized as the direct conjunction of the two precomputed numeric bounds.
Claim. A real number $r$ satisfies the consistency predicate if and only if $1.075 < r < 1.091$.
background
The module records the Hubble tension as a ~5σ discrepancy between late-time (SH0ES, Pantheon+) and early-time (Planck) H0 measurements. Recognition Science derives the late-to-early ratio from cosmic Z-aging on the BIT kernel, producing the φ-rational band (1.075, 1.091) that contains the empirical central value 1.083. The module states that a future joint constraint placing the ratio outside this band at >2σ would falsify the BIT-Z-aging explanation.
proof idea
The definition is a one-line wrapper that applies the conjunction of the lower-bound and upper-bound comparisons. It directly references the numeric constants 1.075 and 1.091 without invoking further lemmas.
why it matters
This predicate supplies the consistency side of the mutual-exclusion theorem consistency_excludes_falsification and populates the HubbleTensionCert structure. It certifies that the empirical central value lies inside the predicted band, closing the structural loop on the BIT-Z-aging account. The band is a tight neighborhood of the canonical RS shift 1 + 1/(2·φ²) and sits inside the eight-tick octave framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.