evalBandsAt
plain-language theorem explainer
Scales a real sample point by a constant and returns the corresponding singleton band list. Anyone wiring RecogSpec band checks against scaled anchors (for example c times a unit sample) cites this. The body is a one-line simp abbreviation of sampleBandsFor on the product.
Claim. For real numbers $c$ and $x$, the evaluated band list at scale $c$ and sample $x$ is the singleton list of the wide band of relative width $1$ centered at $c\cdot x$.
background
In RecogSpec.Bands, a band is a closed real interval with lower and upper endpoints, and a band list is just a list of such intervals. Validity means the lower endpoint does not exceed the upper; containment is ordinary closed-interval membership.
The local sampling primitive builds a singleton list: one wide band of relative width parameter $1$ centered at a given real. That is the only band shape used at this layer. A separate Relativity.ILG.Action structure also named Bands packages PPN, lensing, and GW tolerance coefficients; it is a different schema and is not the return type here.
The present definition simply feeds the product $c\cdot x$ into that sampler, so band centers track a linear rescaling of the sample.
proof idea
One-line definitional wrapper: return the sample-band list for the product $c\cdot x$. Marked simp so downstream rewrites unfold it automatically to the underlying singleton wide-band construction.
why it matters
Feeds the RecogSpec band checker: meetsBandsChecker on a list of anchors at constant $c$ evaluates the checker against the band list obtained by scaling the unit sample. That checker asks whether the anchors lie in any of the candidate bands.
In the broader Recognition stack this is bookkeeping for tolerance windows on dimensionless ratios and bridge observables, not a forcing-chain step. It does not itself encode J-cost uniqueness, the eight-tick octave, or the $\alpha$ band; it only supplies the scaled band list those numerical checks consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.