phi_hierarchy_is_unique_fixed_point
plain-language theorem explainer
Any positive real sequence obeying the Fibonacci recurrence with constant ratio r must be the geometric sequence with ratio phi. Researchers modeling J-cost gradient flow on cache hierarchies cite this to confirm the phi-partition is the sole fixed point. The proof applies the forcing lemma fibonacci_partition_forces_phi for the ratio equality then inducts on the recurrence to recover the explicit form K_n = K_0 phi^n.
Claim. Let $K : ℕ → ℝ$ be a sequence of positive reals satisfying the Fibonacci recurrence and possessing constant positive ratio $r$. Then $r = ϕ$ and $K_n = K_0 ⋅ ϕ^n$ for every natural number $n$.
background
In the J-cost gradient flow on hierarchies, a hierarchy is a sequence $K : ℕ → ℝ$ of positive cache capacities whose total cost is $∑ J(K(ℓ+1)/K(ℓ))$. Under the Fibonacci partition constraint forced by J-symmetry at optimal boundaries, the unique self-similar minimum is the geometric sequence with ratio ϕ. The module first constructs the ϕ-hierarchy and then proves it is the only constant-ratio Fibonacci sequence. Upstream results include the definition of ϕ as the self-similar fixed point and the lemma fibonacci_partition_forces_phi that extracts the ratio from the recurrence and positivity assumptions.
proof idea
The term proof begins with constructor. The first conjunct is discharged by exact application of fibonacci_partition_forces_phi. The second conjunct proceeds by induction on n: the zero case simplifies directly, while the successor case rewrites the constant-ratio hypothesis using the inductive hypothesis, substitutes the already-proved equality r = ϕ, and closes with ring.
why it matters
The declaration supplies the uniqueness half of the gradient-flow fixed-point argument, feeding directly into the exponential-growth statement that total complexity after N steps is at least K_0 ⋅ ϕ^N. It realizes the self-similar fixed-point step (T6) of the forcing chain and confirms that the ϕ-ladder is the only J-cost minimizer compatible with Fibonacci recurrence. No open scaffolding remains in the declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.