Pith. sign in
module module moderate

IndisputableMonolith.Verification.Preregistered.AlphaS.Test

show as:
view Lean formalization →

Wires the frozen RS prediction for the strong coupling α_s(M_Z) to the PDG 2022 measurement and records whether it lies inside the 1σ band. Auditors of the Recognition Science constant ladder cite the pass flag here. The module is a thin structural test: prediction and data stay in separate imports; only this file joins them.

claimThe module checks that the preregistered Recognition Science value of $\alpha_s(M_Z)$ lies inside the one-standard-deviation interval of the PDG 2022 world average, exposing a pass/fail verdict (e.g. $passes\_PDG2022\_1\sigma$).

background

Recognition Science preregisters formulas before they see data. The Core harness enforces that split: Prediction modules must not import measurements; Measurement modules are pure data; only Test modules import both.

Here the observable is $\alpha_s(M_Z)$, the QCD coupling at the Z pole. The Prediction import holds the RS-native formula with no experimental numbers. Measurement_PDG2022 holds the PDG 2022/2024 ballpark central value and uncertainty and is the sole place those numbers may be updated.

This Test module is therefore the only join point. A pass cannot be an artifact of editing the formula after looking at PDG.

proof idea

Definition-and-check module, not a deep proof. It imports the frozen prediction and the PDG 2022 measurement, then builds a boolean or Prop (sibling passes_PDG2022_1sigma) that compares predicted $\alpha_s(M_Z)$ to the measured central value plus-or-minus one sigma. No tactic proof of physics; the content is structural separation plus a numeric band check.

why it matters in Recognition Science

Closes the preregistration loop for the strong coupling inside the Verification domain. Anyone claiming RS-native constants (phi-ladder masses, $\alpha^{-1}$ band, forcing-chain outputs) match experiment without post-hoc tuning needs an auditable leaf like this. Upstream docs state the design goal explicitly: formula frozen before measurement. No downstream used_by edges yet; the module is a terminal verification artifact rather than a lemma feeder.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (1)