meetsBandsChecker_nil
plain-language theorem explainer
The empty list of candidate anchors never satisfies the band-membership checker, for any real center value. Spec and verification authors cite this as a base simp fact when discharging empty-list cases in RecogSpec band checks. The proof is a one-line classical simp that unfolds the checker into list-any over bands.
Claim. For every real number $c$, the band-membership checker on the empty list of anchors at center $c$ evaluates to false.
background
In RecogSpec.Bands, a band is an interval used to test whether numerical anchors land inside predicted windows. The generalized checker takes a list of reals and a collection of bands, and returns true if any list element lies in any band (via classical decide on containment).
The specialized checker fixes the band collection to the evaluation of bands at a real center with unit scale, then asks whether any supplied anchor meets those bands. Empty-list behavior is forced by the semantics of List.any: there is no element that can witness membership.
This module sits under Recognition specification verification (imports BridgeCore), where band windows encode RS-native numerical targets against which computed constants or ladder values are checked.
proof idea
Classical mode, then simp with the two checker definitions. Unfolding the specialized checker yields the generalized form on evalBandsAt c 1; unfolding that yields List.any over the empty list, which simplifies to false.
why it matters
Gives a clean base case for the RecogSpec band-checker API: empty candidate lists never pass. No downstream uses are recorded yet; the lemma is infrastructure for simp-driven discharge of vacuous band checks in verification scripts. It does not itself encode a physics claim (no T0–T8 step, RCL identity, or mass-ladder statement), but keeps the band-validation layer honest when lists are empty or filtered away.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.