pith. machine review for the scientific record. sign in
def definition def or abbrev high

lambda_kin_display

show as:
view Lean formalization →

The kinematic display length λ_kin(display) is defined for any RSUnits gauge U as (2π U.ℓ₀) / (8 ln φ). Certificate authors cite it when they need the length counterpart to the clock display τ_rec(display) for verifying scale-invariant ratios and null conditions. The definition is a direct algebraic expression with no internal lemma applications.

claimFor a structure $U$ of type RSUnits, the kinematic display length is defined by $λ_{kin}(U) := (2π · U.ℓ₀) / (8 ln φ)$.

background

Recognition Science works inside the RSUnits structure that packages the native gauge values τ₀ (tick), ℓ₀ (voxel) and c together with the compatibility relation c τ₀ = ℓ₀. The constant ℓ₀ is the fundamental voxel length, returned as the constant 1 by the upstream definition ell0. The golden ratio φ is the self-similar fixed point forced by the Recognition Composition Law. The module KDisplayCore supplies the two display-scale constants that convert between structural and observable units while preserving the null condition (λ/τ)² = c².

proof idea

The declaration is a direct noncomputable definition whose body is the expression (2 * Real.pi * U.ell0) / (8 * Real.log phi). No lemmas are applied inside the body; the expression is taken verbatim as the definition of the kinematic display length.

why it matters in Recognition Science

This definition supplies the length-side input to the K-gate ratio certificates and to the family of display lemmas that establish (λ_kin / τ_rec) = c. It is used by computeRatios, display_speed_eq_c_of_nonzero, display_ratio_scale_invariant and display_speed_eq_c. The factor 8 in the denominator traces to the eight-tick octave (T7) of the forcing chain, while the logarithm of φ encodes the self-similar scaling fixed by J-uniqueness (T5). The declaration completes the length half of the display bridge that recovers Lorentz structure at the observable level.

scope and limits

formal statement (Lean)

  14@[simp] noncomputable def lambda_kin_display (U : RSUnits) : ℝ :=

proof body

Definition body.

  15  (2 * Real.pi * U.ell0) / (8 * Real.log phi)
  16
  17/-- The K-gate ratio constant. -/

used by (18)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (9)

Lean names referenced from this declaration's body.