alpha_CODATA_uncertainty
plain-language theorem explainer
alpha_CODATA_uncertainty supplies the one-sigma uncertainty on the fine structure constant drawn from CODATA 2022. Researchers comparing Recognition Science predictions against laboratory measurements would reference it when quantifying agreement between the derived alpha interval and observed values. The declaration is a direct numerical assignment of a real number with no computation or lemmas required.
Claim. The one-sigma uncertainty in the fine structure constant is given by $1.1 times 10^{-12}$.
background
The ExternalAnchors module is the single quarantined location for all empirical calibration data entering Recognition Science. Its policy enforces that the cost-first core never imports this module, creating a mechanical separation between pure RCL derivations and external comparisons. The upstream constant definition from Relativity.Fields.Scalar constructs a scalar field with constant value, providing the embedding mechanism used for numerical anchors throughout the framework.
proof idea
The definition is a direct numerical binding of the real number 0.0000000011e-3.
why it matters
This anchor enables quantitative comparison between the RS-native alpha band and CODATA data while preserving the independence of the RCL core. It implements the external calibration policy stated in the module documentation, allowing importing modules to test predictions against experiment. No downstream uses are recorded, leaving open how the phi-ladder mass formula will be confronted with this uncertainty band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.