meetsBandsCheckerP
plain-language theorem explainer
Minimal predicate asserting that a choice of RS units satisfies a prescribed list of numerical bands on the displayed speed of light. Spec authors cite it when a concrete units witness must be lifted to the abstract MeetsBands relation. The body is a one-line alias of the c-component band evaluator.
Claim. For RS units $U=(\tau_0,\ell_0,c)$ with $c\,\tau_0=\ell_0$ and a list of bands $X$, the checker holds if and only if the speed component of $U$ lies inside the bands obtained by evaluating $U$ against $X$ (the $c$-band check).
background
RecogSpec packages the Recognition Science bridge as a checkable specification: anchors fix a units gauge, bands are closed real intervals, and a ledger/bridge pair is said to meet bands when some admissible units witness lands inside those intervals.
RS units are the triple $(\tau_0,\ell_0,c)$ with the structural law $c,\tau_0=\ell_0$. Bands are simply lists of intervals; membership is the usual $b.lo\le x\le b.hi$. The upstream evaluator evalToBands_c is the concrete $c$-component test that compares the displayed speed of a units record against a band list.
This definition sits in the Spec module as the thinnest Prop-level handle on that evaluator, so downstream lemmas can talk about "the checker" without repeating the evaluation call.
proof idea
Pure definitional alias: the predicate is definitionally equal to the $c$-band evaluator applied to the same units and band list. No tactics, no lemmas, no proof obligations.
why it matters
Gives Spec a named, stable Prop for the minimal $c$-band check. Downstream, meetsBands_any_of_checker lifts an existential witness of this checker to the abstract MeetsBands relation on a ledger/bridge pair, and meetsBandsCheckerP_invariant records that the checker is unchanged under units rescaling. Together they let calibration and band-meeting arguments factor through a single lightweight interface rather than inlining the evaluator everywhere.
In the broader RS stack this is bookkeeping, not a forcing step: it does not touch T5–T8, the RCL, or the mass ladder. It only stabilizes the units/bands layer that later certificates (Born rule, display constants) consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.