lambda_kin_from_tau_rec
plain-language theorem explainer
The lemma establishes that the product of light speed and displayed recurrence time equals the displayed kinematic wavelength in RS units. Researchers deriving constants in the Recognition Science framework cite it to confirm the kinematic loop between time and length scales. The proof unfolds the display definitions, invokes the light-cone identity, and finishes with a short ring-plus-rewrite calculation.
Claim. $U.c · τ_rec^display(U) = λ_kin^display(U)$, where $τ_rec^display(U) = (2π τ_0)/(8 ln φ)$ and $λ_kin^display(U) = (2π ℓ_0)/(8 ln φ)$, using the relation $c τ_0 = ℓ_0$.
background
The module supplies clock-side display definitions. The recurrence time is $τ_rec(U) = (2π τ_0)/(8 ln φ)$, with τ_0 the fundamental tick duration. The kinematic wavelength uses the identical form but replaces τ_0 by the fundamental length ℓ_0. RSUnits is the structure that packages (τ_0, ℓ_0, c) together with the light-cone identity c · τ_0 = ℓ_0. The upstream lemma c_ell0_tau0 states exactly this identity in RS-native units.
proof idea
Unfold both display definitions with simp. Introduce the light-cone identity as a local hypothesis from the RSUnits field. Factor the left-hand side with ring, then rewrite the product c τ_0 to ℓ_0 to reach the right-hand side.
why it matters
The identity is invoked by the downstream lemma display_speed_eq_c_of_nonzero to conclude that the displayed speed recovers the structural speed c. It therefore anchors the eight-tick display cycle to the light-cone structure inside the Recognition Science framework. The parent result appears in the KDisplay module that computes the gate ratios.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.