tau_rec_display_pos
plain-language theorem explainer
Positivity of the recursive display time τ_rec_display holds for any RSUnits structure with positive fundamental tick duration τ₀. It is cited when removing nonzero hypotheses from display-speed equalities that equate kinematic and structural speeds. The proof unfolds the definition (2π τ₀)/(8 ln φ) and invokes the positivity tactic after establishing positivity of π and log φ.
Claim. Let $U$ be an RSUnits structure with $0 < U.τ_0$. Then $0 < τ_{rec display}(U)$, where $τ_{rec display}(U) = (2π U.τ_0)/(8 ln φ)$.
background
The module treats the dimensionless bridge ratio K together with display equalities. RSUnits is the structure holding fundamental tick duration τ₀, length ℓ₀, and speed c subject to c τ₀ = ℓ₀. The display recursion time is defined in KDisplayCore by τ_rec_display(U) := (2 Real.pi U.τ₀) / (8 Real.log phi). The supporting lemma one_lt_phi states 1 < phi, which forces log phi > 0.
proof idea
Unfold tau_rec_display. Obtain 0 < Real.pi from Real.pi_pos. Obtain 0 < Real.log phi from Real.log_pos applied to one_lt_phi. Apply the positivity tactic to conclude the strict inequality.
why it matters
The lemma is invoked by tau_rec_display_ne_zero to discharge the nonzero hypothesis in display_speed_eq_c_of_nonzero, yielding (lambda_kin_display U) / (tau_rec_display U) = U.c without extra assumptions. The factor 8 in the denominator aligns with the eight-tick octave of the forcing chain; positivity therefore guarantees that the kinematic display speed matches the structural speed c in RS-native units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.