absolute_layer_invariant
plain-language theorem explainer
Absolute-layer acceptance (unique anchor calibration plus band compliance) is unchanged under admissible RS-units rescalings. Spec and verification authors cite it to record that the absolute layer is gauge-stable. The proof is a pure identity: the witness conjunction does not depend on the ambient units pair, so the rescaling hypothesis is only touched and discarded.
Claim. Fix a ledger $L$, bridge $B$, anchors $A$, and bands $X$. Let $U,U'$ be RS unit packs related by an admissible rescaling. If the absolute-layer witness holds—there is a unique units pack calibrated to $A$, and some units pack meets the band checks for $X$—then that same conjunction continues to hold after the rescaling.
background
In RecogSpec, the absolute layer is the pair of acceptance predicates that do not float with a display choice of units. UniqueCalibration L B A asserts there exists a unique RSUnits pack calibrated to the anchors $A$ (forcing the calibration ratio). MeetsBands L B X asserts there exists some units pack for which the concrete band checker evalToBands_c succeeds on $X$.
An RSUnits pack carries the minimal triple $(\tau_0,\ell_0,c)$ with the structural relation $c\cdot\tau_0=\ell_0$. Admissible rescalings (UnitsRescaled U U') relate two such packs; the native gauge sets $\tau_0$ to one tick, $\ell_0$ to one voxel, and $c=1$. The ledger/bridge pair supplies the underlying recognition structure against which anchors and bands are evaluated.
The local setting is the RecogSpec specification surface: absolute-layer witnesses are meant to be physical, hence invariant under the units quotient, while relative display quantities may still transform.
proof idea
Term/tactic hybrid that is morally a one-line identity. The goal is exactly the second hypothesis hU : UniqueCalibration L B A ∧ MeetsBands L B X. The rescaling hypothesis is mentioned only to force a touch of its c field (have _ := hUU'.c false), then discarded; exact hU closes. No transport lemma is needed because both absolute-layer predicates quantify existentially over units packs and do not mention the ambient $U,U'$ in their statements.
why it matters
Records the gauge invariance that makes absolute-layer acceptance a physical (units-quotient) statement inside RecogSpec, rather than a display artifact. It sits next to the calibration and band witnesses (UniqueCalibration, MeetsBands, Calibrated, unitsFromAnchors) that define when a ledger/bridge meets anchors and observational bands.
No downstream theorem currently depends on it (used_by is empty); it functions as a documented invariance law for the spec surface. In the broader RS picture it supports the claim that acceptance at the absolute layer is stable under the same units freedom that relates SI display constants to the RS-native gauge ($c=1$, and the $\phi$-scaled $\hbar,G$ package), without reopening T5–T8 forcing or the mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.