phi_sq_eq
plain-language theorem explainer
The golden ratio satisfies the quadratic relation φ² = φ + 1. Researchers deriving the phi-ladder lattice or applying J-cost to self-similar structures in aesthetics, archaeology, and astrophysics cite this identity. The proof unfolds the explicit definition of φ as (1 + √5)/2, records that (√5)² = 5, then applies field_simp and nlinarith to verify the squared term equals the right-hand side.
Claim. $φ² = φ + 1$, where $φ = (1 + √5)/2$ denotes the golden ratio.
background
The phi-ladder lattice is the discrete hierarchy forced by Recognition Science theorem T6 on the multiplicative half-line. It consists of the geometric sequence {φ^r : r ∈ ℤ}, which becomes an arithmetic progression on the log scale and admits Poisson summation. The module defines phi explicitly as (1 + √5)/2 together with phiRung, phiLatticePoint, and the reciprocal involution on rungs.
proof idea
The tactic proof first unfolds the definition of phi. It introduces the auxiliary fact that (√5)² = 5 via Real.mul_self_sqrt. An auxiliary equality is then constructed showing ((1 + √5)/2)² equals the same quantity plus one, using field_simp followed by nlinarith on the square fact. The result is discharged by exact.
why it matters
This identity supplies the algebraic engine for the phi-ladder and is invoked by forty downstream declarations, including beautyScore_at_phi (which obtains 3/2 − φ), adjacencyGap_eq, settlementPopRatio_in_Christaller_band, phi_golden_recursion, alfvenToSolarWindRatio_gt_one, and phi_cubed_eq. It realizes the self-similar fixed point required by forcing-chain step T6 and underpins reciprocal symmetry of the J-cost function on the ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.