phi_fixed_point'
The golden ratio satisfies the fixed-point equation φ = 1 + φ^{-1}. Recognition Science derivations cite this when anchoring self-similar scaling from the quadratic identity. The proof reduces the squared form by division justified by positivity, followed by algebraic simplification.
claimThe golden ratio satisfies the equation $φ = 1 + φ^{-1}$.
background
The PhiSupport module records algebraic identities for the golden ratio φ. The upstream theorem phi_squared states that φ² = φ + 1, which is the defining quadratic equation derived from the closed-form expression φ = (1 + √5)/2. As stated in the upstream result: 'φ² = φ + 1: The defining equation of the golden ratio.' This fixed-point form follows by rearrangement and anchors the self-similar scaling in the Recognition framework.
proof idea
The proof invokes the phi_squared theorem to obtain φ² = φ + 1. It then applies field_simp to clear the division by φ (justified by positivity) and uses linarith to equate the sides after simplification.
why it matters in Recognition Science
This result supplies the fixed-point characterization of φ required for the self-similar fixed point in the forcing chain (T6). It supports derivations of the eight-tick octave and the mass ladder by providing the recurrence relation φ = 1 + 1/φ. No downstream uses are recorded yet, but it closes the algebraic foundation for phi-based constants in the framework.
scope and limits
- Does not prove uniqueness of the fixed point beyond positivity.
- Does not connect the fixed point to the J-uniqueness or RCL.
- Does not derive numerical approximations or physical constants from this equation.
formal statement (Lean)
27theorem phi_fixed_point' : phi = 1 + phi⁻¹ := by
proof body
Term-mode proof.
28 have hphi_pos : phi > 0 := phi_pos
29 have hphi_ne : phi ≠ 0 := ne_of_gt hphi_pos
30 -- From phi_squared: φ² = φ + 1
31 -- Divide both sides by φ: φ = 1 + 1/φ
32 have h := phi_squared
33 field_simp at h ⊢
34 linarith
35
36/-- φ > 1: The golden ratio is strictly greater than 1.
37
38 This is already proven in Constants.lean -/