lambda_kin_eq_K_gate_ratio
plain-language theorem explainer
lambda_kin equals the K-gate ratio in RS-native units, aligning the kinematic length scale with the clock-side gate expression. Researchers deriving Planck-scale quantities from gate identities cite this to confirm consistency across length and time expressions. The proof unfolds the lambda_kin definition, invokes log phi nonzero from one_lt_phi, simplifies the unit display forms, then closes via field_simp and ring.
Claim. $λ_{kin} = π / (4 ln φ)$ in RS-native units, where φ denotes the golden ratio and the equality holds with voxel length set to unity.
background
The RSNativeUnits module defines a native measurement system whose base units are the tick (atomic time quantum τ₀) and voxel (spatial step ℓ₀ with c = 1). Derived quanta are the coherence energy coh = φ^{-5} and action act = ħ. All dimensionless ratios are fixed by powers of φ on the phi-ladder, with no external SI anchoring required.
proof idea
The term proof first unfolds lambda_kin. It introduces the auxiliary fact Real.log phi ≠ 0 via ne_of_gt (Real.log_pos one_lt_phi). Simplification then applies the display definitions lambda_kin_display and K_gate_ratio together with the RSUnits structure U and the voxel constant. Field_simp on the nonzero logarithm followed by ring finishes the algebraic identity.
why it matters
The equality anchors the Planck-scale quantities section that follows, where Planck time emerges from gate identities rather than postulates. It supports the first-principles derivation of G = λ_rec² c³ / (π ħ) by ensuring kinematic and gate expressions share the same φ-scaling. In the broader framework it reinforces the self-similar fixed point φ and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.