143theorem phi_hierarchy_is_unique_fixed_point (K : ℕ → ℝ) (r : ℝ) 144 (hr_pos : 0 < r) 145 (hK_pos : ∀ ℓ, 0 < K ℓ) 146 (hfib : fibonacci_recurrence K) 147 (hratio : constant_ratio K r) : 148 r = phi ∧ ∀ n, K n = K 0 * phi ^ n := by
proof body
Term-mode proof.
149 constructor 150 · exact fibonacci_partition_forces_phi K r hr_pos hK_pos hfib hratio 151 · intro n 152 induction n with 153 | zero => simp 154 | succ m ih => 155 have := hratio m 156 rw [ih] at this 157 have hphi_eq := fibonacci_partition_forces_phi K r hr_pos hK_pos hfib hratio 158 rw [hphi_eq] at this 159 rw [this] 160 ring 161 162/-! ## §4 The exponential growth theorem -/ 163 164/-- **φ-HIERARCHY EXPONENTIAL GROWTH** 165 166 After N levels of a φ-optimal cache hierarchy starting from K₀ > 0, 167 the total complexity at level N is exactly K₀ · φ^N. 168 169 Since φ > 1, this is exponential in N. 170 Since gradient flow converges to this hierarchy (Theorem above), 171 any J-cost-minimizing system necessarily builds exponentially 172 growing complexity over time. -/
depends on (24)
Lean names referenced from this declaration's body.