toReal_tickL
plain-language theorem explainer
Transporting the recovered tick unit from the logic-constructed reals back to Mathlib's real line yields the fundamental RS time quantum τ₀ = 1. Anyone embedding RS constants on LogicReal and comparing to IndisputableMonolith.Constants would cite this identity. The proof is a one-line round-trip via the fromReal/toReal adjunction.
Claim. If $\tau_L$ denotes the tick unit lifted into the recovered real line, then the transport map sends $\tau_L$ to the RS-native constant $\tau_0 = 1$ on Mathlib's reals.
background
The module LogicRealConstants places Recognition Science constants on the recovered real line LogicReal. Each constant is introduced by lifting the existing real value through fromReal; companion theorems then show that toReal recovers the original Mathlib constant.
The tick is the fundamental RS time quantum: $\tau_0 = 1$ (also written Constants.tick). Its recovered counterpart is defined by lifting that same value. The transport toReal evaluates a recovered real into Mathlib $\mathbb{R}$ via the comparison equivalence of the two real constructions.
Upstream, the round-trip lemma toReal_fromReal states that toReal (fromReal x) = x for every Mathlib real $x$. That identity is the only ingredient needed here.
proof idea
One-line wrapper. Unfold the definition of the recovered tick (it is exactly fromReal of Constants.tick) and apply the round-trip lemma toReal_fromReal, which cancels the lift. The underscore supplies the implicit real argument. Marked @[simp] so downstream rewrites fire automatically.
why it matters
Closes the transport identity for the fundamental time quantum inside the LogicReal mirror of RS constants. Together with the sibling identities for $\varphi$, the octave, $\hbar$, and $\alpha^{-1}$, it certifies that every named RS constant on the recovered line agrees with IndisputableMonolith.Constants after transport.
The tick anchors the eight-tick octave (forcing-chain T7): one octave equals eight ticks, the fundamental evolution period. Keeping $\tau_0 = 1$ coherent across the two real lines is a prerequisite for any later comparison of discrete ledger timing with continuum physics. No downstream users are recorded yet; the lemma is infrastructure for that bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.