Pith. sign in
module module moderate

IndisputableMonolith.Verification.Preregistered.AlphaS.Prediction

show as:
view Lean formalization →

Preregistered prediction module for the strong coupling: it freezes α_s = 2/17 with no measurement imports. The α_s(M_Z) test suite cites this value as the locked formula. Content is a pure prediction definition plus an equality lemma identifying it with 2/17.

claimThe frozen Recognition Science prediction for the strong coupling is $\alpha_s = 2/17$, declared in a module that does not import measurement data.

background

Under the preregistered test harness, predictions, measurements, and tests live in separate modules. Prediction modules must not import measurement modules, so the formula is structurally frozen before any comparison to data. Tests alone import both sides.

This module sits on that prediction side for the strong coupling $\alpha_s$. It imports the preregistered core and the alpha-construction constants layer (cubic-ledger seed assembly for the EM sector; exact infrared $\alpha^{-1}(0)$ remains an open boundary condition there). The strong-coupling prediction itself is the simple rational $2/17$, exposed as a named prediction object and an equality lemma.

No running or scheme evolution is performed here; the module only locks the number the downstream match test will use.

proof idea

Definition-and-equality module, not a derivation chain. It introduces the prediction constant and a one-line (or short) lemma equating that constant to $2/17$. There is no tactic-heavy argument and no appeal to measurement lemmas. Structural force comes from the import graph: measurement modules are absent, matching the preregistered core design.

why it matters in Recognition Science

Feeds Verification.Preregistered.AlphaS.Test, whose stated goal is a within-$1\sigma$ match of $\alpha_s(M_Z)$ against the frozen prediction. Without this module, the test could not separate formula from data. In the broader RS verification layer it is the strong-coupling counterpart of preregistered EM-alpha checks: a locked rational target, not a post-hoc fit. It does not close the open exact-$\alpha^{-1}(0)$ boundary-condition question in the EM alpha-derivation stack; it only supplies the $\alpha_s$ side of the preregistered harness.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (2)