lambda_kin_display_ratio
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not derive the explicit form of lambda_kin_display from the forcing chain.
- Does not compute a numerical value for phi or K_gate_ratio.
- Does not address the clock-side ratio tau_rec_display.
- Does not extend to non-native unit choices beyond the RSUnits structure.
formal statement (Lean)
28@[simp] lemma lambda_kin_display_ratio (U : RSUnits) (hℓ : U.ell0 ≠ 0) :
29 (lambda_kin_display U) / U.ell0 = K_gate_ratio := by
proof body
Term-mode proof.
30 unfold lambda_kin_display K_gate_ratio
31 field_simp [hℓ]
32 ring
33
34/-- Kinematic consistency: c · τ_rec(display) = λ_kin(display). -/