working_memory_approx
plain-language theorem explainer
Researchers modeling cognitive hierarchies cite the result that working memory capacity, defined via the golden ratio, satisfies 4 < capacity < 5. The bound places the first cache level in the phi-ladder between focal attention and longer-term storage. The tactic proof unfolds the definition to phi cubed then applies nlinarith separately to each side using the supplied phi bounds.
Claim. Let $phi$ denote the golden ratio. Define working memory capacity as $phi^3$. Then $4 < phi^3 < 5$.
background
The Local Cache module develops the phi-optimal hierarchy for access costs under the Recognition Composition Law. Working memory capacity is defined as $phi^3$, giving the relative size of Level 1 cache to focal attention (capacity 1) when the hierarchy ratio is forced to phi. Upstream lemmas supply the tight numerical bounds $phi > 1.61$ and $phi < 1.62$ together with positivity of phi.
proof idea
The proof unfolds working_memory_capacity to $phi^3$. It splits the conjunction with constructor, then handles each inequality by nlinarith. The left side invokes phi_gt_onePointSixOne plus norm_num facts on $1.61^3 > 4$; the right side invokes phi_lt_onePointSixTwo plus $1.62^3 < 5$.
why it matters
The theorem feeds the localCacheStatus summary that lists proved cache results. It supplies the concrete numerical anchor for the working-memory prediction in the phi-optimal hierarchy of the Inevitability of Local Minds paper. Within the Recognition framework it confirms the self-similar fixed point phi at the first rung above focal attention.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.