phi_cost_fixed_point
plain-language theorem explainer
The golden ratio satisfies the fixed-point equation φ = 1 + 1/φ. Researchers constructing self-similar frequency ladders in Recognition Science cite this when identifying minimal-cost resonances above a base frequency f. The proof is a one-line algebraic reduction that invokes the quadratic identity φ² = φ + 1, clears the denominator with field simplification, and closes with linear arithmetic.
Claim. The golden ratio satisfies $φ = 1 + φ^{-1}$.
background
The J-cost function J(r) = ½(r + r^{-1}) − 1 measures the cost of any positive ratio r. The module establishes that φ is the unique positive fixed point of the self-similar recursion r = 1 + 1/r, i.e., the equation r² = r + 1. This supplies the first rung of the φ-ladder: for any frequency f the minimal-cost non-trivial resonance is f × φ. The local setting is the φ-Ladder Frequency Bridge, which closes the gap between the multiplicative recognizer cost and the harmonic forcing chain (T5–T6). Upstream, phi_sq_eq supplies the quadratic identity φ² = φ + 1 and phi_ne_zero supplies φ ≠ 0.
proof idea
One-line wrapper that applies phi_sq_eq to obtain φ² = φ + 1, invokes phi_ne_zero to justify division, then executes field_simp followed by linarith.
why it matters
This theorem supplies the algebraic anchor for the φ-harmonic theorem in the same module, which defines the first φ-ladder harmonic f_phi_rung1 := Mode1 × φ. It directly implements the T6 step of the forcing chain (phi forced as the self-similar fixed point) and justifies the minimal-cost resonance claim used in BodyCosmosResonance. No open scaffolding remains; the result is fully discharged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.