IndisputableMonolith.Verification.Preregistered.Hubble.Test
Preregistered verification suite for the Recognition Science Hubble ratio: the late-time expansion rate predicted from early-universe inputs must match observation within 0.05% relative error. Also checks an Ω_Λ consistency band and an α/π bound used in the geometric pipeline. Anyone auditing the Hubble-tension claim in RS cites this module. Structure is pure test harness: frozen prediction module plus pure measurement data, with Lean inequalities as pass/fail certificates.
claimThe RS-predicted late-to-early Hubble ratio $H_{\mathrm{late}}/H_{\mathrm{early}}$ agrees with the 2022 representative measurements to relative error at most $5\times 10^{-4}$. Separately, $\Omega_\Lambda$ lies inside the $1\sigma$ Planck band, and the fine-structure combination $\alpha/\pi$ obeys the stated numerical bounds used by the CKM-geometry pipeline.
background
Recognition Science freezes formulas before they see data. The preregistered harness (Core) enforces that structurally: prediction modules import no measurement modules; measurement modules are pure data; only test modules import both. Hubble.Prediction therefore carries the RS ratio and $\Omega_\Lambda$ formulas with no observational numbers. Measurement_2022 holds representative Hubble-tension values and Planck $\Omega_\Lambda$, updated only when releases change.
The RS claim under test is that a single early-universe ratio, fixed by the ledger geometry and constants (including $\alpha$), predicts the late expansion rate. Sibling certificates in this module are the relative-error pass for that ratio, a $1\sigma$ pass for $\Omega_\Lambda$, and bounds on $\alpha/\pi$ shared with the CKM geometry derivation (T11).
proof idea
Not a single theorem proof: a test module. It imports the frozen prediction, the 2022 measurement table, and supporting constant/geometry modules, then states Lean propositions that the predicted ratio lies within 0.05% relative of the measured late/early values, that $\Omega_\Lambda$ sits in the Planck $1\sigma$ window, and that $\alpha/\pi$ meets the numeric bounds. Each sibling is a concrete inequality certificate; there is no free parameter fit inside the test.
why it matters in Recognition Science
This is the audit surface for the RS resolution of the Hubble tension under the preregistration discipline: formula frozen, data separate, pass/fail machine-checked. Downstream consumers are external (used_by is empty); the module is a leaf verification artifact rather than a lemma feeder. It sits beside the CKM-geometry and $\alpha$ pipelines so the same constant stack that fixes mixing angles is the one scored against cosmology. A referee checking whether RS overfits late $H_0$ should start here: if the relative-error certificate fails after a measurement update, the claim is falsified without touching the prediction source.
scope and limits
- Does not derive the Hubble ratio formula; that lives in the Prediction module.
- Does not update or choose observational numbers; Measurement_2022 is pure data.
- Does not claim sub-0.05% agreement beyond the stated relative tolerance.
- Does not resolve full cosmological parameter inference or CMB likelihoods.
- Does not feed downstream Lean theorems; used_by is empty (leaf test).