lambda_kin_display
plain-language theorem explainer
The kinematic display length λ_kin is defined as (2π ℓ₀)/(8 ln φ) inside an RSUnits structure. Researchers verifying display-level speed equalities or K-gate ratios in Recognition Science reference this for length scaling. It is introduced by direct substitution of the fundamental length ell0 and the logarithm of phi.
Claim. $λ_{kin}(U) = (2π ℓ_0(U)) / (8 ln φ)$ where $U$ is an RS unit structure containing fundamental length $ℓ_0$.
background
RSUnits is the structure holding fundamental time τ₀, length ℓ₀ and speed c satisfying c τ₀ = ℓ₀. ell0 supplies the base length (equal to 1 in native gauge). The factor 8 arises from the eight-tick octave. The module supplies the length counterpart to the clock-side display definition τ_rec(display) = (2π τ₀)/(8 ln φ). Upstream, K is defined as φ^{1/2} and ell0 as the voxel unit.
proof idea
Direct definition that substitutes ell0 and the constant log phi into the displayed expression. No lemmas or tactics are invoked beyond the imported constants ell0 and phi.
why it matters
Supplies the length input to the display speed lemmas (display_speed_eq_c, display_speed_eq_c_of_nonzero) and the ratio certificate computeRatios. It realizes the eight-tick factor from forcing-chain step T7 and feeds the scale-invariance and null-condition theorems in KDisplay. The definition closes the kinematic half of the display bridge used for unit-gate verification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.