Band
plain-language theorem explainer
A closed real interval is packaged as a pair of endpoints together with its length. Spec authors and bridge verifiers cite it when stating numerical prediction windows (for example the fine-structure band). The declaration is pure data: two real fields and a one-line difference for width.
Claim. A band is a pair of real numbers $(\ell, h)$ interpreted as the closed interval $[\ell, h]$. Its width is the difference $h - \ell$.
background
RecogSpec collects the concrete numerical windows that Recognition Science claims against experiment. A band is the elementary container: lower and upper real endpoints, nothing more.
Upstream, the primitive recognition calculus already works with rational intervals (RatInterval) whose width is hi - lo and whose endpoints are projected to reals via DeltaReal.lo / hi. The present structure lifts that idea to bare reals so that finished predictions (masses, couplings, dimensionless ratios) can be stated without carrying rational approximation data.
Sibling constructors such as wideBand and sampleBandsFor build concrete instances; the structure itself only fixes the type.
proof idea
No proof. The structure declares two real fields. Width is the abbreviation b.hi - b.lo, mirroring the rational-interval width already defined in DeltaReal.
why it matters
Every quantitative RS claim that is checked against data is ultimately a membership statement inside a band (the alpha inverse window near 137.03–137.04 is the canonical example). The structure is the common carrier for those windows inside RecogSpec and the verification bridge. It does not itself force any constant; it only standardizes the interval type that later band lemmas (wideBand_valid, containment of center/lo/hi, sample non-emptiness) reason about.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.