localCacheStatus
plain-language theorem explainer
This definition produces a constant string that reports the proof status of theorems establishing the φ-optimal cache hierarchy and working memory bounds. Modelers of recognition-based cognition cite it to confirm the verified core results on J-cost reduction via caching. The definition is a direct string literal concatenation with no computation or lemmas applied.
Claim. The constant string enumerating proved statements: caching reduces total access cost under (A1–A3); the Fibonacci partition recurrence $K_{ℓ+1}=K_ℓ+K_{ℓ-1}$ with constant ratio forces the golden ratio φ; $J(r)>0$ for $r≠1$ and $r>0$; and working memory capacity satisfies $4<φ^3<5$.
background
Jcost is the recognition cost function with algebraic form $J(x)=(x-1)^2/(2x)$ for $x≠0$, shown positive for $x>0$ and $x≠1$ by the upstream lemmas Jcost_eq_sq and Jcost_pos_of_ne_one. The module documents the local cache theorem as the machine-verified core of the Inevitability of Local Minds paper, listing main results on caching benefit, Fibonacci forcing of φ, and Hebbian covariance matching the J-cost gradient. The local theoretical setting centers on φ-optimal hierarchies where Level 1 capacity equals φ³ relative to focal attention capacity 1.
proof idea
The definition constructs the status string by direct concatenation of literal text blocks, each reporting a theorem's proof status. No lemmas are applied inside the definition itself; upstream results such as Jcost_eq_sq appear only in the enumerated list. It is a pure constant definition with no tactics or reductions.
why it matters
This declaration summarizes the key theorems that establish the φ-optimal hierarchy, directly supporting the main results in the module documentation for the Inevitability of Local Minds paper. It reports on results that rely on J-uniqueness (T5) and the self-similar fixed point φ (T6) from the forcing chain. It touches the translation of these bounds to empirical working memory measurements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.