Information Local Cache Working Memory Approx

The working memory bound

Working memory is the small set of items a mind can hold in focus at once. The classical observation, often called Miller's law, puts that number near seven, plus or minus two. The Recognition Science framework reaches a different, narrower number through a chain of definitions about how a ledger (a discrete record of events) organizes its own access costs.

The framework models memory as a hierarchy of caches. A cache is a small, fast store that holds frequently used items close at hand. The model assigns a cost to every access: a distant item costs more to retrieve than a nearby one. The framework's central cost function, J(x) = (x + 1/x)/2 - 1, measures the price of a ratio between two levels. A theorem in the machine-checked library proves that when this cost is minimized, the optimal hierarchy partitions its levels by the Fibonacci recurrence K(ℓ+2) = K(ℓ+1) + K(ℓ), and that a constant ratio between levels then forces the golden ratio φ = (1+√5)/2.

That result, fibonacci_partition_forces_phi, is the load-bearing step. It derives in the formal system, and the library verifies, that any self-similar cache hierarchy with positive capacities must grow by the golden ratio. The framework then identifies the first level above focal attention as working memory. Its capacity relative to the focal level is φ³, approximately 4.236. The declaration working_memory_approx is a machine-checked theorem stating that this value lies strictly between 4 and 5: 4 < φ³ < 5.

In Recognition Science, this is the formal content of the working memory bound. The theorem does not say that humans can hold exactly 4.236 items. It establishes a mathematical consequence of the framework's cost model: the predicted capacity falls in the interval (4, 5). The empirical claim that human working memory matches this prediction is a separate, unformalized hypothesis. The framework's library proves the arithmetic; it does not prove the psychology.

What the declaration does not claim is just as precise. It does not assert that φ³ is the measured capacity of any biological system. It does not claim that the Fibonacci recurrence is the only way to partition a cache hierarchy; the theorem requires the constant-ratio condition as an explicit premise. And it does not derive the golden ratio from the cost function alone. The derivation needs the Fibonacci recurrence as an input, which the framework justifies from J-cost symmetry but has not yet formalized in the library.

/-- **φ-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 working_memory_approx :
    4 < working_memory_capacity ∧ working_memory_capacity < 5 := by
  unfold working_memory_capacity
  constructor
  · -- φ³ > 4: use φ > 1.61 and 1.61³ > 4
    have hphi : phi > 1.61 := Constants.phi_gt_onePointSixOne
    have hphi_pos : (0:ℝ) ≤ 1.61 := by norm_num
    nlinarith [sq_nonneg phi, sq_nonneg (phi - 1.61), Constants.phi_pos,
               show (1.61:ℝ)^3 > 4 by norm_num]
  · -- φ³ < 5: use φ < 1.62
    have hphi : phi < 1.62 := Constants.phi_lt_onePointSixTwo
    have hphi_pos : (0:ℝ) < phi := Constants.phi_pos
    nlinarith [sq_nonneg (1.62 - phi), sq_nonneg phi,
               show (1.62:ℝ)^3 < 5 by norm_num]

/-- Working memory capacity prediction: φ³ ≈ 4.236.
    The cache hierarchy at ratio φ gives Level 1 (working memory)
    capacity = φ³ relative to Level 0 (focal attention, capacity 1). -/
noncomputable def working_memory_capacity : ℝ := phi ^ 3

What this page does not claim

The theorem does not claim that φ³ is the measured capacity of any biological system. The theorem does not claim that the Fibonacci recurrence is the only way to partition a cache hierarchy. The derivation of the golden ratio from J-cost symmetry is not formalized in the library.

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: