sampleBandsFor_singleton
plain-language theorem explainer
For any real center $x$, the sample band list at $x$ is exactly the singleton list whose only entry is the width-$1$ interval about $x$. Anyone rewriting or simplifying band-list equalities in RecogSpec cites this. The proof is a one-line `simp` unfolding of the definition.
Claim. For every real number $x$, the sample band collection at $x$ equals the one-element list consisting of the closed interval $[x-1, x+1]$.
background
RecogSpec packages numerical targets as bands: closed real intervals with lower and upper endpoints. A wide band about a center $x$ with half-width $\varepsilon$ is the interval $[x-\varepsilon, x+\varepsilon]$.
The sample band list at $x$ is defined to be the singleton list containing the wide band of half-width $1$ about $x$. That definition is marked @[simp], so equality lemmas that merely restate it are available for automatic rewriting.
The local module sits in the verification bridge layer: bands are the containers against which predicted constants and observables are checked for membership.
proof idea
One-line wrapper. Unfold sampleBandsFor by simp; the goal is definitionally the right-hand side, so the equality closes immediately. No arithmetic or interval reasoning is required.
why it matters
The lemma pins the concrete shape of the default sample: one band of half-width $1$ about the supplied center. Downstream band non-emptiness and containment facts in the same module rely on that shape being a singleton list rather than an open-ended collection.
No external parent theorem currently depends on it (empty used-by). It is local hygiene for RecogSpec band rewriting, not a step in the T0–T8 forcing chain. It does not touch mass ladders, $\alpha$, or the Recognition Composition Law; it only stabilizes the band-list API used when bridging predicted reals into interval checks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.