alpha_inv_CODATA_uncertainty
plain-language theorem explainer
This definition supplies the one-sigma uncertainty on the inverse fine-structure constant taken from CODATA 2022. RS modelers cite it when populating the EmpiricalAnchors record to benchmark phi-ladder predictions against laboratory alpha values. The declaration is a direct constant binding with no reduction steps.
Claim. The one-standard-deviation uncertainty on the CODATA value of the inverse fine-structure constant is given by the real number $0.000000021$.
background
The module isolates all external calibration data so the Recognition Composition Law core remains independent of measurement. This definition provides the uncertainty term that fills the alpha_inv_sigma field inside the EmpiricalAnchors structure. The module policy requires that the cost-first derivations never import these values, preserving a mechanical separation between RS-native constants and empirical anchors.
proof idea
The declaration is a noncomputable definition that directly binds the identifier to the literal real number 0.000000021.
why it matters
It supplies the numerical uncertainty required by the EmpiricalAnchors structure, enabling direct numerical comparison between Recognition Science predictions (derived from the Recognition Composition Law and the phi fixed point) and the measured alpha band. The placement keeps the T0-T8 forcing chain free of external data while exposing the calibration seam needed for falsifiability checks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.