sampleBandsFor_nonempty
plain-language theorem explainer
For any real center, the sample band list is a singleton: its length is exactly one. RecogSpec consumers use this when they need a non-empty, fixed-cardinality band pack rather than an open-ended collection. The proof is a one-line simp unfolding of the sample constructor.
Claim. For every real number $x$, the sample band collection at $x$ is a list of length $1$.
background
In RecogSpec.Bands, a band is a closed real interval used as a tolerance window for Recognition Spec numerical targets (masses, couplings, and related constants). Bands is the list type packing one or more such windows. The helper wideBand x w builds a single band centered at $x$ with half-width controlled by $w$.
sampleBandsFor x is the canonical one-band pack: by definition it is the singleton list [wideBand x 1]. The present lemma records the immediate cardinality fact that this pack always has length one. The imported length notion on traces is not used here; the equality is ordinary list length after unfolding the sample constructor.
proof idea
One-line wrapper: simp [sampleBandsFor] unfolds the @[simp] definition sampleBandsFor x = [wideBand x 1] and closes the goal by the standard fact that a singleton list has length 1.
why it matters
This is local scaffolding hygiene inside RecogSpec band construction. Downstream band validity and containment lemmas (wideBand_valid, wideBand_contains_center, width non-negativity) talk about the geometry of a single window; this lemma guarantees the sample pack exposes exactly one such window, so cardinality side-conditions never branch. No parent theorem currently depends on it in the graph, and it does not touch the forcing chain (T0–T8), RCL, or the alpha band numerics; it only stabilizes the sample API used when wiring RecogSpec checks to BridgeCore.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.