alpha_result
plain-language theorem explainer
Packages the RS prediction band for the inverse fine-structure constant against the CODATA 2022 central value and one-sigma uncertainty. Anyone auditing the α⁻¹ confrontation cites this record as the single comparison object. Construction is a pure structure literal: fixed numeric endpoints, no proof obligations.
Claim. The comparison record for $\alpha^{-1}$ with RS interval endpoints $137.030$ and $137.039$, experimental central value $137.035999177$, and experimental uncertainty $2.1\times 10^{-8}$.
background
The module is a quarantined verification layer: it imports experimental PDG/CODATA numbers that are not derived inside Recognition Science, so comparisons stay informational and off the certified surface.
ComparisonResult is a five-field record: a display name, an RS closed interval $(rs_lo, rs_hi)$, and an experimental central value with one-sigma width. Containment of the experimental point in the RS interval is checked by a separate predicate on this record.
In RS-native units the fine-structure target is the open band $(137.030, 137.039)$ forced by the recognition calculus (primer landmark). CODATA 2022 reports $\alpha^{-1}_{\mathrm{exp}} = 137.035999177(21)$, which sits inside that band.
proof idea
Definitional structure literal, not a theorem. The five fields are filled with concrete decimals: RS lo/hi from the certified alpha interval, experimental central and sigma from CODATA 2022. No tactics, no lemmas, no computation at this site.
why it matters
This is the single named payload for the module's headline claim: the RS $\alpha^{-1}$ band contains the measured value. Downstream, alpha_result_contains_exp unfolds the record and discharges containment by norm_num.
In the framework it pins the primer landmark that $\alpha^{-1}$ lies in $(137.030, 137.039)$. The module doc marks the status as CONTAINS experimental value. It does not advance the forcing chain (T0–T8); it only archives the numerical confrontation for auditors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.