Pith. sign in
module module high

IndisputableMonolith.Verification.Preregistered.AlphaInv.Test

show as:
view Lean formalization →

Structural pass/fail test of the preregistered inverse fine-structure constant against CODATA 2022. Anyone auditing the RS alpha claim cites the boolean result here. Prediction and measurement are imported as separate modules so the formula cannot see the data before the check. The argument is a thin harness comparison, not a derivation of alpha itself.

claimThe frozen Recognition Science prediction for $\alpha^{-1}$ is checked against the CODATA 2022 measured value of $\alpha^{-1}$; the module records whether that prediction passes the preregistered acceptance test for the 2022 release.

background

Recognition Science places $\alpha^{-1}$ in a narrow native band near $137.03$–$137.04$. The preregistration harness exists so that claim cannot be tuned after looking at data. Core states the design rule explicitly: predictions live in modules that do not import measurements; measurements are pure data; only tests import both.

The Prediction module holds the frozen $\alpha^{-1}$ formula and intentionally contains no experimental values. Measurement_CODATA2022 is a pure data module for the CODATA 2022 inverse fine-structure constant, meant to be swapped when a later release arrives.

This Test module is the join point. It pulls Core, Prediction, and the 2022 measurement together and exposes the sibling check passes_CODATA2022 as the audit artifact.

proof idea

Not a derivation module. It wires three imports: the preregistration core, the measurement-free alpha prediction, and the CODATA 2022 data module. The live content is the boolean (or Prop) pass check against that release. No algebraic forcing of alpha happens here; the work is structural separation plus a comparison of the frozen prediction to the recorded measurement.

why it matters in Recognition Science

Closes the preregistration loop for $\alpha^{-1}$ under CODATA 2022: formula frozen first, data second, test last. That is the verification-layer counterpart to the framework claim that $\alpha^{-1}$ sits inside $(137.030, 137.039)$. Downstream graph edges are empty from this module, so its role is audit evidence rather than a lemma feeding further proofs. When CODATA updates, only the measurement module should change; this test pattern stays the template for the next release check.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (1)