meetsBands_any_of_eval_rescaled
plain-language theorem explainer
If the centered band checker succeeds for one RS units pack, and a second pack is only a rescaling of the first, the meets-bands witness still holds. Calibration and RecogSpec certificate authors cite this when changing gauge on units. The proof transports the checker by rescaling invariance, then packages the transported pack as an existential MeetsBands witness.
Claim. Let $L$ be a ledger, $B$ a bridge on $L$, and $X$ a band specification. If $U,U'$ are RS unit packs related by a units rescaling and the centered band evaluation of $X$ succeeds at $U$, then the meets-bands property holds for $(L,B,X)$: there exists some RS unit pack for which the centered band check against $X$ succeeds.
background
RecogSpec packages the Recognition Science calibration story: a ledger $L$ of double-entry recognition events, a bridge $B$ linking that ledger to display quantities, and a band specification $X$ of allowed numerical windows. The minimal units pack is RSUnits with tick $\tau_0$, length $\ell_0$, and speed $c$ obeying $c,\tau_0=\ell_0$.
MeetsBands L B X is the acceptance witness: there exists some RSUnits pack for which the centered band checker evalToBands_c succeeds on $X$. It is deliberately existential, so the concrete gauge of the units may vary.
Units rescaling (UnitsRescaled U U') is the relation that two packs differ only by an overall scale change of the display units. Upstream, the centered checker is invariant under that relation: if it holds at $U$ it holds at $U'$. Native RS gauge sets $\tau_0=1$ tick, $\ell_0=1$ voxel, $c=1$.
proof idea
Short two-step tactic proof. First apply the forward direction of evalToBands_c_invariant at $(U,U')$ with the rescaling hypothesis to transport evalToBands_c U X into evalToBands_c U' X. Then feed that transported checker into the sibling meetsBands_any_of_eval at pack $U'$, which turns a concrete successful evaluation into the existential MeetsBands witness. No band arithmetic is redone here; the work is pure transport plus packaging.
why it matters
In the RecogSpec stack this lemma closes the gauge gap between a checker proved in one units pack and the existential meets-bands certificate that downstream calibration wants. Sibling infrastructure includes Calibrated, UniqueCalibration, AnchorsEqv, and the anchor-derived speed/units constructors: together they implement "unique up to units" for physical calibration.
The lemma is local plumbing rather than a forcing-chain landmark (T5–T8, RCL, $\phi$, eight-tick octave). It does not itself pin $\alpha$ or masses; it only ensures band acceptance survives the units quotient that those later comparisons rely on. Currently nothing in the graph lists this lemma as a dependency, so it is a ready witness constructor waiting on certificate assembly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.