lambda_kin_display
plain-language theorem explainer
lambda_kin_display defines the kinematic display length as (2π ℓ₀) / (8 ln φ) for any RSUnits pack U. Researchers checking K-gate certificates or display speed equalities in Recognition Science cite it when confirming scale-invariant ratios. The definition is a direct noncomputable expression that substitutes the fundamental length ell0 and the logarithm of phi.
Claim. For an RSUnits structure $U$, the kinematic display length is defined by $λ_{kin}(display) = (2π · ℓ₀) / (8 ln φ)$, where $ℓ₀$ is the fundamental length unit satisfying the RSUnits relation $c · τ₀ = ℓ₀$.
background
Constants.KDisplayCore supplies the length-side display definitions that parallel the clock-side recurrence definitions in the same module. RSUnits is the structure containing τ₀, ℓ₀, and c with the built-in constraint c · τ₀ = ℓ₀. Upstream ell0 sets the fundamental length to 1 in native units or to c · τ₀ in codata derivations; K is defined as φ^{1/2}. Phi is the self-similar fixed point forced by the T6 step of the UnifiedForcingChain.
proof idea
This is a direct definition that evaluates the expression (2 * Real.pi * U.ell0) / (8 * Real.log phi). It imports ell0 from Constants and the constant phi without invoking any lemmas or reductions.
why it matters
The definition supplies the length display quantity used by display_speed_eq_c, display_null_condition, and display_ratio_scale_invariant to establish that λ_kin / τ_rec equals the structural speed c. It is called inside computeRatios for UnitsKGate certificates. In the framework it realizes the length counterpart to the eight-tick octave scaling, supporting the bridge from RS-native units to observable display rates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.