MeetsBands
plain-language theorem explainer
Bands acceptance is the existence of an RS units pack whose speed of light lands inside a prescribed band set. Spec authors cite it when packaging absolute-layer checks that couple unique calibration to numerical band membership. The body is a one-line existential over the c-band evaluator.
Claim. Given a ledger $L$, a bridge $B$ from $L$, and a band set $X$, the bands-acceptance predicate holds if and only if there exists an RS units pack $U=(\tau_0,\ell_0,c)$ with $c\,\tau_0=\ell_0$ such that the $c$-band checker succeeds for $U$ on $X$.
background
RecogSpec packages the Recognition Science bridge from an abstract ledger to laboratory units. An RS units pack is the minimal triple $(\tau_0,\ell_0,c)$ with the structural law $c,\tau_0=\ell_0$; it is the Core carrier for converting dimensionless RS predictions into SI-facing numbers.
Bands are admissible intervals (or collections of intervals) placed on those converted observables. The c-band evaluator evalToBands_c asks whether the pack's speed $c$ lies in the supplied band set. Ledger and Bridge parameters thread the ambient recognition structure but do not appear in the existential body of this predicate; they fix the ambient context in which units and bands are interpreted.
Sibling material in the same module treats anchors, calibration uniqueness, and transport of units under rescaling. MeetsBands is the pure band half of that stack: a witness that some concrete units pack clears the numerical gates.
proof idea
Definitional, not a proved theorem. The predicate is the bare existential $\exists U:\mathrm{RSUnits},;\mathrm{evalToBands}_c(U,X)$. Downstream lemmas such as meetsBands_any_of_eval are one-line introductions of that pair, and meetsBands_any_default builds a witness from sample bands centred on $U.c$.
why it matters
Absolute-layer acceptance is defined as the conjunction of unique calibration and bands acceptance. Downstream theorems absolute_layer_any, absolute_layer_invariant, and absolute_layer_from_eval_invariant all take MeetsBands as a hypothesis or construct it from a concrete c-band checker, including under admissible units rescaling.
In the Recognition framework this is the numerical gate on the bridge: after the forcing chain fixes dimensionless structure (phi, eight-tick octave, $D=3$), laboratory comparison still needs units packs whose $c$ (and related displays) sit inside declared bands. MeetsBands is that gate as a Prop, so absolute-layer certificates can be stated without baking in a particular units choice.
It does not itself prove any constant lands in the alpha band or mass ladder; it only names the witness shape those later checks inhabit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.