miller_bracket
plain-language theorem explainer
The theorem proves that the canonical span equals 7 and therefore lies inside the interval from 5 to 9. Recognition theorists and cognitive modelers would cite the result to identify Miller's 7 ± 2 rule with the nonzero vectors of F₂³. The proof is a one-line wrapper that unfolds the definition and applies a decision procedure.
Claim. $5 \leq 7 \leq 9$, where the canonical span is defined to be $2^3 - 1$.
background
The module C8 derives working-memory capacity from the geometry of the three-dimensional vector space over the field with two elements. The upstream definition states that the canonical span equals 7 and equals the count of non-identity elements in F₂³. The module documentation records the structural claim that Miller's 7 ± 2 corridor is this count rather than an empirical accident, together with the predicted collapses 7 → 5 → 3 → 1 under reduced bandwidth and the expansion to 15 under super-normal conditions.
proof idea
The proof is a one-line wrapper that unfolds the definition of canonicalSpan to the constant 7 and then invokes decide to verify both sides of the conjunction.
why it matters
The result supplies the miller_bracket field required by the WorkingMemoryFromCubeCert structure. It thereby completes one verification step inside the C8 wave that equates Miller's corridor with |F₂³ \ {0}|. The parent certificate also records the collapse identities spanAt 2 = 3 and spanAt 1 = 1 together with the super-normal value spanAt 4 = 15.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.