tension_sigma
plain-language theorem explainer
Absolute tension of an experimental central value against the midpoint of a Recognition Science prediction interval, in units of the experimental standard deviation. Verification authors use it when summarizing how many sigma separate PDG or CODATA data from an RS band. The body is a direct arithmetic definition: absolute residual of the experiment from the RS midpoint, divided by exp sigma.
Claim. Given a comparison record with RS interval $[a,b]$, experimental central value $x$, and experimental uncertainty $\sigma>0$, the tension is $\bigl|x - (a+b)/2\bigr|/\sigma$.
background
The module Verification.PDGComparison is an informational, quarantined layer: it imports external PDG/CODATA numbers and reports numerical agreement with RS predictions, but those comparisons are not part of the certified forcing chain.
A comparison record packages one observable: a string name, an RS closed interval $[\mathrm{rs_lo},\mathrm{rs_hi}]$, an experimental central value, and its one-sigma uncertainty. Sibling constants in the same file supply CODATA 2022 $\alpha^{-1}$ and PDG lepton masses, together with the machine-verified RS $\alpha^{-1}$ band $(137.030, 137.039)$.
Tension-in-sigma is the standard experimental shorthand for how far a measured central value sits from a predicted center, normalized by the experimental error bar. Here the predicted center is taken as the arithmetic midpoint of the RS interval.
proof idea
Pure definition, no lemmas. Form the RS midpoint $(\mathrm{rs_lo}+\mathrm{rs_hi})/2$, take the absolute residual against the experimental central value, and divide by the experimental sigma. Noncomputable only because it lives in $\mathbb{R}$.
why it matters
Gives a uniform scalar for every PDG/CODATA versus RS interval comparison in this quarantined verification module (fine-structure constant, lepton masses, and any later observables packed as comparison records). It does not feed the certified T0–T8 forcing chain; the module docs explicitly keep experimental imports off the proof surface. Downstream use count is currently zero, so the def is a reporting primitive rather than a lemma dependency. It complements the containment check on the same record: containment asks whether the experimental point lies inside the RS band, while tension reports the signed distance from the band center in experimental sigma units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.