AlphaInvBounds
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the numerical values from the Recognition Composition Law or the forcing chain.
- Does not propagate uncertainties or represent the full error distribution.
- Does not update with future CODATA releases or other experimental sources.
- Does not enforce the bounds inside any theorem or derivation.
formal statement (Lean)
133structure AlphaInvBounds where
134 lower : ℝ := 137.035999114 -- -3σ
proof body
Definition body.
135 upper : ℝ := 137.035999240 -- +3σ
136 codata_year : Nat := 2022
137
138/-- **EXTERNAL ANCHOR** -/