phiL_gt_onePointFive
plain-language theorem explainer
The golden ratio, reconstructed on the logic-derived real line, strictly exceeds 1.5. Anyone comparing LogicReal constants against ordinary numerical bounds cites this. The proof transports the inequality through toReal and invokes the existing Mathlib-side bound φ > 1.5.
Claim. On the recovered real line, $\varphi_L > \mathrm{fromReal}(1.5)$, where $\varphi_L = (1 + \sqrt{5}_L)/2$ is the golden ratio built from logic-real arithmetic and $\mathrm{fromReal}$ embeds ordinary reals into that line.
background
LogicRealConstants mirrors Recognition Science constants on the recovered real line LogicReal. Each definition is written in logic-real arithmetic; companion theorems show that toReal recovers the ordinary constant from IndisputableMonolith.Constants.
Here $\varphi_L$ is defined as $(1 + \sqrt{5}_L)/2$ via fromReal and the logic-real square root. The map fromReal embeds a Mathlib real into LogicReal; toReal is its inverse on the image. Order is preserved: $x < y$ on LogicReal if and only if toReal x < toReal y.
Upstream, Constants.phi_gt_onePointFive already proves $(1.5:\mathbb{R}) < \varphi$ from $\sqrt{5} > 2$. The transport identity toReal phiL = Constants.phi links the two presentations.
proof idea
Term-mode rewrite chain. Rewrite the goal with lt_iff_toReal_lt to move the comparison onto ordinary reals, then simplify the left side by toReal_fromReal and the right side by toReal_phiL. The residual goal is exactly Constants.phi_gt_onePointFive, which is applied directly.
why it matters
Closes the lower numerical bound for the recovered golden ratio on the logic-real line, matching the ordinary RS constant $\varphi$ forced at T6 as the self-similar fixed point. The module's program is that every RS constant (tick, octave, $J$-bit, $\hbar$, $G$, $\alpha^{-1}$, ...) has a LogicReal twin whose toReal image is the classical value; this lemma is the first strict inequality in that twin family.
No downstream users are recorded yet. It stands ready for any LogicReal argument that needs $\varphi_L > 3/2$ without dropping to Mathlib reals mid-proof, and pairs with the companion upper-bound recovery noted in the next doc-comment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.