tau_rec
plain-language theorem explainer
The definition supplies the recognition time display τ_rec = (2π τ₀)/(8 ln φ) inside the RS-native gauge. Researchers scaling discrete ledger intervals to kinematic time would cite it when working with the φ-ladder. It is realized as a direct wrapper that applies the display formula from KDisplayCore to the unit structure U.
Claim. In RS-native units the recognition time display is defined by $τ_{rec} = (2π τ_0)/(8 ln φ)$ where $τ_0$ is the base tick interval set to unity.
background
The RSNativeUnits module establishes a self-contained measurement system whose base standards are the ledger primitives tick (τ₀) and voxel (ℓ₀). Time is introduced as the abbreviation ℝ. The structure RSUnits packages the triple (τ₀, ℓ₀, c) together with the constraint c τ₀ = ℓ₀; the gauge U instantiates this structure by setting τ₀ = tick, ℓ₀ = voxel and c = 1. The upstream definition tau_rec_display (KDisplayCore) encodes the explicit formula (2 π U.τ₀) / (8 Real.log phi).
proof idea
One-line wrapper that applies Constants.RSUnits.tau_rec_display to the native gauge U.
why it matters
The definition supplies the time-scale entry required by the module status summary and by the downstream equality tau_rec_eq_K_gate_ratio. It encodes the eight-tick octave factor (T7) through the denominator 8 ln φ, consistent with the self-similar fixed point φ fixed at T6. The construction keeps all ratios dimensionless and determined solely by φ, as required by the Recognition Science unit system.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.