tau_rec_display_ne_zero
plain-language theorem explainer
The lemma shows that the display recurrence time τ_rec(display) is nonzero whenever the base tick duration τ₀ is positive in an RSUnits structure. Researchers deriving display speeds or scale-invariant ratios in the KDisplay module cite it to justify division by τ_rec. The argument is a one-line wrapper that invokes the companion positivity lemma and applies ne_of_gt.
Claim. Let $U$ be an RSUnits structure with fundamental tick duration satisfying $0 < U.τ₀$. Then the display recurrence time $τ_{rec}(display) := (2π U.τ₀)/(8 ln φ)$ is nonzero.
background
RSUnits is the minimal structure carrying base units τ₀, ℓ₀, c together with the relation c τ₀ = ℓ₀. The definition tau_rec_display unfolds to (2 π τ₀) / (8 log φ), where φ is the self-similar fixed point fixed by the Recognition Composition Law. The upstream lemma tau_rec_display_pos proves 0 < tau_rec_display U under the same hypothesis by unfolding the definition and applying positivity of π together with log φ > 0. The module KDisplay develops dimensionless bridge ratios K and the associated display equalities that equate kinematic and clock-side quantities.
proof idea
The proof is a one-line wrapper that applies tau_rec_display_pos U h to obtain strict positivity of tau_rec_display U and then invokes ne_of_gt to reach the desired inequality.
why it matters
This lemma is invoked directly by display_speed_eq_c to establish that lambda_kin_display / tau_rec_display equals c, and by display_ratio_scale_invariant to obtain scale invariance of the ratio. It supplies the non-vanishing prerequisite needed for the KDisplay development of the dimensionless bridge ratio K. In the Recognition framework it secures the denominator in the eight-tick octave expression (T7) that appears in native-unit display quantities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.