tau_rec_display_ratio
plain-language theorem explainer
The lemma shows that the clock-side display ratio (tau_rec_display U) divided by the fundamental tick tau0 equals the constant K_gate_ratio = pi/(4 ln phi). Physicists deriving unit-invariant quantities from the Recognition Science forcing chain would cite this when establishing equivalence of displays under rescaling. The proof is a direct algebraic reduction: unfold the definitions of tau_rec_display and K_gate_ratio, then simplify the resulting expression using field_simp and ring.
Claim. For an RSUnits structure $U$ with $U.tau0 ≠ 0$, let $τ_{rec}(display) = (2π · U.tau0)/(8 ln φ)$. Then $τ_{rec}(display)/U.tau0 = π/(4 ln φ)$.
background
In the KDisplayCore module the clock-side display is defined by tau_rec_display U := (2 * pi * U.tau0) / (8 * log phi). The K_gate_ratio constant is defined as pi / (4 * log phi). RSUnits is the minimal structure carrying the fundamental units tau0, ell0, c with the relation c * tau0 = ell0. This lemma connects the display definition to the gate ratio used in invariance proofs. Upstream results supply the fundamental tick duration tau0 in RS-native units, consistent with the eight-tick octave and phi-ladder from the forcing chain.
proof idea
The proof unfolds the definitions of tau_rec_display and K_gate_ratio. It then applies field_simp using the hypothesis that tau0 is nonzero to clear the denominator, followed by the ring tactic to verify the algebraic identity.
why it matters
This result is used directly in K_gate_eqK to show both clock and length sides equal the K-gate ratio, and in the invariance theorems displays_invariant_under_equivalence and units_quotient_preserves_K. It fills the step linking the display definition to the constant derived from the Recognition Composition Law and the phi fixed point. It supports the claim that K-gate is independent of units choice in the RS framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.