UnitsRescaled
plain-language theorem explainer
Anchor rescaling relates two RS unit systems by a common positive scale factor on the fundamental tick and length, while holding the speed of light fixed. Anyone proving band or absolute-layer invariance under change of units cites this relation. The structure packages the five fields; reflexivity, symmetry, and transitivity are proved by elementary real arithmetic (inverse and product of positive scales).
Claim. Two RS unit systems $U$ and $U'$ are related by an anchor rescaling when there exists $s>0$ such that $\tau_0(U')=s\,\tau_0(U)$, $\ell_0(U')=s\,\ell_0(U)$, and $c(U')=c(U)$. The relation is reflexive ($s=1$), symmetric ($s\mapsto s^{-1}$), and transitive (multiply the scale factors).
background
The Verification Bridge Core module supplies the minimal invariance infrastructure for the certified RS surface (spec and band checks), deliberately kept small so the import closure stays non-smuggled.
An RS unit system carries the fundamental tick duration $\tau_0$, the fundamental length $\ell_0$ (voxel scale, equal to 1 in RS-native units), and the speed $c$. Anchor rescaling means stretching time and length anchors by the same positive factor while leaving $c$ unchanged; that is the admissible change of display units for dimensionless observables.
Upstream constants supply $\tau_0$ (fundamental tick) and $\ell_0$ (fundamental length). Downstream, dimensionless displays and bridge evaluations are defined to be invariant exactly under this relation.
proof idea
The declaration is a structure plus three constructors, not a deep theorem.
Reflexivity: take $s=1$; positivity is norm_num, and the three equalities are simp/rfl with one_mul.
Symmetry: invert the scale. Positivity of $s^{-1}$ is inv_pos. The $c$ field is symmetry of equality. For $\tau_0$ and $\ell_0$, cancel $s^{-1}\cdot(s\cdot\cdot)$ via associativity and $s\neq 0$ (from $s>0$), then rewrite with the original equalities.
Transitivity: multiply the two scales; positivity is mul_pos. Chain the $\tau_0$ and $\ell_0$ equalities and reassociate with ring; $c$ composes by two applications of cfix.
why it matters
This is the admissible-units relation for the certified surface. Band and absolute-layer acceptance must not depend on the arbitrary choice of tick and length anchors.
Downstream: evalToBands_c_invariant uses cfix to show the $c$-band check is unchanged; meetsBandsCheckerP_invariant and meetsBands_any_of_eval_rescaled lift that to meets-bands witnesses; absolute_layer_invariant and absolute_layer_from_eval_invariant package absolute-layer acceptance as invariant under rescaling. BandsInvariantCert quantifies over all such rescalings. Sibling Dimensionless and anchor_invariance define observables that are constant on this relation.
In RS terms, $c$ is fixed in native units ($c=1$ in the primer), so only the common $(\tau_0,\ell_0)$ scale is free; dimensionless predictions (including the $\alpha$ band) are therefore unit-choice independent once this relation is the equivalence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.