passes_PDG2022_1sigma
plain-language theorem explainer
The Recognition Science prediction for the strong coupling α_s(M_Z) equals 2/17 and lies inside the PDG 2022 one-sigma band. Anyone auditing the preregistered α_s verification cites this pass/fail certificate. The proof freezes the formula via a rewrite, expands the measurement payload, and discharges the inequality by norm_num.
Claim. The preregistered RS prediction for $\alpha_s(M_Z)$ (equal to $2/17$) lies within one standard deviation of the PDG 2022 measured central value and uncertainty.
background
This module is the pass/fail test for the strong coupling at the Z pole inside the preregistered verification layer. Predictions and measurements are kept in separate modules so that a PDG update only touches the measurement file; the RS formula stays frozen.
The predicate within_sigma (from the preregistered core) asserts that a predicted real value falls inside the closed interval formed by a measured central value plus or minus its reported one-sigma error. The α_s prediction is the exact rational $2/17$. The companion fine-structure band lives in a sibling AlphaInv prediction module with interval $(137.030, 137.039)$ and is not used here.
Local setting is purely numerical verification: no forcing-chain or ledger geometry is invoked in the proof body. Upstream gravity and foundation edges appearing in the dependency graph are incidental name collisions, not logical inputs to this certificate.
proof idea
Term-mode tactic script. Unfold the within_sigma predicate to a concrete numeric membership statement. Rewrite the prediction definition by prediction_eq_two_over_17, locking the claim to the rational $2/17$. Simplify away the measurement record constructor for PDG 2022, exposing the central value and sigma as concrete floats or rationals. Finish with norm_num, which decides the resulting closed-interval inequality by exact arithmetic.
why it matters
Closes the preregistered α_s(M_Z) match test for PDG 2022 at one sigma. In the Recognition framework this is an external consistency check on a dimensionless coupling fixed by the same phi-ladder and cost structure that forces α^{-1} into the narrow band near 137 and sets the mass yardstick. No downstream theorems currently depend on it (used_by is empty); it is a leaf certificate meant for auditors and for regression when the measurement module is swapped after a PDG release.
It does not itself derive $2/17$ from the forcing chain (T0–T8) or the Recognition Composition Law; that derivation lives in the prediction module. The test only certifies agreement with the published experimental band under the frozen formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.