Information Local Cache

The local cache

An information local cache is a small, fast store of frequently used items, kept close to the point of use. A processor keeps a cache of recent memory reads; a mind keeps a cache of familiar faces, words, and routes. The general principle is that fetching an item from a distant, slow store costs more than fetching it from a nearby, fast one. If some items are used much more often than others, it pays to keep those items in the fast store. The cost of a cache is the sum of access frequencies times distances, plus a maintenance overhead for each cached item. A machine-checked library of formal theorems proves that if a frequently accessed distant item exists, and caching it saves more than the maintenance cost, then caching strictly reduces total cost. This is the theorem local_cache_benefit in the framework's library.

The interesting question is how to organize a cache hierarchy when there are several levels, from the smallest and fastest to the largest and slowest. The framework's library proves that the optimal partition of items between levels follows a Fibonacci recurrence: each level's capacity is the sum of the two smaller levels. If the ratio between consecutive levels is constant, that ratio must be the golden ratio φ = (1 + √5)/2 ≈ 1.618. This is the theorem fibonacci_partition_forces_phi. The derivation starts from the J-cost function, which measures the cost of a recognition event, and its symmetry J(x) = J(1/x). Balancing the overshoot cost of putting an item in a level too large against the undershoot cost of putting it in a level too small forces the boundary between levels to lie at the geometric mean of the two capacities, which yields the Fibonacci recurrence.

In Recognition Science, the framework models a mind as a hierarchy of such caches. The smallest level, focal attention, has capacity 1. The next level, working memory, has capacity φ³ ≈ 4.236, which the library proves lies between 4 and 5. This is a prediction about a measurable cognitive quantity, not a theorem about the world. The framework also connects the J-cost to Hebbian learning: the cost of a synapse is J(f_u / f_v), where f_u and f_v are firing rates. The library proves that J(r) = 0 if and only if r = 1, and J(r) > 0 otherwise. So balanced firing rates between two neurons have zero cost, and any imbalance has positive cost. This is the mathematical content of Hebb's rule: correlated firing is cheap, uncorrelated firing is expensive.

The library's results are machine-checked theorems, meaning they are derived from axioms by a computer-verified proof system. The theorems establish that caching reduces cost, that the golden ratio is the only constant ratio for a Fibonacci partition, and that J-cost has the Hebbian sign structure. These are formal results about the abstract cost model. The application to actual minds, with real neurons and real memory limits, is a hypothesis that the model is intended to explain. The framework's contribution is to show that the golden ratio and the Hebbian rule are not arbitrary assumptions but consequences of a single cost function. This is a surprising result: a number famous for its appearance in art and nature also appears as the forced solution to a cache optimization problem.

/-- **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]

/-- The Fibonacci partition recurrence: each level's capacity equals the sum
    of the next two smaller levels. This arises from J-cost-optimal partitioning
    (see paper §4 for the derivation). -/
def fibonacci_recurrence (K : ℕ → ℝ) : Prop :=
  ∀ ℓ : ℕ, K (ℓ + 2) = K (ℓ + 1) + K ℓ

/-- **φ-OPTIMAL HIERARCHY THEOREM (Theorem 4.2, rigorous)**

If a cache hierarchy satisfies:
1. Fibonacci partition: K_{ℓ+2} = K_{ℓ+1} + K_ℓ (optimal partitioning)
2. Constant ratio: K_{ℓ+1}/K_ℓ = r (self-similarity)
3. r > 0, all K_ℓ > 0

Then r = φ = (1+√5)/2. -/
theorem fibonacci_partition_forces_phi (K : ℕ → ℝ) (r : ℝ)
    (hr_pos : 0 < r)
    (hK_pos : ∀ ℓ, 0 < K ℓ)
    (hfib : fibonacci_recurrence K)
    (hratio : constant_ratio K r) :
    r = phi := by
  have hgolden := fibonacci_ratio_forces_golden K r hr_pos hK_pos hfib hratio
  -- r > 0 and r² = r + 1 implies r = φ (by uniqueness of positive root)
  -- Use the fact that φ is the unique positive solution to x² = x + 1
  have h_eq : r ^ 2 - r - 1 = 0 := by linarith
  -- Both r and φ satisfy x² - x - 1 = 0
  have h_phi_eq : phi ^ 2 - phi - 1 = 0 := by
    have := Constants.phi_sq_eq
    linarith
  -- The product of roots = -1 (Vieta's), so the other root is negative.
  -- Since r > 0 and φ > 0, they must be the same root.
  nlinarith [sq_nonneg (r - phi), sq_nonneg (r + phi - 1),
             Constants.phi_pos, sq_nonneg (Real.sqrt 5 - 2),
             Real.sq_sqrt (show (5 : ℝ) ≥ 0 by norm_num)]

/-- **THEOREM (Hebbian Sign Structure)**:

  J(r) = 0 iff r = 1 (balanced firing), and J(r) > 0 for r ≠ 1.
  Therefore the unique J-cost minimum on the neural graph is at
  balanced (correlated) firing rates.

  The Hebbian covariance f_u·f_v - ⟨f_u⟩·⟨f_v⟩ is positive when firing
  is correlated (r ≈ 1, J ≈ 0) and negative when uncorrelated (r ≠ 1, J > 0).
  Thus J-cost descent ↔ Hebbian sign structure. -/
theorem hebbian_sign_structure (r : ℝ) (hr : 0 < r) :
    (Jcost r = 0 ↔ r = 1) ∧ (r ≠ 1 → 0 < Jcost r) := by
  constructor
  · constructor
    · intro h
      -- J(r) = (r-1)²/(2r) = 0 iff r = 1
      have heq := Jcost_eq_sq (ne_of_gt hr)
      rw [heq] at h
      have hden : (2 * r) ≠ 0 := by positivity
      have h0 : (r - 1) ^ 2 = 0 := by
        by_contra hne
        have : 0 < (r - 1) ^ 2 / (2 * r) := div_pos (by positivity) (by positivity)
        linarith
      nlinarith [sq_nonneg (r - 1)]
    · intro h; subst h; exact Jcost_unit0
  · exact Jcost_pos_away_from_one r hr

What this page does not claim

The theorems do not prove that real brains implement this exact cache hierarchy. The working memory capacity of φ³ is a prediction, not a measured fact. The Hebbian sign structure theorem does not specify the dynamics of synaptic weight change.

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: