fibonacci_ratio_fixed_point
plain-language theorem explainer
The golden ratio φ satisfies φ = 1 + 1/φ. Workers on J-cost minimization for cache hierarchies cite this to confirm that any Fibonacci recurrence forces the φ ratio as its fixed point. The proof is a direct algebraic reduction that invokes the identity φ² = φ + 1, clears the denominator by field simplification, and closes with nonlinear arithmetic.
Claim. The golden ratio satisfies the fixed-point equation $φ = 1 + 1/φ$.
background
In the module on J-cost gradient flow, a hierarchy is a sequence of positive reals K : ℕ → ℝ giving cache capacities at successive levels. The total J-cost is the sum over adjacent levels of J(K(ℓ+1)/K(ℓ)). When the hierarchy obeys the Fibonacci recurrence K(n+2) = K(n+1) + K(n) with positive terms, the successive ratios r_n = K(n+1)/K(n) satisfy the map r ↦ 1 + 1/r. The upstream lemma phi_sq_eq records the identity φ² = φ + 1 that defines the golden ratio.
proof idea
The proof first obtains φ ≠ 0 and φ² = φ + 1 from the constants module. It then applies field_simp to rewrite the target equality and finishes with nlinarith using the nonnegativity of φ² together with positivity of φ.
why it matters
This supplies the algebraic step that any Fibonacci partition forces the φ ratio, closing the loop to the claim that the φ-geometric sequence is the unique self-similar minimum of the J-cost functional. It supports the module's larger result that gradient descent on hierarchies converges to the Fibonacci/φ partition and corresponds to the T6 forcing of φ as the self-similar fixed point in the Recognition Science chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.