meetsBandsChecker_gen
plain-language theorem explainer
Boolean predicate on a list of reals and a list of closed intervals: true exactly when at least one sample lands in at least one band. RecogSpec verification and band-sampling lemmas cite it as the generic membership check before specializing to evaluated bands at a center. The body is a classical double List.any over decidable interval containment.
Claim. Given a finite list of real samples $x_i$ and a finite list of closed bands $[\ell_j,h_j]$, return true if and only if there exist $i,j$ with $\ell_j \le x_i \le h_j$; otherwise false.
background
In RecogSpec, a band is a closed real interval with endpoints lo and hi. Containment is the standard predicate $\ell \le x \le h$, matching the Numerics.Interval containment relation. A collection of bands is just a list of such intervals; validity of a single band means $\ell \le h$, but the checker does not require validity up front.
The module sits in the verification layer that compares computed anchors against candidate observational windows. Upstream, interval containment is the atomic geometric test; here it is lifted to an existential check over two finite lists so that empty samples or empty band catalogs fail cleanly.
A separate ILG Action structure also named Bands packages PPN, lensing, and GW tolerances; the RecogSpec abbrev is the simpler list-of-intervals type used by this checker.
proof idea
Definitional, not a proof. Under classical logic, evaluate List.any on the sample list; for each sample, List.any on the band list with decide applied to the Prop Band.contains b x (i.e. $b.lo \le x \le b.hi$). The result is the Boolean encoding of existential membership.
why it matters
This is the generic engine behind meetsBandsChecker, which specializes the band list to evalBandsAt c 1 and asks whether anchors meet those windows. Downstream simp lemmas (meetsBandsChecker_gen_nil, meetsBandsChecker_gen_nilBands, meetsBandsChecker_nil) pin the empty-list edge cases to false, so verification scripts can discharge trivial failures without unfolding.
In the Recognition stack, band checks gate whether predicted constants or observables sit inside the RS-native windows (for example the alpha inverse band near 137). The definition itself is pure plumbing; its value is that every specialized checker and nil-case lemma funnels through one decidable double-existential.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.