alphaInv_RS_center
plain-language theorem explainer
The midpoint of the Recognition Science band for the inverse fine-structure constant is the arithmetic mean of the certified endpoints 137.030 and 137.039, hence 137.0345. Auditors and PDG-comparison proofs cite this center when measuring offset from CODATA. The declaration is a one-line average of the two bound constants.
Claim. The RS interval center for the inverse fine-structure constant is $\alpha^{-1}_{\mathrm{RS,c}} := (\alpha^{-1}_{\mathrm{RS,lo}} + \alpha^{-1}_{\mathrm{RS,hi}})/2$, with $\alpha^{-1}_{\mathrm{RS,lo}} = 137.030$ and $\alpha^{-1}_{\mathrm{RS,hi}} = 137.039$.
background
The module Machine-Verified PDG Comparison is quarantined from the certified surface: it imports experimental CODATA/PDG numbers and reports informational numerical checks, not proof-chain content. Its headline check is that the RS band $137.030 < \alpha^{-1}_{\mathrm{RS}} < 137.039$ contains the CODATA 2022 central value $137.035999177(21)$.
The two endpoints are module-local constants: lower bound $137.030$ and upper bound $137.039$. Those bounds encode the RS native prediction band for $\alpha^{-1}$ (primer: $\alpha^{-1}$ inside $(137.030, 137.039)$). The present definition simply names the midpoint of that closed numerical interval so deviation and equality lemmas can refer to a single real.
proof idea
Definition only: the body is the arithmetic mean of the two endpoint constants. No tactics, no lemmas. A sibling equality theorem later unfolds this definition together with the endpoint defs and discharges $\mathrm{center} = 137.0345$ by norm_num.
why it matters
Gives a single real handle on the RS $\alpha^{-1}$ band so comparison lemmas stay readable. Downstream, the deviation from CODATA is defined as this center minus the CODATA 2022 central value, and a short theorem proves that deviation is negative with absolute value below $0.002$ (RS sits slightly low). A companion equality pins the center exactly at $137.0345$.
In the broader framework this sits on the primer $\alpha$ band landmark, not on the T0–T8 forcing chain. It is verification scaffolding around an already-stated numerical prediction, not a derivation of $\alpha$ itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.