contains_exp
plain-language theorem explainer
Predicate on a comparison record: the experimental central value lies strictly inside the Recognition Science prediction interval. Used by the machine-checked α⁻¹ containment theorem and any later PDG/CODATA checks in this quarantined verification module. The body is a two-sided strict inequality on the four real fields of the record.
Claim. For a comparison record $r$ with RS bounds $r_{\mathrm{lo}}, r_{\mathrm{hi}}$ and experimental central value $x_{\mathrm{exp}}$, the containment predicate holds iff $r_{\mathrm{lo}} < x_{\mathrm{exp}} < r_{\mathrm{hi}}$.
background
The PDGComparison module is quarantined from the certified RS surface: it imports external CODATA/PDG numbers and only reports informational numerical agreement. Its key showcase is inverse fine structure, where the machine-verified RS band $137.030 < \alpha^{-1}{\mathrm{RS}} < 137.039$ is checked against CODATA 2022 $\alpha^{-1}{\mathrm{exp}} = 137.035999177(21)$.
A ComparisonResult packs one observable: a name string, RS lower/upper bounds, experimental central value, and experimental one-sigma. The containment predicate is the Boolean core of that check: whether the experimental center sits strictly inside the RS interval. Sibling constants supply the CODATA α⁻¹ center and sigma and the RS α⁻¹ bounds used to build the α record.
proof idea
Definitional, not a proof. Expands to the conjunction of two strict inequalities on the real fields of the comparison record: RS lower bound below experimental center, and experimental center below RS upper bound. Downstream theorems discharge it by unfolding the concrete record and running norm_num on the numeric literals.
why it matters
Gives a uniform Prop for “RS interval contains experiment” so each observable can share the same statement shape. The immediate consumer is the theorem that the α⁻¹ comparison record satisfies containment, which is the module’s headline verification claim (RS band contains CODATA 2022). That claim sits outside the forcing chain (T0–T8) and the Recognition Composition Law; it is a post-hoc numerical audit of the derived α band against external data, not a step in deriving constants. The same predicate can be reused for lepton-mass or other PDG rows once their RS intervals are filled in.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.