Dimensionless
plain-language theorem explainer
A real-valued map on RS unit anchors is dimensionless precisely when it is unchanged under simultaneous positive rescalings of the time and length anchors that keep c fixed. Bridge and certified-surface authors cite it to mark displays that may be compared across gauges. The body is a one-line universal quantification over the anchor-rescaling relation.
Claim. A map $f$ from RS unit anchors $(\tau_0,\ell_0,c)$ to $\mathbb{R}$ is dimensionless when, whenever two anchors are related by a common scale $s>0$ on $\tau_0$ and $\ell_0$ with $c$ held fixed, one has $f(U)=f(U')$.
background
The module supplies the minimal bridge-invariance layer for the certified surface: anchor rescaling, dimensionless displays, bridge evaluation, and the K-gate equality, without pulling in the larger verification scaffolds.
RS unit anchors are triples $(\tau_0,\ell_0,c)$ with the consistency $c\cdot\tau_0=\ell_0$. The relation UnitsRescaled says two anchors differ by a common factor $s>0$ on the time and length anchors while $c$ is unchanged; reflection at $s=1$ is immediate. In the RS-native gauge one takes $\tau_0=1$ tick, $\ell_0=1$ voxel, $c=1$.
Dimensionlessness is the invariance of a numeric display under that relation. Downstream, an observable is exactly such a dimensionless display, ready for bridge evaluation and anchor-invariance arguments.
proof idea
Pure definition: the predicate is the universal statement that for all pairs of anchors related by a positive common scale on $\tau_0$ and $\ell_0$ with $c$ fixed, the real values of $f$ agree. No lemmas are applied; the body is the Prop itself.
why it matters
Bridge comparisons are only meaningful for quantities that do not depend on the arbitrary choice of time/length anchors. This predicate is the formal filter used throughout the certified surface: observables are dimensionless displays, and anchor-invariance theorems discharge equality of bridge evaluations under rescaling.
It feeds constants and chemistry layers that need gauge-stable numbers (alpha constructions, dimensional bookkeeping, eight-beat period proxies, periodic-table indexing). In the broader framework it sits under the verification half of the forcing chain: once $c$ is fixed and the eight-tick structure is in place, only dimensionless combinations may be matched to external bands such as $\alpha^{-1}\in(137.030,137.039)$.
Without it, K-gate and band-invariance claims would smuggle unit dependence into the certified import closure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.