within_sigma
plain-language theorem explainer
Absolute residual between a frozen point prediction and a measured central value is strictly smaller than k times the reported uncertainty (default k = 1). Verification authors cite it when checking RS formulas against PDG or cosmological data under a clean import split. The body is a one-line absolute-value inequality; no proof obligations.
Claim. Given a point prediction with value $v$, a measurement with central value $c$ and uncertainty $\sigma$, and a real scale $k$ (default $1$), the predicate holds precisely when $|v - c| < k\,\sigma$.
background
The preregistered harness keeps predictions and measurements in separate Lean modules so the build graph cannot silently feed data into formulas. Tests alone import both sides. That enforces an auditable freeze of the formula before comparison; it does not claim historical preregistration outside the repo.
A point prediction is a named real value. A measurement here is a named triple: central value plus a one-sigma width. Sibling structures in the same module supply those fields; other Measurement types elsewhere in the monolith (protocol windows, spin axes) are unrelated and not used by this predicate.
proof idea
Definition only. The proposition is the strict inequality comparing the absolute residual of the prediction value against the measurement central value to the product of the scale factor and the reported sigma. Default scale is one, matching ordinary one-sigma checks. No lemmas, tactics, or reductions.
why it matters
Parent sites are the AlphaS PDG2022 one-sigma pass theorem and the Hubble $\Omega_\Lambda$ one-sigma pass theorem. Both unfold this predicate, keep the RS prediction opaque or frozen, and reduce only the measurement payload to a concrete numeric inequality. That pattern is the verification layer's way of checking RS outputs (coupling and cosmological parameters) against external data without contaminating the forcing chain or the native-unit constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.