phiHierarchy_value
plain-language theorem explainer
The declaration shows that the φ-hierarchy function at level N evaluates exactly to the initial capacity K₀ multiplied by the golden ratio φ raised to N. Researchers deriving exponential bounds on total complexity in J-cost optimized cache hierarchies cite this identity directly. The proof is a one-line term that applies reflexivity to the definition of the hierarchy.
Claim. For initial capacity $K_0$ and level $N$, the φ-hierarchy satisfies $K_0$·φ-hierarchy$(K_0,N)=K_0·φ^N$.
background
The module establishes that a hierarchy is a sequence of positive reals representing cache-level capacities whose 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. Upstream results include the definition of K as φ^{1/2} and the cost function induced by a multiplicative recognizer.
proof idea
The proof is a one-line wrapper that applies reflexivity to the definition of phiHierarchy.
why it matters
This identity is invoked by cumulative_growth_lower_bound to bound total complexity from below by K₀·φ^N and by phi_hierarchy_exponential_growth to establish exact exponential growth after N levels. It supplies the concrete evaluation step in the argument that J-cost gradient descent on hierarchies converges to the φ-partition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.