def
definition
working_memory_capacity
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Information.LocalCache on GitHub at line 245.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
242/-- Working memory capacity prediction: φ³ ≈ 4.236.
243 The cache hierarchy at ratio φ gives Level 1 (working memory)
244 capacity = φ³ relative to Level 0 (focal attention, capacity 1). -/
245noncomputable def working_memory_capacity : ℝ := phi ^ 3
246
247theorem working_memory_approx :
248 4 < working_memory_capacity ∧ working_memory_capacity < 5 := by
249 unfold working_memory_capacity
250 constructor
251 · -- φ³ > 4: use φ > 1.61 and 1.61³ > 4
252 have hphi : phi > 1.61 := Constants.phi_gt_onePointSixOne
253 have hphi_pos : (0:ℝ) ≤ 1.61 := by norm_num
254 nlinarith [sq_nonneg phi, sq_nonneg (phi - 1.61), Constants.phi_pos,
255 show (1.61:ℝ)^3 > 4 by norm_num]
256 · -- φ³ < 5: use φ < 1.62
257 have hphi : phi < 1.62 := Constants.phi_lt_onePointSixTwo
258 have hphi_pos : (0:ℝ) < phi := Constants.phi_pos
259 nlinarith [sq_nonneg (1.62 - phi), sq_nonneg phi,
260 show (1.62:ℝ)^3 < 5 by norm_num]
261
262/-! ## Status -/
263
264def localCacheStatus : String :=
265 "═══════════════════════════════════════════════════\n" ++
266 " LOCAL CACHE THEOREM — LEAN STATUS\n" ++
267 "═══════════════════════════════════════════════════\n" ++
268 "✓ local_cache_benefit: Caching reduces cost (proved)\n" ++
269 "✓ fibonacci_ratio_forces_golden: Fib + ratio → r²=r+1 (proved)\n" ++
270 "✓ fibonacci_partition_forces_phi: Fib + ratio → r=φ (proved)\n" ++
271 "✓ hebb_is_Jcost_gradient: J'(r) = (1-r⁻²)/2 (proved)\n" ++
272 "✓ hebbian_matches_descent: J' > 0 for r > 1 (proved)\n" ++
273 "✓ Jcost_min_at_one: J(1) = 0 (proved)\n" ++
274 "✓ Jcost_pos_of_ne_one: J(r) > 0 for r ≠ 1 (proved)\n" ++
275 "✓ working_memory_approx: 4 < φ³ < 5 (proved)\n" ++