alphaInv_RS_center_eq
plain-language theorem explainer
The Recognition Science inverse fine-structure interval is centered at 137.0345. Anyone comparing the RS α⁻¹ band to CODATA would cite this equality as the fixed midpoint. The proof unfolds the midpoint of the certified lo/hi endpoints and finishes by decimal arithmetic via norm_num.
Claim. The center of the Recognition Science prediction interval for the inverse fine-structure constant equals $137.0345$.
background
This module holds machine-checked numerical comparisons between Recognition Science predictions and PDG/CODATA values. It is quarantined from the certified surface: experimental inputs are informational, not part of the derivation chain.
The RS band for the inverse fine-structure constant is the open interval $(137.030, 137.039)$, the framework landmark for $\alpha^{-1}$. The center is the arithmetic midpoint of the certified lower and upper endpoints of that interval. CODATA 2022 reports $\alpha^{-1}_{\mathrm{exp}} = 137.035999177(21)$, which lies inside the RS window.
proof idea
Computational one-shot. Unfold the definitions of the RS center and of its lower and upper endpoints, then apply norm_num to evaluate the midpoint arithmetic to the decimal $137.0345$. No external lemmas are required beyond those definitions.
why it matters
Fixes the numerical midpoint of the RS $\alpha^{-1}$ band used throughout the PDG comparison module. The module's headline check is that the machine-verified RS interval contains the CODATA 2022 central value; this equality makes the midpoint explicit for the subsequent deviation-from-CODATA quantity. It sits on the primer landmark that $\alpha^{-1}$ lies in $(137.030, 137.039)$. The current dependency graph shows no downstream theorem edges, so the result is a local numerical anchor rather than a link in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.