phiHierarchy_pairCost
plain-language theorem explainer
The theorem shows that the J-cost of each adjacent pair in the φ-geometric hierarchy equals J(φ). Workers on J-cost gradient flow for cache hierarchies cite it to confirm the per-pair cost is constant along the φ-ladder. The proof is a direct term-mode reduction: unfold the two definitions, then apply congruences and field simplifications to cancel the ratio to φ.
Claim. Let $K_0 > 0$ and define the hierarchy by $K(ℓ) = K_0 φ^ℓ$. Then the pairwise J-cost at level $ℓ$ satisfies $J(K(ℓ+1)/K(ℓ)) = J(φ)$.
background
A hierarchy is a sequence of positive reals $K : ℕ → ℝ$ giving cache-level capacities. The J-cost of one adjacent pair is defined by pairCost $K$ $ℓ$ := Jcost$(K(ℓ+1)/K(ℓ))$. The φ-hierarchy is the explicit geometric sequence phiHierarchy $K_0$ $ℓ$ := $K_0 · φ^ℓ$. The module studies J-cost gradient descent on hierarchies and shows that the unique minimum-cost self-similar solution under the Fibonacci partition constraint is this φ-sequence.
proof idea
The term proof unfolds pairCost and phiHierarchy, yielding the ratio $K_0 φ^{ℓ+1} / (K_0 φ^ℓ)$. It then applies congr 1, field_simp on the nonzero hypothesis $K_0 φ^ℓ ≠ 0$, rewrites the successor power, and finishes with a second field_simp that cancels the remaining positive terms.
why it matters
This declaration verifies that every adjacent pair in the φ-hierarchy carries exactly the cost J(φ), a necessary intermediate fact for the module's claim that the φ-ladder is the unique global minimum under the Fibonacci constraint. It directly supports the Recognition Science forcing chain at T6 (φ as self-similar fixed point) and the Recognition Composition Law. The result closes one step toward the exponential-growth lower bound stated in the module doc-comment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.