lambda_kin_display
plain-language theorem explainer
lambda_kin_display supplies the kinematic length display unit λ_kin(display) = (2π ℓ₀)/(8 ln φ) for any RSUnits pack. Certificate authors and K-gate verifiers cite it when checking scale-invariant ratios or null conditions. The definition is a direct algebraic expression with no lemmas or tactics applied.
Claim. For an RSUnits structure $U$ with fundamental length component $U.ℓ_0$, the kinematic display length is defined by $λ_{kin}(display) := (2π U.ℓ_0)/(8 ln φ)$.
background
RSUnits is the structure holding native units τ₀ (tick), ℓ₀ (voxel) and c with the relation c τ₀ = ℓ₀. ell0 is the constant voxel length 1 in native units. The factor 8 and ln φ trace to the eight-tick octave and self-similar fixed point in the Recognition framework. This length-side definition parallels the clock-side τ_rec(display) = (2π τ₀)/(8 ln φ) stated in the module documentation.
proof idea
One-line definition that directly substitutes U.ell0 into the expression (2 * π * ell0) / (8 * log phi). No lemmas from the depends_on list are invoked.
why it matters
Supplies the length component for the K-display layer and is used by display_speed_eq_c, display_ratio_scale_invariant, display_null_condition and computeRatios. It completes the parallel to the clock display, supporting the eight-tick structure (T7) via the explicit factor 8 while preserving the structural speed c. No open scaffolding is closed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.