IsFalsifier
The predicate flags a measured late-to-early Hubble ratio as falsifying the RS band when the value lies more than one full band width below the lower edge. Cosmologists testing the BIT-Z-aging account of the H0 tension would cite it to classify future joint constraints. It is realized as a direct arithmetic comparison against the fixed constants 1.075 and 1.091.
claimLet $r$ be the measured late-to-early $H_0$ ratio. Then $r$ is a falsifier when $r < 1.075 - (1.091 - 1.075)$.
background
The module records the RS-predicted band for the late-to-early Hubble ratio as the interval from 1.075 to 1.091, obtained from cosmic Z-aging on the BIT kernel. The sibling definitions hubbleRatioLower and hubbleRatioUpper supply these endpoints; the falsifier condition requires the measured ratio to fall below the lower endpoint by more than the full width of the interval, serving as a rough 2σ proxy. The module documentation states that the empirical central value 1.083 lies inside the band and that the structure certifies consistency while exposing a clear falsification route.
proof idea
The definition is a one-line arithmetic predicate that subtracts the band width from the lower bound and compares the input ratio against the result. It directly references the pre-defined constants hubbleRatioLower and hubbleRatioUpper.
why it matters in Recognition Science
This definition supplies the falsification side of the mutual-exclusion theorem consistency_excludes_falsification and is embedded in the HubbleTensionCert structure. It operationalizes the predictive band stated in the module documentation, which arises from the phi-rational shift in the Recognition Science framework. The predicate closes the falsification interface for this cosmological claim.
scope and limits
- Does not incorporate statistical uncertainties or covariance from specific surveys.
- Does not assert that current data satisfies or violates the predicate.
- Does not derive the numerical band values from first principles.
- Does not address other tensions or cosmological parameters.
formal statement (Lean)
61def IsFalsifier (h0_ratio : ℝ) : Prop :=
proof body
Definition body.
62 h0_ratio < hubbleRatioLower - (hubbleRatioUpper - hubbleRatioLower)
63
64/-- Consistency and falsification are mutually exclusive. -/