display_speed_positive
plain-language theorem explainer
The theorem shows that the kinematic display speed, the ratio of λ_kin(display) to τ_rec(display) in RS units, is strictly positive when the fundamental tick duration τ₀ and speed of light c are positive. Researchers verifying null-cone structure and K-gate consistency in Recognition Science constants would cite it to confirm lightlike propagation. The proof is a one-line wrapper that rewrites the ratio to c via display_speed_eq_c and invokes the given positivity of c.
Claim. Let $U$ be an RSUnits structure satisfying $0 < U.τ₀$ and $0 < U.c$. Then $0 < λ_{kin}(display)(U) / τ_{rec}(display)(U)$.
background
The KDisplay module treats the dimensionless bridge ratio K together with display equalities that map RS-native units to observable lengths and times. RSUnits is the minimal structure carrying τ₀ (fundamental tick duration), ℓ₀ (length scale), and c (speed of light) with the relation c τ₀ = ℓ₀. The kinematic display length is defined by λ_kin(display) = (2π ℓ₀) / (8 ln φ) while τ_rec(display) supplies the matching recurrence time; upstream display_speed_eq_c equates their ratio to c once τ₀ > 0.
proof idea
The proof is a one-line wrapper. It rewrites the target ratio by the lemma display_speed_eq_c (which reduces it to c) and then applies the hypothesis that c is positive.
why it matters
The result secures positivity of the display speed, confirming lightlike (null-cone) behavior inside the Recognition constants layer. It supports K-gate invariance and scale-invariance claims in the same module, consistent with the eight-tick octave and RS-native units where c = 1. No downstream uses are recorded, but the lemma closes a basic positivity gate required for any further display-layer derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.