center_in_each_sample
plain-language theorem explainer
For any real center x, every band in the sample-band collection at x contains x. RecogSpec authors use this when checking that predicted values sit inside their own sampling windows. The proof collapses sample membership to the singleton wide band of radius parameter 1 and invokes the wide-band center lemma.
Claim. For every real number $x$ and every closed interval band $b$ in the sample-band set built at $x$, the center lies in the band: $\mathrm{lo}(b)\le x\le\mathrm{hi}(b)$.
background
The RecogSpec.Bands module packages closed real intervals as Band records with endpoints lo and hi, together with width and containment helpers. A wide band around a center $x$ with positive slack parameter $\varepsilon$ is the canonical interval used for tolerance checks; the sibling lemma wideBand_contains_center states that $x$ always lies in that interval when $\varepsilon>0$.
Sample bands for a point $x$ are the finite collection of such intervals attached to a predicted scalar (here realized as the singleton consisting of the wide band with $\varepsilon=1$). The module sits under RecogSpec verification bridges that compare RS-native predictions (mass ladder rungs, $\alpha^{-1}$ windows, dimensional constants) against numerical bands rather than exact equalities.
Upstream dimension and kernel constants appear only as ambient imports; this lemma is pure interval arithmetic and does not depend on the forcing value $D=3$ or BIT kernels.
proof idea
Tactic proof in three beats. Introduce an arbitrary band $b$ with membership hypothesis in the sample set. Unfold the sample-band definition to obtain the equality $b=$ wide band at $x$ with $\varepsilon=1$ (the collection is a singleton). Rewrite and finish by wideBand_contains_center at $\varepsilon=1$, discharging positivity by norm_num.
why it matters
Supplies the elementary centering fact for RecogSpec sampling windows: every predicted scalar is inside each band the sampler attaches to it. That is prerequisite hygiene before comparing RS outputs (phi-ladder masses, the $\alpha^{-1}$ band near $(137.030,137.039)$, eight-tick or $D=3$ arithmetic checks) against numerical envelopes.
No downstream theorems currently cite it in the graph; it is local infrastructure beside wideBand_valid, sampleBandsFor_nonempty, and sampleBandsFor_singleton. It does not itself force dimensions or close a T0–T8 step; it only keeps band bookkeeping honest so later bridge lemmas can treat containment as automatic at the sample center.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.