meetsBands_any_param
plain-language theorem explainer
For any ledger, bridge, RS units pack, and nonnegative tolerance, a singleton wide band centered on that pack's speed of light is accepted by the RecogSpec band checker. Calibration and acceptance wiring cite this as the default meets-bands witness. The proof evaluates the centered band, then packages the given units pack as the existential witness.
Claim. Let $L$ be a ledger, $B$ a bridge on $L$, $U$ an RS units pack, and $\mathrm{tol}\ge 0$. Then $\mathrm{MeetsBands}(L,B,[\mathrm{wideBand}(U.c,\mathrm{tol})])$ holds: there exists a units pack for which the band evaluation on the singleton list of a wide band centered at speed $U.c$ with half-width $\mathrm{tol}$ succeeds.
background
RecogSpec packages the Recognition Science calibration interface: anchors determine a speed, units packs carry $(\tau_0,\ell_0,c)$ with $c\cdot\tau_0=\ell_0$, and band lists encode acceptance windows on displayed constants.
MeetsBands L B X is the acceptance witness: there exists some Constants.RSUnits pack such that evalToBands_c succeeds on the band list $X$. A wide band centered at a reference speed with nonnegative half-width is the default tolerance window around the units pack's own $c$.
The local setting is the Spec layer over Core, Anchors, and Bands: once units are fixed, one needs a trivial positive witness that a centered band around $U.c$ is met, independent of the particular ledger and bridge.
proof idea
Two-step term-style proof. First apply evalToBands_c_wideBand_center at the given units pack $U$ and tolerance $\mathrm{tol}\ge 0$ to obtain successful band evaluation of the singleton list $[\mathrm{wideBand}(U.c,\mathrm{tol})]$. Then feed that evaluation fact into meetsBands_any_of_eval, which turns a concrete successful evaluation at $U$ into the existential MeetsBands witness for arbitrary ledger and bridge. No case splits; the ledger and bridge are parametric dummies.
why it matters
Supplies the default meets-bands witness used whenever RecogSpec only needs a centered tolerance window on $c$, rather than a tight multi-band certificate. It closes the gap between the pure evaluation lemma on wide bands and the existential acceptance predicate that Spec consumers quantify over.
In the broader framework this sits under calibration uniqueness and anchors transport (siblings such as UniqueCalibration, AnchorsEqv, unitsFromAnchors_calibrated): once anchors fix a speed and units, a nonnegative tolerance band around that speed is automatically met. No downstream consumers are recorded yet; the lemma is infrastructure for band-acceptance APIs rather than a forcing-chain step (T0–T8). It does not touch mass ladders, $\alpha$ bands, or eight-tick structure directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.