phi_is_cfrac_fixed_point
plain-language theorem explainer
The golden ratio satisfies the fixed-point equation of the map x ↦ 1 + 1/x. Researchers tracing self-similar attractors in J-cost optimization cite this when anchoring the ground state of sequential choices. The proof is a term reduction that unfolds the iteration definition and applies the symmetric form of the algebraic identity for φ.
Claim. Let φ denote the golden ratio. Then φ equals the image of φ under the map x ↦ 1 + 1/x.
background
The module interprets continued fractions as sequential J-cost optimization. The iteration map is defined by x ↦ 1 + 1/x. The upstream theorem states that φ satisfies x = 1 + 1/x (the continued fraction defining equation), proved from the quadratic φ² = φ + 1 by field simplification. The local setting from the module document is that J(x) = ½(x + x⁻¹) − 1 has a self-similar fixed point at φ, making the infinite nesting converge to this attractor because J is strictly convex on the positive reals.
proof idea
The term proof applies simp to unfold the iteration definition, then invokes the symmetric form of the upstream theorem establishing φ = 1 + 1/φ.
why it matters
This fixed-point statement is invoked by the theorem that identifies the continued-fraction ground state as φ, by the core lemma for φ being worst approximable, and by the theorem that sequential optimization forces φ. It realizes the self-similar fixed point step (T6) in the forcing chain after J-uniqueness (T5), supplying the algebraic anchor that links Ramanujan's identities to the Recognition Science phi-ladder and mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.