phi_squared
plain-language theorem explainer
The golden ratio satisfies φ² = φ + 1 by direct algebraic reduction from its closed form. Recognition Science modelers and astrophysicists cite this identity when anchoring the phi-ladder for mass formulas and deriving information-balance relations. The proof unfolds the definition of phi, invokes the square root identity for 5, then reduces via field simplification and ring normalization.
Claim. The golden ratio satisfies the equation $φ^2 = φ + 1$.
background
In the PhiSupport module phi is the golden ratio, the positive real root of the quadratic x² = x + 1, equivalently (1 + √5)/2. This supplies the self-similar fixed point required by the Recognition Science forcing chain at step T6. The module imports Constants for the definition and PhiLadderLattice for lattice structures that assume the same algebraic relation.
proof idea
The tactic proof unfolds the definition of phi, proves (0 : ℝ) ≤ 5 by norm_num, records Real.sqrt(5)² = 5, then applies field_simp followed by ring_nf, rewrites with the square identity, and finishes with ring.
why it matters
This identity is the algebraic base for phi_fixed_point' and phi_fixed_point, which derive the fixed-point form φ = 1 + 1/φ. It feeds directly into ObservabilityLimits theorems information_balance_gives_phi and imf_from_j_minimization, where φ² ≈ 2.618 appears in slope estimates near the Salpeter value 2.35. Within the framework it realizes the self-similar fixed point used by the eight-tick octave and the D = 3 spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.