display_speed_eq_c
plain-language theorem explainer
The lemma establishes that in RS units with positive base tick duration the ratio of kinematic display wavelength to recursive display period equals the speed of light. Researchers verifying display-level Lorentz structure in Recognition Science cite it when confirming lightlike propagation from the K bridge. The term proof first confirms the display period is nonzero via a prior lemma then reduces directly to the nonzero case.
Claim. In an RS unit system $U$ with $0 < U.tau_0$, the ratio of the kinematic display length to the recursive display time equals the speed of light $c(U)$.
background
The module treats dimensionless bridge ratios and display equalities. RSUnits is the minimal structure holding tau0, ell0 and c subject to the relation c * tau0 = ell0. K is defined as phi to the power 1/2. The kinematic display length and recursive display time are auxiliary quantities that carry the K ratio into observable speeds. Upstream results include the RSUnits structure from Constants and the independent spatial semantics from the ClassicalBridge module.
proof idea
The proof is a term-mode reduction. It first obtains the fact that the recursive display time is nonzero by applying tau_rec_display_ne_zero, then invokes the specialized lemma for the nonzero case to obtain the equality.
why it matters
This lemma supports the display null condition theorem that asserts the Lorentz null structure at the display level and the positivity theorem for display speed. It completes a step in the constants derivation for the K bridge ratio, reinforcing that c emerges as the invariant speed from the phi-ladder and eight-tick octave. Downstream results quote it directly to obtain ((lambda/tau)^2 = c^2).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.