IndisputableMonolith.Verification.Preregistered.AlphaInv.Test
Preregistered pass/fail check that the RS inverse fine-structure prediction lies inside the CODATA 2022 α⁻¹ band. Anyone auditing the frozen-before-data claim for α cites this module. Structure is a thin test harness: import prediction and measurement separately, then assert the numerical containment via the core preregistration API.
claimThe preregistered RS prediction for $\alpha^{-1}$ is tested against the CODATA 2022 measured value: the predicted interval must contain the reported $\alpha^{-1}$ (within the stated uncertainty). The module exposes a Boolean pass flag for that containment.
background
Recognition Science fixes $\alpha^{-1}$ in a narrow band near $137.03$–$137.04$ from the forcing chain and the Recognition Composition Law, without fitting to QED data. The preregistration harness (Core) enforces a structural split: prediction modules must not import measurement modules, measurement modules are pure data, and only test modules may import both.
This Test module is the α⁻¹ instance of that pattern. Upstream, Prediction holds the frozen RS formula and claimed interval with no experimental numbers. Measurement_CODATA2022 is a pure data module for the CODATA 2022 release of $\alpha^{-1}$, intended to be swapped when a later CODATA value appears.
The sibling passes_CODATA2022 is the concrete Boolean that records whether the frozen prediction covers the 2022 datum.
proof idea
This is a verification/test module, not a derivation. It wires three imports: Core (harness API), Prediction (frozen $\alpha^{-1}$ claim), and Measurement_CODATA2022 (pure CODATA numbers). The argument is a numerical containment check: evaluate whether the preregistered predicted band includes the measured central value (to the stated uncertainty). No new physics lemmas are proved here; the module only certifies the pass/fail bit against the frozen inputs.
why it matters in Recognition Science
In the RS stack, $\alpha^{-1}$ is a landmark constant (primer band $(137.030, 137.039)$). Preregistration is how the project claims the formula was fixed before looking at the datum. This module is the audit point for that claim on α: Prediction stays measurement-free, Measurement stays formula-free, and Test alone joins them.
No downstream Lean dependents are listed; the consumer is the verification layer and human auditors of the α prediction. When CODATA updates, only the measurement module changes; the prediction and this test pattern stay put. That separation is the point of the Core design goal “formula frozen before measurement.”
scope and limits
- Does not derive or re-prove the RS formula for α⁻¹.
- Does not import or mix prediction algebra into the CODATA data module.
- Does not claim agreement with pre-2022 or post-2022 CODATA releases.
- Does not bound QED higher-order terms or experimental systematics beyond the stated CODATA uncertainty.
- Does not feed other Lean theorems; used_by is empty.