phi_squared
plain-language theorem explainer
The golden ratio satisfies φ² = φ + 1. Recognition theorists cite this when constructing the phi-ladder for mass formulas and when deriving the fixed-point relation used in J-minimization. The proof is a one-line simplification that reduces the constant to Mathlib's goldenRatio and invokes its square identity.
Claim. Let φ denote the golden ratio. Then φ² = φ + 1.
background
The PhiSupport.Lemmas module collects elementary support facts for the golden ratio in Recognition Science certificates. The sibling lemma phi_def equates the phi field of the CPM constants bundle to Mathlib's Real.goldenRatio. Upstream, the main PhiSupport module supplies the closed-form definition φ = (1 + √5)/2 and directly verifies the square relation by algebraic expansion. The local setting is real-number algebra that underpins the self-similar fixed point required by the forcing chain.
proof idea
One-line wrapper that applies simp with the phi_def unfolding and Mathlib's Real.goldenRatio_sq lemma.
why it matters
This identity supplies the algebraic core for the fixed-point corollary phi_fixed_point and for the downstream astrophysics results imf_from_j_minimization and information_balance_gives_phi. It realizes the T6 step that forces phi as the self-similar fixed point and supports the eight-tick octave construction. No open scaffolding remains at this level.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.