alpha_inv_uncertainty_eq
plain-language theorem explainer
The CODATA one-sigma uncertainty on the inverse fine-structure constant is exactly $2.1\times 10^{-8}$. Anyone converting an Alpha Genesis residual into a significance in $\sigma$ cites this equality. The proof is pure reflexivity against the external anchor definition.
Claim. The stored CODATA one-sigma uncertainty on $\alpha^{-1}$ equals $0.000000021$ as a real number.
background
This lives in the quarantined Alpha Genesis M7 measurement-verdict module. That module imports empirical CODATA anchors and deliberately is not imported by the forward Alpha Genesis construction, so measurement data never pollute the derivation of $\alpha$.
The external anchor alpha_inv_CODATA_uncertainty is the fixed real $2.1\times 10^{-8}$, the published one-sigma uncertainty on $\alpha^{-1}$. The module's main comparison is the coarse but decisive inequality that the first-order Alpha Genesis value exceeds the CODATA central value by more than $0.0007$. Dividing that certified margin by the one-sigma width yields a $>30000\sigma$ exclusion before any seam correction.
Recognition Science targets $\alpha^{-1}$ inside the band $(137.030, 137.039)$; the measurement verdict here is only about how far the present first-order genesis number sits from the empirical anchor.
proof idea
One-line term proof by rfl. The left-hand side is the external-anchor definition, whose body is literally the real literal $0.000000021$, so definitional equality closes the goal.
why it matters
Without a pinned numerical uncertainty, the module's claim that the certified $0.0007$ overshoot is more than $30000$ one-sigma widths would be informal. This equality freezes the denominator so the $\sigma$-count is a pure arithmetic consequence of the residual theorem.
It supports the quarantine reply to the strongest measurement-side objection: the current first-order Alpha Genesis value is excluded by CODATA before any seam correction is derived. No downstream Lean consumers are recorded yet; the declaration is infrastructure for the measurement-verdict narrative rather than a link in the T0–T8 forcing chain.
Framework context: $\alpha$ is among the RS-native constants (with $c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^{5}/\pi$), and the honest residual status matters for whether the first-order genesis formula already matches the empirical band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.