alpha_summary
plain-language theorem explainer
Human-readable status report for the inverse fine-structure constant: RS proves α⁻¹ lies in [137.030, 137.039], and that interval contains the CODATA 2022 central value 137.035999177(21). Anyone auditing the PDG/CODATA comparison module cites this string as the packaged summary. The body is pure string concatenation of fixed bounds, experimental figures, and the containment claim.
Claim. A fixed report string summarizing the inverse fine-structure constant comparison: Recognition Science proves $137.030 < \alpha^{-1} < 137.039$ (width $\approx 0.009$, about 66 ppm); CODATA 2022 gives $\alpha^{-1}_{\mathrm{exp}} = 137.035999177(21)$; the RS interval contains the experimental value, with RS center $137.0345$ deviating by about $-0.0015$ ($\sim 0.001\%$ of the value).
background
The module Machine-Verified PDG Comparison is quarantined from the certified surface: it imports experimental CODATA/PDG numbers that are not derived inside Recognition Science, and the numerical side-by-side is informational rather than part of the forcing chain.
The key constant is $\alpha^{-1}$. In RS-native units the primer places the prediction inside $(137.030, 137.039)$. Sibling definitions in this file pin the experimental anchors (alphaInv_CODATA_2022 and its $1\sigma$ band) and the machine-verified RS bounds (alphaInv_RS_lo, alphaInv_RS_hi). Containment is recorded as the named comparison that the RS open interval holds the CODATA central value.
Local setting: report strings only. No new physics is proved here; the string packages already-proved interval theorems and published experimental figures for audit readability.
proof idea
Not a proof. The definition is a multi-line string built by successive ++ concatenation. It hard-codes the RS lower/upper bounds (citing the proved inequalities that give 137.030 and 137.039), the CODATA 2022 central value and uncertainty, the containment check, a center-vs-experiment deviation note, and a status paragraph on interval width versus experimental precision. No tactics, no lemmas applied at runtime.
why it matters
This is the human-facing ledger line for the $\alpha$ band landmark in the Recognition framework: the machine-verified RS window $(137.030, 137.039)$ is stated to contain CODATA 2022. The module doc elevates that containment as the key result of the quarantined comparison layer.
No downstream Lean theorems depend on the string (used_by is empty). Its role is audit and documentation: a single printable artifact that ties the proved bound theorems to the experimental reference (Tiesinga et al., CODATA 2022) without pulling experiment into the certified forcing chain (T0–T8, RCL, $\phi$). The closing sentence flags the open tightening path: shrinking the RS width needs sharper $\phi$ and $\pi$ bounds, since theoretical uncertainty still exceeds experiment by many orders of magnitude.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.