sampleBandsFor
plain-language theorem explainer
Builds the default one-band sample around a real center x: the singleton list whose only entry is the closed interval [x-1, x+1]. Spec and evaluation lemmas cite it as the canonical tolerance package when checking that a predicted value lands in band. The body is a one-line list constructor wrapping wideBand with fixed half-width 1.
Claim. For any real number $x$, the sample band package at $x$ is the singleton list consisting of the closed interval $[x-1,\,x+1]$.
background
In RecogSpec, a band is a closed real interval with endpoints lo and hi, and a package of bands is simply a list of such intervals. Membership is the usual $b.lo \le x \le b.hi$; validity is $b.lo \le b.hi$.
The helper wideBand x ε builds the symmetric interval $[x-\varepsilon,,x+\varepsilon]$. The present definition freezes the half-width at $1$ and wraps that single band in a list, giving a minimal default tolerance package used throughout the RecogSpec evaluation layer.
A similarly named structure appears in the ILG action module as a consolidated observable-band schema (PPN, lensing, GW); here the name is the list abbreviation, not that structure.
proof idea
Pure definition: return the singleton list whose unique element is wideBand x 1. Marked @[simp], so downstream proofs reduce membership and length goals by unfolding to that constructor. No lemmas are applied in the body itself.
why it matters
This is the default band package for RecogSpec checks. Downstream lemmas prove the list is nonempty of length 1, that the center $x$ lies in its unique band, and that the package satisfies the evalToBands_c predicate when anchors are set to $x$. evalBandsAt is defined by scaling the center and calling this constructor. The Spec layer uses it in meetsBands_any_default, so any "value meets default bands" argument bottoms out here. It is scaffolding for tolerance bookkeeping rather than a forcing-chain step (T0–T8); it does not itself constrain $\phi$, $\alpha$, or the eight-tick structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.