Information Local Cache Local Cache Benefit

The cache theorem

A cache is a small, fast store that holds copies of items you expect to need again, so you can reach them without traveling to the slow, distant original. The theorem named local_cache_benefit states the exact condition under which storing such a copy is guaranteed to pay for itself. It compares two costs. Without a cache, every access to an item costs its frequency times its distance. With a cache, a cached item is reached at a tiny distance ε, while uncached items still cost full distance, and each cached item adds a maintenance overhead α.

The theorem proves that caching strictly reduces total cost when one frequently accessed distant item v* exists and three conditions hold: its frequency times its distance dominates the cost, its distance exceeds the near-cache distance ε, and the maintenance overhead α is positive but smaller than the saving freq(v*)·(dist(v*) − ε). The conclusion is the inequality freq_star · dist_star − (freq_star · ε + α) > 0, which says the saving beats the overhead. The proof is a short algebraic argument, checked in the machine-verified library of formal theorems.

What the theorem does not claim is just as important. It does not say that caching every item is beneficial, nor that the optimal cache size is derivable from this inequality alone. It assumes the three conditions hold; if the overhead is too large or the item is not accessed often enough, the inequality fails and caching can lose. The theorem also says nothing about which item to cache, only that if a dominant distant item exists, caching it helps. It is a local, conditional statement about one item, not a global policy for an entire memory hierarchy.

The broader framework uses this result as a building block. A companion theorem in the same file shows that when cache levels follow a Fibonacci partition with a constant ratio, that ratio must be the golden ratio φ. The local cache theorem supplies the cost-side justification: caching a dominant item reduces cost, which makes the hierarchical structure worth building. The framework's claim is that the golden ratio appears in optimal cache hierarchies because the cost structure forces it, and this theorem is the first step in that argument.

/-- **LOCAL CACHE THEOREM (Theorem 3.1)**

If there exists a frequently-accessed distant item v* such that
caching it saves more than the maintenance cost, then caching
strictly reduces total cost.

Conditions:
  (A1) Non-uniformity: freq(v*) · dist(v*) is the dominant cost term
  (A2) Distance spread: dist(v*) > ε
  (A3) Positive maintenance: 0 < α < freq(v*) · (dist(v*) - ε) -/
theorem local_cache_benefit
    (freq_star dist_star ε α : ℝ)
    (_hε_pos : 0 < ε)
    (_hdist : ε < dist_star)
    (_hα_pos : 0 < α)
    (hα_lt : α < freq_star * (dist_star - ε))
    (_hfreq_pos : 0 < freq_star) :
    -- The cost reduction from caching v* is strictly positive
    freq_star * dist_star - (freq_star * ε + α) > 0 := by
  have h1 : freq_star * dist_star - freq_star * ε = freq_star * (dist_star - ε) := by ring
  linarith [hα_lt]

/-- **LOCAL CACHE THEOREM (Theorem 3.1)**

If there exists a frequently-accessed distant item v* such that
caching it saves more than the maintenance cost, then caching
strictly reduces total cost.

Conditions:
  (A1) Non-uniformity: freq(v*) · dist(v*) is the dominant cost term
  (A2) Distance spread: dist(v*) > ε
  (A3) Positive maintenance: 0 < α < freq(v*) · (dist(v*) - ε) -/
theorem local_cache_benefit
    (freq_star dist_star ε α : ℝ)
    (_hε_pos : 0 < ε)
    (_hdist : ε < dist_star)
    (_hα_pos : 0 < α)
    (hα_lt : α < freq_star * (dist_star - ε))
    (_hfreq_pos : 0 < freq_star) :
    -- The cost reduction from caching v* is strictly positive
    freq_star * dist_star - (freq_star * ε + α) > 0 := by
  have h1 : freq_star * dist_star - freq_star * ε = freq_star * (dist_star - ε) := by ring
  linarith [hα_lt]

/-- **LOCAL CACHE THEOREM (Theorem 3.1)**

If there exists a frequently-accessed distant item v* such that
caching it saves more than the maintenance cost, then caching
strictly reduces total cost.

Conditions:
  (A1) Non-uniformity: freq(v*) · dist(v*) is the dominant cost term
  (A2) Distance spread: dist(v*) > ε
  (A3) Positive maintenance: 0 < α < freq(v*) · (dist(v*) - ε) -/
theorem local_cache_benefit
    (freq_star dist_star ε α : ℝ)
    (_hε_pos : 0 < ε)
    (_hdist : ε < dist_star)
    (_hα_pos : 0 < α)
    (hα_lt : α < freq_star * (dist_star - ε))
    (_hfreq_pos : 0 < freq_star) :
    -- The cost reduction from caching v* is strictly positive
    freq_star * dist_star - (freq_star * ε + α) > 0 := by
  have h1 : freq_star * dist_star - freq_star * ε = freq_star * (dist_star - ε) := by ring
  linarith [hα_lt]

What this page does not claim

Caching every item is beneficial regardless of the conditions. The theorem identifies which item to cache or how large the cache should be. The theorem applies to a global memory hierarchy without additional assumptions.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Information/LocalCache.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: