tau_rec_eq_K_gate_ratio
plain-language theorem explainer
The theorem shows that the recognition time display equals the K-gate ratio π/(4 ln φ) in RS-native units where the tick is unity. Workers on the φ-ladder or clock-side constants cite it to lock the display definitions together. The proof unfolds the time definition, invokes positivity of log φ, simplifies the explicit expressions, and finishes with field simplification plus ring arithmetic.
Claim. In RS-native units with fundamental tick τ₀ = 1, the recognition time display satisfies τ_rec = π / (4 ln φ), where φ denotes the golden ratio.
background
The RS-native units module treats the ledger tick τ₀ = 1 as the base time quantum and voxel as the base length, with c = 1. Recognition time display is defined as (2π τ₀) / (8 ln φ). K-gate ratio is defined directly as π / (4 ln φ). The upstream lemma one_lt_phi supplies 1 < φ, which guarantees ln φ > 0 and permits the later field simplification. The module organizes all derived quantities on the φ-ladder with the eight-tick octave as the fundamental period.
proof idea
Unfold the definition of τ_rec to expose the display expression. Introduce the auxiliary fact that ln φ ≠ 0 from one_lt_phi. Apply simp to substitute the K-gate ratio definition, the display definition, and tick = 1. Close with field_simp on the nonzero logarithm followed by ring to equate the two sides.
why it matters
The equality anchors the clock-side display definition inside the constants module and confirms internal consistency of the RS unit system. It supports the φ-ladder scaling and the eight-tick octave (T7) by fixing the numerical prefactor π/(4 ln φ). No downstream theorems yet reference it, but it closes a potential gap between the kinematic and gate-ratio presentations of the same quantity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.