phiL_lt_onePointSixTwo
plain-language theorem explainer
The recovered golden ratio on the logic-real line is strictly less than 1.62. Anyone needing a concrete numerical ceiling on the LogicReal copy of φ cites this. The proof is a short transport: compare after toReal, then invoke the existing real bound φ < 1.62.
Claim. Let $\varphi_L$ be the golden ratio constructed in the recovered logic-real line by $\varphi_L = (1 + \sqrt{5})/2$. Then $\varphi_L < \iota(1.62)$, where $\iota$ embeds ordinary reals into that line.
background
LogicRealConstants mirrors Recognition Science constants on the recovered real line LogicReal. Each constant is defined in LogicReal, and companion theorems show that transport by toReal recovers the ordinary real constant from IndisputableMonolith.Constants.
Here $\varphi_L$ is defined exactly as $(1 + \sqrt_L 5)/2$ using the logic-real square root and the embedding fromReal. The sibling identity toReal_phiL states toReal $\varphi_L$ = Constants.phi. On the ordinary reals, Constants.phi_lt_onePointSixTwo already gives the tighter ceiling $\varphi < 1.62$ (from $\sqrt{5} < 2.24$).
The comparison lemma lt_iff_toReal_lt lets inequalities on LogicReal be decided after transport to $\mathbb{R}$.
proof idea
Rewrite the goal with lt_iff_toReal_lt, so it becomes an ordinary real inequality between toReal phiL and toReal (fromReal 1.62). Simplify the right side by toReal_fromReal and the left by the simp lemma toReal_phiL, reducing exactly to Constants.phi < 1.62. Finish by exact Constants.phi_lt_onePointSixTwo.
why it matters
φ is forced in the Recognition chain as the self-similar fixed point (T6). Numerical control of that constant, once lifted to the logic-real mirror, keeps later LogicReal identities (tick, octave, ħ, α⁻¹, etc. in this module) inside certified bounds without dropping back to ad-hoc real arithmetic.
The module’s charter is that every LogicReal constant transports to its Constants counterpart; this lemma is the matching strict upper bound for φ. No downstream users are wired yet (used_by empty), so it is presently a certified numerical fact ready for later forcing or certification steps that need φ_L < 1.62 on the recovered line.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.