meetsBandsChecker_gen_nil
plain-language theorem explainer
The empty list of real samples never meets any band collection: the generalized band-membership checker returns false for every band list. Simplifiers and RecogSpec band-validation proofs cite this as the empty-sample base case. Proof is a one-line unfold of the List.any definition under classical.
Claim. For every list of closed real intervals $B$, the generalized band checker on the empty sample list returns false: $\mathrm{meets}(\emptyset, B) = \mathsf{false}$.
background
In RecogSpec.Bands, a band is a closed real interval (lo, hi), with containment $b.lo \le x \le b.hi$ and validity $b.lo \le b.hi$. Bands is just a list of such intervals. The generalized checker asks whether any sample real lies in any band: it is xs.any of bs.any of a decidable containment test.
The module packages observational band constraints for Recognition Science verification bridges (BridgeCore). A sibling ILG Action structure also named Bands holds consolidated PPN, lensing, and GW widths; the checker here uses the list-of-intervals form, not that structure.
proof idea
One-line simp wrapper. Unfold the definition of the generalized checker; List.any on [] is false, so the Bool equality holds. The classical block supplies the decidability instance used by decide inside the definition.
why it matters
Empty-list base case for the simp set around RecogSpec band checking. Downstream goals that reduce to an empty sample list discharge automatically. No used_by edges are recorded yet; this is local infrastructure, not a forcing-chain step. It does not touch T0–T8, the Recognition Composition Law, phi, the eight-tick octave, or the mass ladder. It only stabilizes Boolean band-membership reductions used when wiring observables into verification bridges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.