meetsBands_any_of_checker
plain-language theorem explainer
If some units pack passes the bands checker predicate against a fixed band set, the ledger-bridge pair meets those bands. Spec and calibration authors cite this to promote a checker witness into the existential MeetsBands acceptance form. The proof unpacks the existential and hands it to the evaluation lemma.
Claim. Let $L$ be a ledger, $B$ a bridge on $L$, and $X$ a band specification. If there exists a units pack $U$ such that the bands checker predicate holds for $U$ and $X$, then $\mathrm{MeetsBands}(L,B,X)$ holds: there exists an RS units pack whose $c$-evaluation lands inside $X$.
background
In RecogSpec, physical acceptance of a calibration is phrased as band membership for display constants (notably $c$) relative to a fixed Bands package $X$. The predicate MeetsBands is the existential witness form: there is some RSUnits pack whose evaluation against $X$ succeeds (evalToBands_c).
A separate checker predicate (meetsBandsCheckerP) is the concrete boolean-style gate on a units pack and band set. The RS-native units pack sets $\tau_0$ to one tick, $\ell_0$ to one voxel, and $c=1$; bridges and ledgers supply the native-to-display comparison structure against which bands are judged.
This lemma lives in the Spec layer that ties anchors, units transport, and band acceptance together, alongside calibration uniqueness and anchor equivalence up to speed.
proof idea
Term-style unpacking. Destructure the hypothesis $\exists U,,\mathrm{meetsBandsCheckerP},U,X$ to a concrete units pack $U$ and a checker proof $hU$. Apply the upstream evaluation bridge lemma meetsBands_any_of_eval at $(L,B,X,U)$ with $hU$, which converts a successful checker run into the existential MeetsBands witness. No further algebra.
why it matters
Band acceptance is the gate between abstract RS units and empirically stated windows (including the fine-structure band near $\alpha^{-1}\in(137.030,137.039)$ and $c$-centred default bands). Promoting checker success to MeetsBands keeps the Spec API uniform: downstream calibration and uniqueness results can assume the existential form without threading checker internals.
No recorded downstream users yet in the graph; the lemma still closes the checker-to-witness gap next to MeetsBands, Calibrated, and UniqueCalibration. It is bookkeeping rather than a forcing-chain step (T5–T8), but it is required glue for any claim that a ledger-bridge pair sits inside published RS bands.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.