meetsBandsChecker
plain-language theorem explainer
Specialized Boolean checker: given a list of real anchors and a center, decide whether those anchors meet the unit-width band family at that center. Spec and verification code cite it when testing RS-native constants against predicted bands. One-line wrapper that feeds the generic checker the bands from evaluating at the center with width parameter 1.
Claim. For a finite list of real anchors $x_s$ and a center $c \in \mathbb{R}$, return the Boolean that is true precisely when $x_s$ meets the candidate bands obtained by evaluating the band family at $c$ with width parameter $1$.
background
The RecogSpec.Bands module packages interval bands used to check whether Recognition Science predictions land inside stated numerical windows (for example the fine-structure band around $\alpha^{-1}$). A band is a closed real interval; families of bands are built from a center and a width recipe such as the wide-band constructors in this module.
The generic predicate (sibling) walks a list of anchors against an explicit band list and returns a Boolean. Separately, evalBandsAt materializes the candidate band list at a chosen center and scale. The RS-native units package fixes $c=1$ in the native gauge ($\tau_0$ one tick, $\ell_0$ one voxel), so band checks are often run in that gauge.
This definition is the fixed-width specialization: width parameter locked to $1$, center supplied by the caller.
proof idea
One-line definitional wrapper. It applies the generic list-vs-bands checker to the input list together with the band list produced by evaluating bands at the given center with width parameter $1$. No separate proof obligations; the body is pure composition of those two siblings.
why it matters
Gives the default entry point for band membership tests in the RecogSpec layer: callers pass anchors and a center without assembling bands by hand. Downstream, the simp lemma for the empty list records that the checker returns false on [], which anchors list induction and simplification in verification scripts.
In the broader framework this sits with numerical band claims (constants in RS-native units, the $\alpha^{-1}$ window near $137.03$–$137.04$) rather than with the forcing chain T0–T8 itself. It is plumbing for spec checks, not a derivation of $\phi$, the eight-tick octave, or $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.