meetsBands_any_default
plain-language theorem explainer
For any ledger, bridge, and RS units pack U, the sample bands centered on U's speed c satisfy bands acceptance. Calibration and verification paths cite this as the default witness that band checks pass when bands are built around the units' own c. The proof takes the center-in-band fact for U.c and lifts it through the existential MeetsBands constructor.
Claim. For every ledger $L$, bridge $B$ on $L$, and RS units pack $U$, the sample bands centered at the speed $U.c$ meet the bands-acceptance condition: there exist units for which the $c$-band evaluation succeeds on those sample bands.
background
In RecogSpec, physical constants are packaged as RS units: a triple $(\tau_0, \ell_0, c)$ with the structural constraint $c \cdot \tau_0 = \ell_0$. Bands are tolerance windows around displayed quantities. The bands-acceptance predicate asserts that there exists some units pack making the $c$-band evaluation succeed on a given band set $X$.
Sample bands for a speed value $x$ are the default windows centered on $x$. The lemma supplies a canonical acceptance witness: when the band set is exactly the samples built from $U.c$ itself, acceptance is automatic for that $U$.
The local setting is the RecogSpec specification layer tying ledgers and bridges to calibrated units and band checks. Absolute-layer acceptance later bundles unique calibration with this bands predicate.
proof idea
Invoke the center-in-sample-bands fact at $x = U.c$ to obtain a concrete band $b$ in the sample set with $U.c$ inside $b$. Package that triple as a $c$-band evaluation witness for $U$ against the sample bands of $U.c$. Finish by the any-of-eval lemma, which turns any such evaluation witness into the existential bands-acceptance predicate (the ledger and bridge are parametric and unused in the witness).
why it matters
Bands acceptance is the band half of absolute-layer acceptance, which the module pairs with unique calibration. This default witness closes the common case where bands are the samples centered on the units' own $c$, so verification paths need not hand-build custom band data. It lives in the RecogSpec layer that connects RS-native units (native gauge $c = 1$) to displayed calibration checks against tolerance windows. No recorded downstream dependents yet; the lemma is a ready default for any absolute-layer or bridge-certification argument that requires bands acceptance on sample bands.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.