alpha_inv_bounds
plain-language theorem explainer
This definition supplies the CODATA 2022 empirical bounds for the inverse fine-structure constant within three standard deviations. Researchers aligning Recognition Science predictions for couplings and masses with experiment cite these anchors for calibration. The implementation populates the AlphaInvBounds structure with its default lower and upper limits in a single line.
Claim. The inverse fine-structure constant satisfies $137.035999114 ≤ α^{-1} ≤ 137.035999240$ (CODATA 2022, ±3σ).
background
ExternalAnchors is the quarantined module that holds all empirical calibration data entering Recognition Science. It enforces a mechanical separation so that the cost-first core, built on the Recognition Composition Law, never imports measurements. AlphaInvBounds is the record type that stores the lower bound, upper bound, and codata_year for α^{-1} at the three-sigma level.
proof idea
The declaration is a definition that constructs an AlphaInvBounds instance by supplying the default field values for the empirical bounds on α^{-1}. No tactics or lemmas are applied; it directly uses the structure's built-in defaults.
why it matters
This anchor supplies the measured interval for α^{-1} that Recognition Science predictions must match, consistent with the framework interval (137.030, 137.039). It completes the external calibration seam in the constants layer without feeding into any listed downstream theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.