phi_continued_fraction_eq
plain-language theorem explainer
The golden ratio satisfies the fixed-point equation φ = 1 + 1/φ that encodes its infinite continued fraction. Number theorists and Recognition Science researchers cite this identity when establishing invariance under the iteration map x ↦ 1 + 1/x or linking continued fractions to J-cost geodesics. The proof is a short algebraic reduction from the quadratic relation φ² = φ + 1, using field simplification after invoking non-vanishing of φ.
Claim. The golden ratio satisfies the equation $φ = 1 + 1/φ$.
background
The module interprets continued fractions as sequential J-cost optimization on the functional J(x) = ½(x + x⁻¹) − 1, whose self-similar fixed point is the unique positive attractor of the recursion x ↦ 1 + 1/x. Upstream results supply the necessary algebraic scaffolding: phi_sq_eq asserts the key identity φ² = φ + 1 (from the defining equation x² − x − 1 = 0), while phi_ne_zero states φ ≠ 0. These lemmas appear in Constants, PhiLadderLattice, and PhiSupport.Lemmas, confirming the quadratic relation holds in the real numbers.
proof idea
The term proof first obtains phi_ne_zero to license division. It then invokes phi_sq_eq to replace φ² with φ + 1. Field simplification rewrites the target equality after division by φ, and nlinarith together with sq_nonneg phi closes the resulting linear relation.
why it matters
This identity supplies the algebraic core for the downstream theorem phi_is_cfrac_fixed_point, which asserts cfracIteration phi = phi. It realizes the self-similar fixed point T6 in the forcing chain and supports the module's interpretation of continued fractions as J-cost geodesics. The result feeds the Fibonacci convergents section and the Ramanujan bridge constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.