phi_sq
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.