octaveL
plain-language theorem explainer
The eight-tick octave, lifted from the ordinary real constant into the logic-derived real line. Anyone citing RS constants inside LogicReal uses this binding. It is a one-line transport of the Mathlib real through the canonical embedding fromReal.
Claim. Let the recovered real line be the Cauchy completion of the logic-derived rationals. The recovered octave is the image of the ordinary real constant $8\tau$ (eight ticks) under the canonical embedding of Mathlib $\mathbb{R}$ into that recovered line.
background
This module mirrors Recognition Science constants on the recovered real line LogicReal. Each constant is written in LogicReal; companion theorems show that transport by toReal recovers the existing Mathlib real from Constants.
LogicReal is the Cauchy completion of the recovered rationals, realized via Mathlib's completion of $\mathbb{Q}$ and the equivalence of logic rationals with $\mathbb{Q}$. The map fromReal sends a Mathlib real $x$ to the corresponding recovered real by the inverse comparison equivalence.
Upstream, Constants.octave is defined as $8\cdot\mathrm{tick}$: one octave equals eight ticks, the fundamental evolution period. That matches the T7 landmark (eight-tick octave, period $2^3$).
proof idea
Pure definition: apply fromReal to Constants.octave. No proof obligations; the body is the transport of the already-defined real octave into LogicReal.
why it matters
Gives the eight-tick period a native name on the recovered line so later LogicReal developments can cite the octave without dropping back to Mathlib reals. Downstream, toReal_octaveL is the simp lemma that closes the round-trip: toReal octaveL = Constants.octave. That is the module's contract for every mirrored constant. Framework landmark T7 (eight-tick octave) is the physical content being mirrored; the definition itself does not re-derive the period, it only places the forced value on LogicReal.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.