phiHierarchy_pos
plain-language theorem explainer
The φ-hierarchy K(ℓ) = K₀ φ^ℓ stays strictly positive for every natural number level ℓ whenever the base capacity K₀ is positive. Researchers deriving cumulative complexity bounds under J-cost gradient flow on cache hierarchies cite this to keep all summands positive. The proof is a one-line wrapper that unfolds the definition and applies the lemmas mul_pos and pow_pos.
Claim. If $K_0 > 0$ and $ℓ ∈ ℕ$, then $K_0 φ^ℓ > 0$, where the φ-hierarchy is the geometric sequence $K(ℓ) = K_0 φ^ℓ$.
background
The module studies J-cost gradient flow on hierarchies, where a hierarchy is a sequence of positive reals K : ℕ → ℝ giving cache-level capacities and the total J-cost is the sum of pairwise ratio costs ∑ J(K(ℓ+1)/K(ℓ)). Under the Fibonacci partition constraint the minimum-cost self-similar solution is the unique φ-geometric sequence. The upstream definition phiHierarchy supplies the explicit form K(ℓ) = K₀ · φ^ℓ.
proof idea
The proof is a one-line wrapper. It unfolds phiHierarchy to the product K₀ * φ^ℓ and applies mul_pos to the hypothesis 0 < K₀ together with pow_pos applied to phi_pos at exponent ℓ.
why it matters
This result is invoked directly by cumulative_growth_lower_bound to establish that the sum of the first N+1 terms is at least K₀ φ^N. It thereby supports the module's key claim that after N optimization cycles on the φ-ladder the total complexity is at least K₀ · φ^N, closing the loop from the Fibonacci recurrence to the self-similar fixed point φ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.