phiL_gt_one
plain-language theorem explainer
The recovered golden ratio on the LogicReal line is strictly greater than one. Anyone transporting RS constants through the Cauchy completion of recovered rationals cites this ordering fact before using φ-ladder inequalities. The proof rewrites the LogicReal order via the toReal bridge and applies the classical φ > 1 result.
Claim. On the recovered real line, $1 < \varphi_L$, where $\varphi_L = (1 + \sqrt{5})/2$ is the golden ratio constructed inside $\mathrm{LogicReal}$.
background
LogicRealConstants mirrors Recognition Science constants on LogicReal, the Cauchy completion of the recovered rationals (via Bourbaki reals and the LogicRat ≃ ℚ equivalence). Each constant is defined in LogicReal; companion theorems show that transport by toReal recovers the classical real from IndisputableMonolith.Constants.
The recovered golden ratio is defined by $\varphi_L = (1 + \sqrt{5})/2$ using fromReal and sqrtL. The simp lemma toReal_phiL states toReal($\varphi_L$) = Constants.phi. Order on LogicReal is defined so that $x < y$ if and only if toReal $x$ < toReal $y$ (lt_iff_toReal_lt is definitional). The unit satisfies toReal 1 = 1.
proof idea
One short tactic proof. Rewrite the goal with lt_iff_toReal_lt, then simplify the two sides by toReal_one and toReal_phiL. The resulting real inequality is exactly Constants.phi_gt_one, which is applied directly.
why it matters
In the RS forcing chain, T6 forces φ as the self-similar fixed point of the cost geometry, and every φ-ladder mass and coupling bound needs φ > 1. This lemma places that elementary inequality on the recovered LogicReal line, so later LogicReal constants (tick, octave, ħ, G, α⁻¹) can inherit strict positivity and ordering without dropping back to Mathlib ℝ by hand.
The module's contract is that every LogicReal constant transports to its classical counterpart; phiL_gt_one is the first ordering consequence of that contract for φ. No downstream users are recorded yet, but any proof that needs φ_L > 1 inside LogicReal (ladder steps, eight-tick comparisons, or α-band bounds expressed in LogicReal) will call it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.