display_speed_eq_c_of_nonzero
plain-language theorem explainer
The lemma shows that the ratio of kinematic display length to recurrence display time equals the structural speed c whenever the recurrence time is nonzero. Researchers consolidating K-gate display equalities in Recognition Science constants cite it to confirm that phi-scaled display quantities recover c. The proof is a short calc chain that substitutes the kinematic consistency relation then cancels the nonzero term via division and multiplication identities.
Claim. Let $U$ be an RS-units structure. If the display recurrence time satisfies $τ_{rec}(U) ≠ 0$, then $λ_{kin}(U) / τ_{rec}(U) = c_U$.
background
RSUnits is the minimal structure carrying base scales τ₀, ℓ₀ and structural speed c together with the relation c · τ₀ = ℓ₀. The display quantities are defined as τ_rec_display U := (2π τ₀) / (8 ln φ) and λ_kin_display U := (2π ℓ₀) / (8 ln φ). The upstream lemma lambda_kin_from_tau_rec states that c · τ_rec_display U = λ_kin_display U, which supplies the kinematic consistency relation used here. The module addresses dimensionless bridge ratios K and display equalities.
proof idea
The proof invokes lambda_kin_from_tau_rec to replace λ_kin_display U with c · τ_rec_display U. It then rewrites the ratio as c · (τ_rec / τ_rec) using mul_div_assoc, cancels to c · 1 via div_self on the nonzero hypothesis, and finishes with mul_one.
why it matters
This lemma supplies the core equality for the K-gate display speed and is invoked by the strengthened version display_speed_eq_c that removes the nonzero hypothesis via positivity. It fills the step connecting the phi-based display scales to the invariant speed c in the Recognition framework, where c = 1 in native units and the eight-tick octave governs the denominators.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.