Bands
plain-language theorem explainer
A band list is simply a finite list of closed real intervals, each carrying a lower and upper endpoint. Recognition Spec uses this type as the carrier for candidate windows on dimensionless observables (notably the speed of light in RS units). Anyone checking whether an evaluated constant lands inside an allowed window cites it. The declaration is a one-line type synonym for List of Band.
Claim. Write $\mathrm{Bands}$ for the type of finite lists of closed real intervals (bands). Each band is a pair of reals $(\ell,h)$ with width $h-\ell$; a list of such pairs is the ambient type on which membership and checker predicates are later defined.
background
In RecogSpec, a single band is the structure with real endpoints $\ell$ (lo) and $h$ (hi). Its width is $h-\ell$. Validity means $\ell\le h$; containment of a real $x$ means $\ell\le x\le h$. These notions are packaged so that later checkers can ask whether an evaluated constant sits inside any listed window.
The module sits in the Recognition Spec layer that bridges RS units to verifiable numerical claims. It imports Mathlib and the verification bridge core. An upstream namesake in Relativity.ILG.Action is a different structure (fixed $\kappa$ slots for PPN, lensing, GW); the present synonym is the lightweight list-of-intervals carrier used by RecogSpec evaluators.
Sibling helpers build a wide unit-width band about a center, sample a singleton list of such bands, and decide containment. The list type is what those helpers return and what the Spec absolute-layer predicates consume.
proof idea
One-line abbreviation: Bands is defined to be List Band. There is no proof obligation; the body is the type synonym itself. Downstream lemmas unfold the synonym and work with ordinary list membership and the Band.contains / Band.Valid predicates defined immediately below in the same module.
why it matters
This carrier is the common type for every RecogSpec band check. Downstream, sampleBandsFor builds a singleton wide band, evalBandsAt scales a center by a constant, and evalToBands_c asks whether the RS-units speed of light $U.c$ lies in any listed band. The invariance lemma evalToBands_c_invariant then shows that units rescaling (with $c$ fixed by the bridge) preserves the check.
Higher up, Spec.absolute_layer_any and absolute_layer_from_eval_invariant thread these band lists into the absolute recognition layer: observables must land inside declared windows. In the broader framework this is how numerical claims (for example the $\alpha^{-1}$ band near 137, or $c=1$ in RS-native units) are stated as finite interval membership rather than bare equalities, keeping the verification bridge decidable and units-invariant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.