phi_fixed_point
plain-language theorem explainer
φ equals one plus its reciprocal. Researchers deriving cost fixed points and self-similar structures in Recognition Science cite this identity when building the phi-ladder. The proof is a short calc chain that substitutes the quadratic relation φ² = φ + 1 and cancels using field arithmetic.
Claim. $φ = 1 + 1/φ$
background
The PhiSupport.Lemmas module records elementary facts about the golden ratio for certificates. It includes φ² = φ + 1 from Mathlib, the fixed-point identity, and uniqueness of the positive root of x² = x + 1. These rest only on real algebra. Upstream lemmas supply one_lt_phi (1 < φ) and phi_ne_zero (φ ≠ 0) from the Constants module.
proof idea
The proof invokes phi_squared to obtain φ² = φ + 1. A calc block rewrites φ as φ²/φ, substitutes the quadratic, splits the division, and cancels φ/φ = 1 using phi_ne_zero.
why it matters
This supplies the algebraic identity required by the downstream lemma phi_is_cost_fixed_point in Cost.FixedPoint. It realizes the self-similar fixed point at forcing-chain step T6. The identity supports the phi-ladder for mass formulas and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.