miller_bracket
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 in Recognition Science
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₂³.
scope and limits
- Does not derive the integer 7 from the forcing chain or phi-ladder.
- Does not prove the empirical validity of the 7 ± 2 law in human data.
- Does not address the predicted super-normal plateau at 15.
- Does not establish the collapse sequence under reduced bandwidth.
formal statement (Lean)
50theorem miller_bracket : 5 ≤ canonicalSpan ∧ canonicalSpan ≤ 9 := by
proof body
One-line wrapper that applies unfold.
51 unfold canonicalSpan; decide
52