evalToBands_c
plain-language theorem explainer
Predicate asserting that the light-speed anchor of an RS units pack lies inside at least one interval from a candidate band list. Spec and absolute-layer witnesses cite it as the concrete c-check inside MeetsBands. The body is a one-line existential over Band.contains.
Claim. For RS units $U$ (with light-speed component $U.c$) and a finite list $X$ of closed real intervals, the statement holds iff there exists a band $b\in X$ such that $b.\mathrm{lo}\le U.c\le b.\mathrm{hi}$.
background
RecogSpec packages Recognition Science constants into checkable numerical bands. A Band is a closed real interval $[\mathrm{lo},\mathrm{hi}]$; Bands is just a list of such intervals. Containment is the ordinary predicate $\mathrm{lo}\le x\le\mathrm{hi}$.
RSUnits is the minimal units pack used in Core: tick $\tau_0$, length $\ell_0$, and light speed $c$, linked by $c\cdot\tau_0=\ell_0$. In the RS-native gauge one takes $c=1$, but the band machinery is written against a general pack so that rescaling can be tracked.
The local module builds acceptance witnesses for the absolute layer: whether a bridge's derived anchors fall inside prescribed tolerance bands. The $c$-component is the first such check.
proof idea
Definitional, not a proved theorem. Unfolds to a single existential: some band in the list contains $U.c$ under the ordinary closed-interval predicate. No tactics or upstream lemmas are invoked in the body; downstream lemmas (invariance under units rescaling, wide-band centering, sample-band convenience) expand this definition and discharge the existential by exhibiting an explicit band.
why it matters
This is the atomic $c$-check inside the RecogSpec acceptance stack. MeetsBands is defined as existence of some units pack for which the check succeeds; default and rescaled witnesses (meetsBands_any_default, meetsBands_any_of_eval, meetsBands_any_of_eval_rescaled) all route through it. The absolute-layer constructor absolute_layer_from_eval_invariant lifts a successful check plus a units-rescaling hypothesis to the full UniqueCalibration $\wedge$ MeetsBands pair.
In framework terms it pins the RS-native $c=1$ (and its rescaled images) against numerical tolerance bands, so the light-speed anchor of the forcing chain is not free-floating. Sibling lemmas prove the check is invariant under units rescaling ($c$ fixed by the rescaling relation) and that centered wide bands and sample bands always pass.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.