meetsBandsCheckerP_invariant
plain-language theorem explainer
Under a units rescaling between two RS unit systems, the bands-checker predicate is unchanged: one system meets a fixed band list exactly when the other does. Calibration and verification code that switches gauges cites this. The proof is a one-line wrapper of the c-invariance lemma for band evaluation.
Claim. Let $U,U'$ be RS unit systems (each carrying $\tau_0,\ell_0,c$ with $c\,\tau_0=\ell_0$) related by a units rescaling, and let $X$ be a list of real intervals (bands). Then $U$ satisfies the bands-checker predicate on $X$ if and only if $U'$ does.
background
RSUnits is the minimal Recognition Science unit bundle: a tick $\tau_0$, a length $\ell_0$, a speed $c$, and the structural law $c,\tau_0=\ell_0$. The native gauge sets $\tau_0=1$, $\ell_0=1$, $c=1$. A units rescaling (Verification.UnitsRescaled) relates two such bundles when they differ only by a consistent change of display scale.
Bands is an abbreviation for a list of closed real intervals; each band has a contains predicate and a validity condition $\mathrm{lo}\le\mathrm{hi}$. The bands-checker predicate asks whether the constants extracted from a given RSUnits land inside a prescribed band list $X$.
This lemma lives in RecogSpec.Spec, the specification layer that ties anchors, calibrated units, and band targets together for verification. The upstream engine is the c-invariance of band evaluation: once $c$ (and the induced length/time scales) transform under rescaling, membership of the evaluated constants in $X$ is unchanged.
proof idea
One-line wrapper. The goal is the biconditional meetsBandsCheckerP U X ↔ meetsBandsCheckerP U' X under the rescaling hypothesis h. It is discharged by applying evalToBands_c_invariant at the same U, U', h, and X; that lemma already proves the underlying evaluation-to-bands relation is invariant under units rescaling, which is exactly the content of the checker predicate.
why it matters
RecogSpec is the bridge between abstract RS constants and concrete numerical band targets used in verification. Invariance of the checker under UnitsRescaled means band compliance is a gauge-invariant statement: it does not depend on which display units one chose for $\tau_0$, $\ell_0$, and $c$.
Sibling material in the same module (Calibrated, UniqueCalibration, MeetsBands, AnchorsEqv, unitsFromAnchors) builds the calibration story; this lemma guarantees that once anchors fix a unit system up to rescaling, band membership is well-defined on the equivalence class. No downstream consumers are recorded yet, so the lemma is presently a local hygiene fact inside Spec rather than a cited step in a larger theorem.
Framework-wise it supports the RS-native units picture ($c=1$ in the native gauge, with display $c$ recovered from anchors) without forcing a preferred scale when checking band targets such as the $\alpha^{-1}$ window.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.