tickL
plain-language theorem explainer
The fundamental RS time quantum (one tick, τ₀ = 1) lifted onto the recovered real line via the canonical Mathlib-to-LogicReal transport. Anyone building LogicReal-side constants or transport lemmas cites this binding. The body is a one-line definition: apply fromReal to Constants.tick.
Claim. Define the recovered tick unit as the image of the RS-native time quantum $\tau_0 = 1$ under the canonical embedding of Mathlib reals into the recovered real line $\mathrm{LogicReal}$.
background
This module mirrors Recognition Science constants on the recovered real line. Each constant is written as a LogicReal value; companion theorems show that transport by toReal recovers the ordinary real from Constants.
The RS tick is the fundamental time quantum: $\tau_0 = 1$ in RS-native units (also written tick). One octave is eight ticks, the fundamental evolution period forced by the eight-tick structure (T7 in the forcing chain).
LogicReal is the Cauchy completion of the recovered rationals, realized via Mathlib's completion of $\mathbb{Q}$ and the equivalence with logic-derived rationals. The map fromReal sends a Mathlib real $x$ to the corresponding recovered real by the inverse comparison equivalence.
proof idea
One-line definition. Apply fromReal to Constants.tick (the real value $1$). No tactics or lemmas beyond the transport constructor.
why it matters
Gives the LogicReal-side name for the tick so the rest of the constant suite (octave, $\hbar$, $\alpha^{-1}$, etc.) can be stated uniformly on the recovered line. The immediate consumer is toReal_tickL, which proves toReal tickL = Constants.tick by the general toReal_fromReal identity.
In the framework this is bookkeeping for the eight-tick octave: once the tick lives on LogicReal, the octave $8\cdot\tau_0$ and the period-$2^3$ evolution structure can be mirrored without leaving the recovered reals. It does not itself force the octave; it only places the unit where later forcing and constant theorems can use it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.