UnitsEquivalent
plain-language theorem explainer
Two RSUnits packs are equivalent when they share the same c and their tau0 and ell0 differ by a common nonzero real scaling factor alpha. Researchers establishing invariance of dimensionless displays and observables under unit rescaling cite this relation to quotient out fundamental scale choices. The definition is direct from the RSUnits structure and is immediately shown to be an equivalence relation by explicit reflexivity, symmetry via inversion, and transitivity via composition of scalings.
Claim. Two unit systems $U_1$ and $U_2$, each consisting of a speed $c$, fundamental time interval $τ_0$, and fundamental length $ℓ_0$, are equivalent if $c_1 = c_2$ and there exists nonzero real $α$ such that $τ_0^{(2)} = α τ_0^{(1)}$ and $ℓ_0^{(2)} = α ℓ_0^{(1)}$.
background
The module addresses the dimensionless bridge ratio K and display equalities. RSUnits packages the constants c, tau0 (fundamental tick duration, defined as the placeholder tick), ell0 (fundamental length unit set to the RS-native voxel value 1), and the compatibility field c_ell0_tau0. UnitsEquivalent encodes that two such packs represent physically equivalent units up to a shared nonzero rescaling of the time and length scales while preserving c.
proof idea
The declaration is a direct definition of the predicate on RSUnits. The accompanying theorems establish it as an equivalence relation: reflexivity takes alpha = 1; symmetry inverts the witnessing alpha and applies field_simp; transitivity composes the two alphas and uses ring to reassociate the products.
why it matters
This definition is invoked by displays_invariant_under_equivalence and observable_factors_through_quotient to show that tau_rec_display ratios and general observables factor through the units quotient. It supports construction of the dimensionless K by ensuring scale-invariant ratios, consistent with Recognition Science emphasis on relations independent of unit choice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.