ell0_div_tau0_eq_c
plain-language theorem explainer
The lemma establishes that the ratio of fundamental length to fundamental time equals the speed of light inside the RSUnits structure whenever the time unit is nonzero. Researchers working on Recognition Science constants and display equalities cite this identity to confirm structural speed consistency. The proof is a short calc chain that substitutes the defining relation c tau0 = ell0, rewrites the quotient, cancels the nonzero factor, and simplifies to c.
Claim. In the RSUnits structure, if the fundamental time unit satisfies $U.tau0 ≠ 0$, then $U.ell0 / U.tau0 = U.c$.
background
The RSUnits structure packages the three core constants together with their defining relation: it contains fields tau0 (fundamental tick duration), ell0 (fundamental length, set to 1 in native units), c (speed of light), and the axiom c * tau0 = ell0. This relation is the light-cone identity imported from Constants.c_ell0_tau0. The module focuses on dimensionless bridge ratios K and display equalities that recover c from the ratio ell0/tau0. Upstream, tau0 is defined as the tick duration and ell0 as the voxel length in RS-native units.
proof idea
The proof is a calc tactic that begins with the substitution U.ell0 / U.tau0 = (U.c * U.tau0) / U.tau0 using the structure field c_ell0_tau0. It then applies mul_div_assoc to obtain U.c * (U.tau0 / U.tau0), invokes div_self on the nonzero hypothesis to reach U.c * 1, and finishes with mul_one.
why it matters
This lemma supplies the structural speed identity that underpins display equalities in the KDisplay module. It directly instantiates the light-cone relation c_ell0_tau0 inside the RSUnits packaging and supports later claims that display speed recovers c. In the Recognition framework it confirms that the ratio ell0/tau0 equals c in native units, consistent with the eight-tick octave and the setting c = 1 after rescaling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.