local_cache_benefit
plain-language theorem explainer
The local cache benefit theorem shows that under positive frequency f, distance spread d > ε > 0, and maintenance cost α strictly below f(d - ε), the net access cost reduction f d - (f ε + α) is strictly positive. Information theorists modeling hierarchical memory in Recognition Science cite it to justify local caching as a cost-minimizing necessity. The proof is a short tactic sequence that rewrites the difference via ring and concludes via linear arithmetic on the given bound.
Claim. Let $f, d, ε, α ∈ ℝ$ satisfy $0 < ε < d$, $0 < α < f(d - ε)$, and $0 < f$. Then $f d - (f ε + α) > 0$.
background
The Local Cache Theorem and φ-Optimal Hierarchy module formalizes cost savings from caching under non-uniform access. Total access cost for a distant item v* is given by freq_star · dist_star; after caching it drops to freq_star · ε + α, where ε is the reduced effective distance and α the maintenance overhead. Upstream results supply the underlying cost functions: ObserverForcing.cost defines the cost of a recognition event as its J-cost, while MultiplicativeRecognizerL4.cost derives cost from the comparator on positive ratios.
proof idea
The proof applies the ring tactic to obtain freq_star · dist_star - freq_star · ε = freq_star · (dist_star - ε). It then invokes linarith on the hypothesis α < freq_star · (dist_star - ε) to conclude the target strict inequality.
why it matters
This is the core statement of Theorem 3.1 in the Local Cache section and feeds directly into the localCacheStatus definition, which reports the theorem as proved and derives working memory capacity as phi^3. The result supports the inevitability of local minds by showing J-cost reduction forces hierarchical caching, consistent with the Recognition Composition Law and the phi-ladder structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.