phi_sq
The golden ratio satisfies φ² = φ + 1 by definition from its quadratic equation. Workers on the phi-ladder, J-cost bounds, or self-similar fixed points in Recognition Science cite this identity when deriving mass rungs or T6 relations. The proof is a direct term reference to the algebraic identity already established in Constants.
claim$φ² = φ + 1$ where $φ = (1 + √5)/2$ is the positive root of $x² - x - 1 = 0$.
background
The Inequalities module supplies basic lemmas on the golden ratio and related functions for use in foundation proofs. Phi is introduced in Constants as the positive solution to the quadratic, with the identity φ² = φ + 1 obtained by direct substitution and algebraic simplification. Upstream results include the lemma phi_sq_eq in Constants, which expands the definition via ring_nf and linear_combination on the square of √5, and the parallel statement in PhiLadderLattice that unfolds the same definition.
proof idea
One-line wrapper that applies Constants.phi_sq_eq.
why it matters in Recognition Science
This identity supplies the fixed-point relation that forces phi in the T6 step of the unified forcing chain and underpins the phi-ladder mass formula. It is referenced by sibling inequalities such as J_formula_min_at_one and phi_pos when bounding J-cost or defect distances. No open scaffolding remains; the result closes the algebraic prerequisite for downstream phi-based derivations.
scope and limits
- Does not prove uniqueness of the positive root.
- Does not derive the identity from the Recognition Composition Law.
- Does not supply numerical approximations or bounds on φ.
- Does not extend to complex or negative roots of the quadratic.
formal statement (Lean)
106theorem phi_sq : φ^2 = φ + 1 := Constants.phi_sq_eq
proof body
Term-mode proof.
107
108/-- φ + 1/φ = √5 -/