display_speed_eq_c_of_nonzero
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not establish positivity of τ_rec_display U.
- Does not extend to cases where τ_rec_display vanishes.
- Does not derive the value of c from other axioms.
Lean usage
have hτ : tau_rec_display U ≠ 0 := tau_rec_display_ne_zero U h0; exact display_speed_eq_c_of_nonzero U hτformal statement (Lean)
24lemma display_speed_eq_c_of_nonzero (U : RSUnits)
25 (hτ : tau_rec_display U ≠ 0) : (lambda_kin_display U) / (tau_rec_display U) = U.c := by
proof body
Tactic-mode proof.
26 have h := lambda_kin_from_tau_rec U
27 calc
28 (lambda_kin_display U) / (tau_rec_display U)
29 = (U.c * tau_rec_display U) / (tau_rec_display U) := by rw [h]
30 _ = U.c * (tau_rec_display U / tau_rec_display U) := by rw [mul_div_assoc]
31 _ = U.c * 1 := by rw [div_self hτ]
32 _ = U.c := by rw [mul_one]
33
34/-! Strengthen display-speed equality: remove nonzero hypothesis by proving positivity. -/