anchor_invariance
plain-language theorem explainer
Bridge evaluation of any dimensionless observable is unchanged under positive rescaling of the time and length anchors that keeps c fixed. Anyone working the certified RS bridge surface or K-gate equalities cites this. The proof is a one-line application of the observable's built-in dimensionless witness.
Claim. For any dimensionless observable $O$ (a map $f$ from RS unit systems to $\mathbb{R}$ with a dimensionless certificate) and any pair of unit systems $U,U'$ related by a common factor $s>0$ on the time and length anchors with $c$ held fixed, the bridge evaluation of $O$ at $U$ equals its evaluation at $U'$.
background
The module supplies the minimal bridge-invariance layer for the certified RS surface: anchor rescaling, dimensionless observables, bridge evaluation, and the K-gate equalities, without the larger verification scaffolds.
UnitsRescaled U U' means there is $s>0$ with $\tau'_0 = s,\tau_0$, $\ell'_0 = s,\ell_0$, and $c'=c$. An Observable is a map $f:\mathrm{RSUnits}\to\mathbb{R}$ packaged with a Dimensionless certificate that $f$ is invariant under such rescalings. BridgeEval O U is simply $O.f,U$: evaluate the display under the chosen anchors.
Upstream constants such as the dimensionless bridge ratio $K=\varphi^{1/2}$ and the RS-native gauge $(\tau_0,\ell_0,c)=(1,1,1)$ sit behind the K-gate observables that this invariance is meant to protect; the theorem itself only needs the structure of Observable and UnitsRescaled.
proof idea
One-line term proof. The goal BridgeEval O U = BridgeEval O U' unfolds to O.f U = O.f U'. That equality is exactly the content of the field O.dimless : Dimensionless O.f, applied to the hypothesis hUU' : UnitsRescaled U U'. No further rewriting or lemmas are required.
why it matters
This is the Q half of the certified bridge (A ∘ Q): evaluation does not depend on rescaled anchors. The module doc places it with UnitsRescaled, Observable, BridgeEval, and the canonical K-gate bridge equality as the small import-closure used by the RS spec and band-invariance surface.
Without anchor-invariance, dimensionless displays (including the bridge ratio $K=\varphi^{1/2}$ and the K-gate observables) could drift under unit choice and the certified equalities would not be unit-stable. The declaration closes that gap by construction: every Observable carries its own dimensionless certificate, so invariance is free at every use site.
No downstream edges are recorded yet in the graph; the intended consumers are the sibling K-gate bridge lemmas and any certified-surface check that evaluates dimensionless displays under varying anchors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.