canonicalSpan_eq
plain-language theorem explainer
The identity shows that the canonical span equals seven, the count of nonzero vectors in the three-dimensional vector space over F₂. Researchers modeling working memory capacity through finite geometry or algebraic reductions of Miller's 7 ± 2 would cite this result. The proof is a one-line decision procedure confirming the arithmetic equality 2³ − 1 = 7.
Claim. The canonical span satisfies $7 = 2^3 - 1$.
background
In the CrossDomain module, the canonical span is defined as the integer seven, representing |F₂³ ∖ {0}|. The module doc states the structural claim that Miller's 7 ± 2 is not empirical but equals 2³ − 1, with predictions of integer collapse under reduced bandwidth (7 → 5 → 3 → 1) and a super-normal plateau at 15. The upstream definition supplies canonicalSpan : ℕ := 7 as the base value.
proof idea
The proof is a one-line wrapper that invokes the decide tactic to verify the numerical equality between the defined canonical span and the expression 2^3 - 1.
why it matters
This theorem supplies the canonical value to the WorkingMemoryFromCubeCert certificate, which aggregates the span reductions, the super-normal case, and the Miller bracket. It directly implements the C8 claim that 2³ − 1 = 7 as the algebraic origin of working memory capacity, anchoring the eight-tick octave and D = 3 to cognitive span limits. The module notes that the empirical predictions remain testable on span-reduction protocols.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.