observable_factors_through_quotient
plain-language theorem explainer
Any real-valued observable O on RSUnits that remains unchanged when the fundamental time and length units are scaled by a positive factor alpha while c is held fixed is constant on units related by such a rescaling. Researchers verifying the dimensionless bridge ratio K or checking K-gate consistency would cite this result to justify working directly with scale-invariant quantities. The proof extracts the scaling witness from the equivalence hypothesis, applies the invariance condition to the first unit, reconstructs the second unit as its resk
Claim. Let $O : RSUnits → ℝ$. Suppose that for every unit structure $U$ and every $α ≠ 0$, $O$ of the rescaled structure with $τ₀' = α τ₀$, $ℓ₀' = α ℓ₀$, $c' = c$ equals $O(U)$. Then for all unit structures $U_1, U_2$, if $U_1$ and $U_2$ differ only by a common positive scaling factor on $τ₀$ and $ℓ₀$ (with $c$ unchanged), it follows that $O(U_1) = O(U_2)$.
background
RSUnits is the structure carrying the three constants $τ₀$ (fundamental tick), $ℓ₀$ (fundamental length), and $c$ (speed of light) together with the light-cone identity $c · τ₀ = ℓ₀$. The relation UnitsEquivalent identifies two such structures when one is obtained from the other by multiplying both $τ₀$ and $ℓ₀$ by the same positive real $α$ while leaving $c$ fixed. The hypothesis hQuot encodes precisely the invariance of $O$ under this rescaling. Upstream lemmas supply the concrete definitions: c_ell0_tau0 asserts the light-cone identity, ell0 and tau0 fix the RS-native units, and K is defined as $φ^{1/2}$ in the same module.
proof idea
The tactic proof intros U1, U2 and the equivalence witness h. It obtains the triple (hc : c equal, α ≠ 0, and the two scaling equations) from h. It applies the invariance hypothesis hQuot directly to U1 and α. It then reconstructs U2 as the scaled copy of U1 by case analysis on the structure constructor, using simp on the mk.injEq and the supplied scaling equations. Finally it rewrites the reconstructed equality and applies symmetry to finish.
why it matters
The result guarantees that any observable satisfying the scaling invariance descends to the quotient of RSUnits, which is the mathematical prerequisite for treating K as a purely dimensionless bridge ratio. It supports the K-gate verification procedure documented in the same module (measure τ_rec and λ_kin independently, compare the two derived K values). The theorem sits inside the Constants layer that feeds the larger forcing chain (T5–T8) by ensuring that display quantities remain well-defined once units are quotiented by the eight-tick octave scaling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.