caching_is_forced
plain-language theorem explainer
The theorem proves that any frequency-weighted allocation with at least one remote node has strictly higher total J-cost than the fully collocated case where all distances are zero. Researchers modeling brain holography or graph caching under J-cost minimization would cite this to establish forced locality. The proof isolates a remote index and invokes sum_lt_sum with nonnegativity of J-cost on the zero-distance terms together with the strict inequality from collocation minimization at the remote site.
Claim. Let $J$ denote the J-cost function and $φ$ the golden ratio. Given positive real frequencies $f_i > 0$ for $i = 1, …, n$ and nonnegative integer distances $d_i$ with some $d_k > 0$, the inequality $∑_i f_i J(φ^0) < ∑_i f_i J(φ^{d_i})$ holds.
background
The J-cost function is $J(x) = (x + x^{-1})/2 - 1$, nonnegative for $x > 0$ by the AM-GM inequality as established in Jcost_nonneg. The module LocalCacheForcing proves that J-cost minimization on connected graphs forces hierarchical local caching, closing Gap G1 in the brain holography proof. Upstream results include Jcost_nonneg from Cost and Gravity modules, which confirm nonnegativity via algebraic identities or AM-GM, and PrimitiveDistinction.from which derives structural conditions from axioms.
proof idea
The proof obtains a remote index j from the existence hypothesis. It applies Finset.sum_lt_sum. The non-strict inequality for every term follows from multiplying the nonnegative J-cost at zero distance (via access_cost_zero_at_origin and Jcost_nonneg) by positive frequencies. The strict inequality is witnessed at j by multiplying the positive frequency by the strict cost increase given by collocation_minimizes_cost.
why it matters
This result establishes that remote allocations are strictly suboptimal under J-cost, feeding into the local_cache_forcing_certificate and supporting the claim that J-cost minimization forces local caching in the GCIC framework. It closes Gap G1 in the brain holography proof by showing collocation is preferred. The argument relies on the strict increase of Jcost along phi-powers from Jcost_phi_pow_strictMono.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.