phi_gt_one
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the explicit algebraic value of phi.
- Does not invoke J-cost or the Recognition Composition Law.
- Does not establish self-similarity or ladder closure properties.
formal statement (Lean)
29theorem phi_gt_one : φ > 1 := Constants.one_lt_phi
proof body
Term-mode proof.
30
31/-! ## φ Satisfies Self-Similarity -/
32
33/-- **THEOREM**: The golden ratio satisfies r² = r + 1. -/