phi_gt_one
plain-language theorem explainer
The golden ratio exceeds one. Researchers building the phi-ladder or invoking self-similarity axioms cite this inequality as an immediate prerequisite. The proof is a one-line wrapper that applies the established constant lemma from the Constants module.
Claim. The golden ratio satisfies $1 < phi$.
background
The PhiEmergence module derives the golden ratio from J-cost minimization under the Recognition Composition Law. Here phi denotes the positive solution to $x^2 = x + 1$, equivalently $(1 + sqrt(5))/2$. The upstream Constants module records one_lt_phi via explicit square-root comparison: $1 < sqrt(5)$ yields $2 < 1 + sqrt(5)$, hence $1 < phi$. PhiSupport and its Lemmas re-export the same fact for local use.
proof idea
The proof is a one-line wrapper that applies Constants.one_lt_phi.
why it matters
This inequality anchors every subsequent phi-ladder construction and the self-similarity theorems in the same module. It supplies the strict positivity needed for T6, where phi emerges as the self-similar fixed point of the forcing chain. No downstream results are recorded yet; the fact remains a basic prerequisite rather than a derived claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.