lambda_kin_display_ratio
plain-language theorem explainer
The lemma establishes that the kinematic display length normalized by the base length equals the constant K_gate_ratio = π/(4 ln φ). Researchers verifying display scalings in RS-native units cite it when confirming length-side consistency with clock-side ratios. The proof is a direct algebraic reduction that unfolds the two explicit definitions and normalizes via field simplification and ring.
Claim. Let $U$ be an RS unit structure with $U.ell_0 ≠ 0$. Then $λ_{kin}(display,U)/U.ell_0 = π/(4 ln φ)$, where $λ_{kin}(display,U) = (2π U.ell_0)/(8 ln φ)$.
background
RSUnits is the minimal structure carrying base time τ₀, length ℓ₀ and speed c satisfying c τ₀ = ℓ₀. In the native gauge both τ₀ and ℓ₀ are set to 1. The kinematic display length is defined by lambda_kin_display U := (2 π U.ell_0)/(8 log φ). K_gate_ratio is the constant π/(4 log φ). Upstream, ell0 is introduced as c τ₀ in the Derivation module and specialized to the constant 1 in the core Constants module.
proof idea
The proof is a one-line wrapper that unfolds lambda_kin_display and K_gate_ratio, applies field_simp using the hypothesis U.ell_0 ≠ 0, and finishes with the ring tactic.
why it matters
The lemma supplies the length-side half of the identity proved in the downstream theorem K_gate_eqK, which asserts that both display ratios equal K_gate_ratio. It thereby closes the canonical K-gate statement inside the constants module and supports the eight-tick octave scaling (T7) together with the phi-ladder relations used throughout the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.