consistency_excludes_falsification
plain-language theorem explainer
The theorem proves that no real Hubble ratio can satisfy both the RS consistency predicate and the falsifier predicate at once. Cosmologists testing the BIT-Z-aging account of the Hubble tension would cite this result when assembling structural certificates for the predicted band. The proof is a short term-mode argument that assumes the conjunction, unfolds the numerical bounds, and applies linear arithmetic to obtain an immediate contradiction.
Claim. For any real number $r$, it is impossible that both $1.075 < r < 1.091$ and $r < 1.075 - (1.091 - 1.075)$ hold simultaneously.
background
The module records a predictive band for the late-to-early Hubble constant ratio under the Recognition Science BIT-Z-aging model. The lower bound is fixed at 1.075 and the upper bound at 1.091. A ratio $r$ is consistent with RS precisely when it lies strictly inside this interval; it qualifies as a falsifier when it lies below the lower bound by more than the full band width, serving as a rough 2σ exclusion proxy.
proof idea
The term proof assumes both predicates hold for a given $h_0$. It unfolds IsFalsifier together with the concrete values of hubbleRatioLower and hubbleRatioUpper, then invokes linarith. The resulting arithmetic contradiction follows at once because the falsifier condition forces the ratio strictly below the lower bound while consistency requires it to exceed that bound.
why it matters
The result populates the HubbleTensionCert structure, which bundles band nontriviality, the empirical central value inside the band, and this mutual exclusion. It thereby certifies that the RS-predicted interval remains logically disjoint from its falsifiers, supporting the claim that current data do not yet exclude the BIT-Z-aging explanation. The band itself is noted as a tight neighborhood of the canonical RS shift $1 + 1/(2·φ²)$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.