PointPrediction
plain-language theorem explainer
A point prediction is a named real-valued forecast used by the preregistered verification harness. Anyone wiring a frozen RS formula (strong coupling, Hubble ratio, dark-energy density) into an auditable Lean test cites this carrier. It is a two-field structure: a string label and a real value, with no proof obligations.
Claim. A point prediction is a pair consisting of a string label and a real number value (the forecast).
background
The Preregistered Test Harness enforces “formula frozen before measurement” inside the Lean build graph. Prediction modules must not import measurement modules; measurements are pure data; tests import both. That separation does not prove historical preregistration, but it makes silent data dependence structurally impossible.
A point prediction packages a human-readable name with a single real forecast. Sibling carriers in the same module include interval predictions and measurements. The comparison predicate within_sigma takes a point prediction and a measurement and asserts that the absolute residual is strictly less than $k$ times the reported sigma (default $k=1$).
proof idea
Pure structure definition: two fields, a String name and a real val. No constructors beyond the default, no axioms, no proof body.
why it matters
This is the standard carrier for frozen RS point forecasts in the verification layer. Downstream instances include the strong-coupling forecast $\alpha_s(M_Z)=2/N_{\mathrm{wallpaper}}$, the late-to-early Hubble ratio $H_{\mathrm{late}}/H_{\mathrm{early}}=13/12$, and $\Omega_\Lambda=11/16-\alpha/\pi$. The harness predicate that checks agreement with data consumes this type. It sits under the Verification domain and supports auditable preregistration of RS-native constants and cosmology ratios without claiming historical lock-in.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.