ComparisonResult
plain-language theorem explainer
Data record packing one observable's RS prediction interval against an experimental central value and one-sigma uncertainty. Downstream PDG checks (containment, tension in sigma, the α⁻¹ bundle) all read this shape. Pure carrier structure with no proof obligations.
Claim. A comparison result is a five-field record: a label, an RS lower endpoint $r_{\mathrm{lo}}$, an RS upper endpoint $r_{\mathrm{hi}}$, an experimental central value $x_{\mathrm{exp}}$, and an experimental standard uncertainty $\sigma_{\mathrm{exp}}$.
background
The module Machine-Verified PDG Comparison is quarantined from the certified surface: it imports external CODATA/PDG numbers and treats numerical agreement as informational, not part of the forcing chain. Its headline check is the inverse fine-structure constant, where RS supplies a machine-verified band $137.030 < \alpha^{-1}_{\mathrm{RS}} < 137.039$ against CODATA 2022 $\alpha^{-1}=137.035999177(21)$.
Sibling constants in the file fix the experimental anchors (CODATA $\alpha^{-1}$ and PDG lepton masses with sigmas) and the RS interval endpoints for $\alpha^{-1}$. Interval containment elsewhere in the stack is the standard predicate $\mathrm{lo}\le x\le\mathrm{hi}$; the comparison layer uses a strict interior check on the experimental center.
This structure is only a typed bundle so those numbers travel together under one name.
proof idea
No proof. The declaration is a structure (five fields: name string, two RS reals, experimental center, experimental sigma). Instantiation is by record literal, as in the α⁻¹ bundle that fills the RS band 137.030–137.039 and the CODATA center and sigma.
why it matters
Gives the PDG layer a uniform handle on each observable so containment and tension can be stated once. Immediate consumers: the α⁻¹ comparison bundle; the predicate that the RS open interval strictly contains the experimental center; and the tension-in-sigma functional (distance from experimental center to the RS midpoint, in units of $\sigma_{\mathrm{exp}}$).
In the broader framework this is the bookkeeping face of the α band cited in the primer (roughly 137.030–137.039). It does not derive α; it only packages the already-computed RS interval against CODATA so the containment claim can be stated and audited. The module itself remains outside the certified forcing chain (T0–T8) because experimental inputs are external.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.