center_in_sampleBandsFor
plain-language theorem explainer
For any real $x$, the default sample band list built from $x$ contains at least one band that contains $x$. Spec and bridge authors cite it when they need a free meets-bands witness for a constant (typically $c$). The proof exhibits the width-1 wide band and reuses the center-containment lemma.
Claim. For every real number $x$, there exists a band $b$ belonging to the sample band list of $x$ such that $\mathrm{lo}(b)\le x\le\mathrm{hi}(b)$.
background
In RecogSpec.Bands, a band is a closed real interval with endpoints lo and hi. The constructor wideBand x ε builds the symmetric interval $[x-\varepsilon,x+\varepsilon]$. Containment is the standard predicate $\mathrm{lo}\le x\le\mathrm{hi}$ (imported from the interval numerics layer).
The sample band list for a point $x$ is defined by simplification as the singleton list whose only entry is the width-1 wide band around $x$. Upstream, wideBand_contains_center already records that whenever $\varepsilon\ge 0$, the center $x$ lies in wideBand x ε.
This module supplies the band infrastructure used by Recognition Spec checks that a ledger/bridge pair meets prescribed numerical bands on RS units.
proof idea
Term-style existence proof via refine. The witness band is wideBand x 1. Membership in sampleBandsFor x is immediate by unfolding the simp definition (singleton list). Containment of the center follows from wideBand_contains_center at $\varepsilon=1$, with nonnegativity of $1$ discharged by norm_num, then rewritten by simpa.
why it matters
Feeds the default meets-bands witness meetsBands_any_default in RecogSpec.Spec, whose doc-comment states it supplies a "Default meets-bands witness using the sample bands centred on U.c." That lemma unpacks this existence result at $x=U.c$ and packages it as an evalToBands_c certificate.
In the Recognition framework this is scaffolding for Spec-level checks that RS units (here the speed of light in RS-native units, $c=1$) land inside declared numerical bands. It does not itself force any physical constant; it only guarantees the sample band list is a valid default target for such checks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.