meetsBandsChecker_gen_nilBands
plain-language theorem explainer
For any list of candidate reals, the generalized band-membership checker returns false when the band list is empty. Spec and verification authors cite it to discharge empty-band side conditions under simp. The proof is a one-line classical simp that unfolds the definition: empty `any` is false.
Claim. For every finite list $xs$ of real numbers, the generalized band checker on $xs$ with the empty band list equals $\mathsf{false}$.
background
In RecogSpec, a band is a closed real interval used to state tolerance windows on predicted constants and observables. A band list ("Bands") is a finite collection of such windows. The generalized checker meetsBandsChecker_gen asks whether any candidate value in a list $xs$ lies in any band of a given list $bs$: it is the Boolean any over $x \in xs$ of any over $b \in bs$ of the decidable predicate "$b$ contains $x$".
When $bs$ is empty there is no window that can contain a candidate, so the inner any is identically false and the whole checker must return false. This module sits under Recognition verification bridges that compare computed RS quantities against declared numeric bands.
proof idea
Classical mode, then simp with the definition of the generalized checker. Unfolding replaces the goal by xs.any (fun x => [].any (...)) = false. The empty-list any reduces to false for every $x$, so the outer any is false.
why it matters
Empty-band base case for the RecogSpec band machinery. It keeps simp normal forms honest when band lists are constructed dynamically or discharged by cases, so later band-satisfaction lemmas do not stall on the nil constructor. No downstream theorems currently depend on it in the graph; it is infrastructure for band checks that gate RS numeric claims (alpha band, mass windows, and related RecogSpec tolerances) rather than a physics identity itself. It does not touch the forcing chain T0–T8 or the RCL; it only stabilizes the Boolean layer that reports whether a computed real meets a declared window.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.