pith. machine review for the scientific record. sign in
def definition def or abbrev high

alpha_inv_bounds

show as:
view Lean formalization →

alpha_inv_bounds supplies the CODATA 2022 ±3σ interval for the inverse fine-structure constant as a quarantined external anchor. Researchers comparing Recognition Science predictions against experiment cite this single calibration seam. The definition is a direct structure instantiation that populates the lower, upper, and year fields from their declared defaults.

claimThe inverse fine-structure constant satisfies $137.035999114 < α^{-1} < 137.035999240$ at the 3σ level according to CODATA 2022 data.

background

The ExternalAnchors module is the single quarantined location for all empirical calibration data that enters Recognition Science from external sources. Its policy requires that the cost-first core never imports this module, preserving a mechanical separation between pure RCL derivations and measured constants. AlphaInvBounds is the structure that records the lower bound 137.035999114, upper bound 137.035999240, and codata_year 2022 for α^{-1}.

proof idea

The definition is a one-line structure instantiation that supplies the default values declared inside AlphaInvBounds.

why it matters in Recognition Science

This anchor supplies the experimental interval against which RS-native predictions for α^{-1} are compared. It directly implements the framework statement that α^{-1} lies inside (137.030, 137.039). No downstream theorems yet reference it, leaving open its eventual use in coupling or mass-ladder derivations.

scope and limits

formal statement (Lean)

 139def alpha_inv_bounds : AlphaInvBounds := {}

proof body

Definition body.

 140
 141end FineStructure
 142
 143/-! ## Particle Masses
 144
 145**EXTERNAL ANCHOR SECTION**
 146
 147Dimensionless mass ratios (from PDG 2024 / CODATA 2022).
 148-/
 149
 150section MassRatios
 151
 152/-- **EXTERNAL ANCHOR**: Electron mass (CODATA 2022).
 153    m_e = 9.1093837139(28) × 10⁻³¹ kg
 154    m_e = 0.51099895069(16) MeV/c² -/

depends on (3)

Lean names referenced from this declaration's body.