hubble_ratio
plain-language theorem explainer
Preregistered RS forecast that the late-to-early Hubble ratio equals the rational 13/12. Cosmologists and auditors of the RS Hubble-tension test cite this constant as the fixed prediction side of the comparison. It is a bare PointPrediction record: name string plus the literal real value 13/12, with no further computation.
Claim. The preregistered point prediction for the Hubble ratio $H_{\mathrm{late}}/H_{\mathrm{early}}$ is the real number $13/12$.
background
This module holds preregistered predictions for the Hubble ratio and $\Omega_\Lambda$. By design it stores no observational numbers, so the forecast cannot be retuned against data after the fact.
A point prediction is a simple named real: a string label together with a value in $\mathbb{R}$. The companion measurement module supplies the early and late Hubble figures used only at test time ($H_{\mathrm{early}}=67.4$, $H_{\mathrm{late}}=73.04$). Those figures never appear in this definition.
The ratio $13/12$ is therefore the pure RS-side claim. Downstream arithmetic multiplies the early measurement by this fraction and checks proximity to the late measurement.
proof idea
Definitional construction only. The declaration builds a point-prediction record whose name is the string "H_late/H_early" and whose value is the real literal $(13:\mathbb{R})/12$. There are no lemmas, tactics, or proof obligations.
why it matters
Feeds the relative-error test hubble_ratio_passes_rel_0p05pct, whose doc-comment states: "RS ratio predicts late from early within 0.05% relative error." That theorem checks
$|H_{\mathrm{early}}\cdot(13/12)-H_{\mathrm{late}}|/H_{\mathrm{late}}<5\cdot10^{-4}$
by pure arithmetic on the measurement-module numbers.
In the Recognition verification pipeline this is the locked forecast half of the Hubble-tension comparison: early-universe $H$ scaled by $13/12$ should recover late-universe $H$ to the stated tolerance. It does not itself derive the fraction from the forcing chain (T0–T8) or from BIT kernel families; it only freezes the number that those layers are expected to justify.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.