toReal_phiL
plain-language theorem explainer
Transport of the recovered golden ratio through the LogicReal-to-real map equals the standard Mathlib constant φ. Bound and positivity lemmas for the recovered φ cite this identity, as does the hbar transport theorem. The proof is a one-line simp unfolding the algebraic definition and the fromReal round-trip.
Claim. If $\varphi_L$ denotes the golden ratio constructed on the recovered real line as $(1+\sqrt{5})/2$, then the canonical transport $\mathrm{toReal}:\mathrm{LogicReal}\to\mathbb{R}$ satisfies $\mathrm{toReal}(\varphi_L)=\varphi$, where $\varphi$ is the usual real golden ratio.
background
LogicRealConstants mirrors Recognition Science constants on the recovered real line LogicReal. Each constant is defined inside LogicReal; companion theorems show that transport via toReal recovers the corresponding entry of IndisputableMonolith.Constants.
The recovered golden ratio is built algebraically as $(1+\sqrt{5})/2$ using fromReal and the recovered square root. The transport toReal is comparison along the equivalence between the recovered completion and Mathlib's $\mathbb{R}$. The key upstream fact is the round-trip identity toReal (fromReal x) = x, so pure real literals and rational combinations push forward unchanged.
In the broader framework, $\varphi$ is the self-similar fixed point forced at T6 of the UnifiedForcingChain; placing it on the recovered line is the first step toward expressing RS-native units ($\hbar=\varphi^{-5}$, etc.) without leaving the logical construction.
proof idea
One-line simp wrapper. Unfold the definition of the recovered golden ratio and of Constants.phi, then apply the round-trip lemma toReal_fromReal so every fromReal literal cancels. No arithmetic or inequality reasoning is required; the equality is definitional once transport is simplified.
why it matters
This is the bridge that lets every subsequent inequality about the recovered $\varphi$ reduce to a known fact about Mathlib's $\varphi$. Downstream, positivity (phiL_pos), the bounds $\varphi_L>1$, $\varphi_L>1.5$, $\varphi_L<1.62$, and the hbar transport identity all rewrite through this simp lemma and then invoke the corresponding real theorem.
In the Recognition chain it anchors T6 (phi forced as the self-similar fixed point) on the recovered line, so later RS-native constants built from powers of $\varphi$ (notably $\hbar=\varphi^{-5}$) inherit a clean transport. Without it, the LogicReal mirror of the constant ladder would be disconnected from the verified real numerics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.