toReal_octaveL
plain-language theorem explainer
Transporting the LogicReal octave back to Mathlib reals recovers the standard RS octave constant (eight ticks). Anyone equating constants on the recovered real line with IndisputableMonolith.Constants cites this. The proof is a one-line application of the round-trip identity toReal ∘ fromReal = id.
Claim. If $\mathrm{octave}_L$ is the octave constant lifted into the logic-recovered real line via $\mathrm{fromReal}$, then $\mathrm{toReal}(\mathrm{octave}_L)$ equals the ordinary real octave $8\cdot\mathrm{tick}$.
background
LogicRealConstants mirrors Recognition Science constants on the recovered real line (LogicReal). Each definition is built by fromReal of an existing Mathlib real from IndisputableMonolith.Constants; companion theorems show that toReal undoes the lift.
The octave is the fundamental evolution period: one octave equals eight ticks (Constants.octave := 8 * tick). That period is the T7 landmark in the forcing chain (period $2^3$). The LogicReal copy is octaveL := fromReal Constants.octave.
toReal transports a LogicReal value into Mathlib's $\mathbb{R}$ via the comparison equivalence. The key upstream identity is toReal_fromReal: for every real $x$, toReal (fromReal x) = x.
proof idea
One-line wrapper. Unfold octaveL as fromReal Constants.octave and apply toReal_fromReal, which states that toReal is a left inverse of fromReal on Mathlib reals. The underscore fills the real argument automatically. Marked @[simp] so downstream rewrites fire without naming the lemma.
why it matters
Closes the LogicReal bridge for the eight-tick octave, the T7 forcing-chain landmark (period $2^3$). Without this identity, any computation that mixes LogicReal constants with Mathlib reals would have to re-prove the round trip by hand. Sibling lemmas do the same for $\varphi$, the tick, $J$-bit, $\hbar$, $G$, and $\alpha^{-1}$. No downstream users are recorded yet; the lemma is infrastructure for later constant-transport proofs in the foundation layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.