AlphaInvBounds
plain-language theorem explainer
Alpha inverse bounds structure packages the CODATA 2022 empirical interval for α⁻¹ at ±3σ. Researchers comparing Recognition Science native predictions to measured fine-structure data cite it to anchor the alpha band. The implementation is a record with three default fields for lower limit, upper limit, and reference year.
Claim. The empirical bounds structure for the inverse fine-structure constant consists of the closed interval with lower endpoint 137.035999114, upper endpoint 137.035999240, and reference year 2022.
background
The ExternalAnchors module is the single quarantined location for all empirical calibration data that enters Recognition Science from external sources. Its module documentation states that the cost-first core derives everything from the RCL primitive and must not import this module, creating a mechanical separation between pure cost derivations and experimental anchors. AlphaInvBounds is the structure that holds the specific bounds on α⁻¹.
proof idea
The declaration is a structure definition that supplies default values for its three fields. No lemmas are applied and no tactics are used; it is a direct record declaration with hardcoded numerical constants.
why it matters
This definition supplies the external calibration point for the fine-structure constant, instantiated by the downstream definition alpha_inv_bounds. It anchors the RS-native prediction of α⁻¹ inside the interval (137.030, 137.039) to the 2022 CODATA data, enabling comparison with experiment while preserving the separation policy of the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.