miller_bracket
plain-language theorem explainer
The theorem establishes that the canonical span equals 7 and therefore lies inside the interval from 5 to 9. Cognitive scientists modeling working-memory capacity as the nonzero vectors in F₂³ would cite the result to replace the empirical 7 ± 2 rule with an exact cube-count identity. The proof is a one-line wrapper that unfolds the definition of canonicalSpan and decides the inequality.
Claim. $5 ≤ 7 ≤ 9$, where the canonical span is the integer $2^3 - 1$.
background
The module derives working-memory capacity from the geometry of the three-dimensional vector space over the field with two elements. The canonical span is introduced as the count of non-identity elements, written $2^3 - 1 = 7$. This supplies the structural origin of Miller’s observed range rather than an empirical fit.
proof idea
One-line wrapper that unfolds canonicalSpan to the literal value 7 and then decides the bounds 5 ≤ 7 ≤ 9.
why it matters
The result populates the miller_bracket field of the WorkingMemoryFromCubeCert structure, which also records the canonical equality and the integer collapses to 5, 3 and the super-normal extension to 15. It therefore completes the module’s claim that Miller’s corridor is exactly the count of nonzero vectors in F₂³.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.