tau_rec_display
plain-language theorem explainer
This definition supplies the explicit formula for the clock-side display period in Recognition Science units: the period equals (2π times the fundamental tick duration) divided by (8 times the natural log of the golden ratio). Researchers on K-display invariants and unit-gate certificates cite this when computing normalized rates or verifying null conditions. It is introduced by a direct one-line expression with no additional lemmas or reductions.
Claim. $τ_{rec}(display) = (2π τ_0)/(8 ln φ)$, where $τ_0$ is the fundamental tick duration from the minimal units structure.
background
The minimal units structure holds the fundamental time unit $τ_0$ (duration of one tick), length unit $ℓ_0$, and speed $c$ satisfying $c τ_0 = ℓ_0$. Upstream definitions set $τ_0$ as the base tick duration in native units, either as a placeholder or derived from $ℏ$, $G$, and $c$. The constant $φ$ is the golden ratio fixed point from the forcing chain. This definition resides in the module that isolates display expressions for time and length scales. It builds directly on the upstream units structure and tick-duration definitions that supply the input value. The factor of eight encodes the octave period from the unified forcing chain.
proof idea
The declaration is a direct definition that returns the algebraic expression (2 * π * input.τ_0) / (8 * log φ) for the given units input. No lemmas or tactics are applied; the body consists of the explicit formula using the standard real constants for π and the logarithm.
why it matters
It supplies the clock component for ratio computations in the units-gate certificate and is invoked to prove that display speed equals $c$ and that the null condition holds. The definition encodes the eight-tick octave scaling into the display period, linking the base tick to observable kinematic scales. It supports the scale-invariance and equivalence results in the surrounding display module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.