evalToBands_c_invariant
plain-language theorem explainer
The speed-of-light band check is invariant under RS unit rescaling: if two unit systems are related by UnitsRescaled, then c lies in a given band list for one iff it does for the other. Spec and certification layers cite this to move MeetsBands and absolute-layer witnesses across gauges. The proof is a short bidirectional argument using the c-fix equality from the rescaling hypothesis.
Claim. Let $U,U'$ be RS unit systems related by a units rescaling (so in particular $U'.c=U.c$), and let $X$ be a finite list of real intervals (bands). Then $U.c$ lies in some band of $X$ if and only if $U'.c$ lies in some band of $X$.
background
In RecogSpec, a Band is a closed real interval $[\mathrm{lo},\mathrm{hi}]$, and Bands is a list of such intervals. Containment is the usual predicate $\mathrm{lo}\le x\le\mathrm{hi}$. The checker evalToBands_c asks whether the speed-of-light coordinate of an RS unit system falls inside at least one band of a supplied list.
RS units (RSUnits) package the elementary scales $\tau_0$, $\ell_0$, and $c$ with the structural relation $c\cdot\tau_0=\ell_0$. A units rescaling between two such systems is required to fix $c$ (the cfix field): only the auxiliary scales may change. In the RS-native gauge one has $c=1$, but the band machinery is written for a general unit system so that verification certificates remain gauge-stable.
The local module builds sample and wide bands around constants; this lemma isolates the pure $c$-invariance fact used by the Spec layer when assembling MeetsBands witnesses.
proof idea
Unfold the definition of the $c$-band checker. From the rescaling hypothesis extract $U'.c=U.c$. Both directions of the biconditional unpack an existential witness band $b\in X$ with $b$ containing the relevant $c$, then reassemble the same band with containment rewritten by simpa along $U'.c=U.c$ (or its symmetric). No arithmetic beyond equality substitution is required.
why it matters
Gauge invariance of band checks is a prerequisite for absolute-layer and certification statements that must not depend on an arbitrary choice of RS units. Downstream, meetsBands_any_of_eval_rescaled applies the forward direction to obtain a MeetsBands witness after rescaling; meetsBandsCheckerP_invariant is literally this lemma under a renamed checker; and absolute_layer_from_eval_invariant builds the absolute-layer package (unique calibration plus meets-bands) from a concrete $c$-eval in one gauge. The verification certificate BandsInvariantCert quantifies over all rescalings and band lists, so this fact is the atomic step that certificate discharges for the $c$ coordinate.
In the broader RS picture, $c$ is fixed to $1$ in native units and enters the forcing chain only as a structural scale; the lemma ensures that numerical band windows placed on $c$ survive the passage between native and laboratory gauges without reopening T5–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.