meetsBands_any_of_eval
plain-language theorem explainer
Given a concrete RS units pack that passes the c-band checker on a band specification, the ledger-bridge pair is certified as meeting those bands. RecogSpec acceptance proofs cite this to turn a concrete evaluation into the existential MeetsBands witness. The argument is a one-line existential introduction of that units pack.
Claim. For any ledger $L$, bridge $B$ on $L$, band specification $X$, and RS units pack $U$, if the $c$-band evaluation of $U$ against $X$ succeeds, then $(L,B)$ meets the bands $X$ (i.e., there exists some units pack for which the $c$-band check holds).
background
RecogSpec packages the Recognition Science claim that a ledger and its bridge land inside prescribed numerical bands once units are fixed. The predicate MeetsBands is the acceptance witness: it asserts existence of a concrete Constants.RSUnits pack for which the c-band checker evalToBands_c succeeds against the given Bands object.
The checker itself compares derived display quantities (notably the speed of light in the chosen units) to interval constraints stored in X. Anchors and calibration uniqueness live nearby in the same module: equivalent anchors are those that induce the same calibration speed via speedFromAnchors, so band acceptance is ultimately about physical content up to overall scale.
This lemma is the introduction rule that turns a fully evaluated units pack into that existential witness. The ledger and bridge parameters are carried for interface uniformity with the rest of the Spec API; the mathematical content of the witness is the units pack alone.
proof idea
One-line term proof. The goal is MeetsBands L B X, defined as ∃ units, evalToBands_c units X. The hypotheses already supply a concrete pack U and a proof h : evalToBands_c U X, so the proof is the pair ⟨U, h⟩ (existential introduction). No further lemmas are applied.
why it matters
Band acceptance is the RecogSpec gate between abstract ledger structure and the numerical RS constants (c-display, and downstream the alpha band and mass-ladder checks). Without a clean introduction lemma, every certificate would re-unfold the existential by hand.
The declaration sits with the calibration and uniqueness cluster (Calibrated, UniqueCalibration, AnchorsEqv, unitsFromAnchors_*). Together they implement the paper-level claim that once anchors fix units up to scale, band membership is a definite yes/no on the derived constants. No downstream edges are recorded in the graph snapshot, so its immediate consumers are local Spec certificates rather than a named parent theorem.
Framework-wise this is infrastructure for the constant-band side of RS (alpha inverse in the narrow window near 137, c fixed to 1 in RS-native units), not a forcing-chain step (T5–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.