units_identity_holds
plain-language theorem explainer
The lemma confirms that the units identity c τ₀ = ℓ₀ holds for every RS-native unit anchor. Researchers normalizing lengths and times inside the Recognition Science constants would cite it to verify dimensional consistency across anchors. The proof reduces the universal claim to the per-anchor light-cone identity by direct simplification.
Claim. For every RS-native unit anchor $U$, the speed of light times the fundamental time interval equals the fundamental length interval: $c_U · τ_{0,U} = ℓ_{0,U}$.
background
The RS-native gauge fixes τ₀ to one tick, ℓ₀ to one voxel, and c to one, as stated in the upstream definition of U. The units identity proposition is the statement that this gauge satisfies the light-cone relation for any such anchor. The upstream lemma c_ell0_tau0 supplies the explicit light-cone identity ℓ₀ = c · τ₀ in RS-native units, with the module doc describing the overall setting as the units identity as a Prop: c·τ0 = ℓ0 for all anchors.
proof idea
The proof introduces an arbitrary RS-native unit structure U and applies the simplification tactic directly to the light-cone identity lemma c_ell0_tau0 contained inside U.
why it matters
This lemma discharges the units identity proposition, confirming consistency of the RS-native gauge inside the constants module. It supplies the required relation that supports the eight-tick octave and the forcing chain steps leading to D = 3. No downstream uses appear yet, so its role in later adapter proofs remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.