canonicalSpan_eq
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not address the empirical accuracy of Miller's law in psychological experiments.
- Does not derive the value from the Recognition Composition Law or J-function.
- Does not extend the count to higher-dimensional cubes beyond F₂⁴.
- Does not provide a proof of the super-normal plateau at fifteen.
Lean usage
theorem span_is_seven : canonicalSpan = 7 := canonicalSpan_eqformal statement (Lean)
26theorem canonicalSpan_eq : canonicalSpan = 2 ^ 3 - 1 := by decide
proof body
Term-mode proof.
27
28/-- Reduced spans along the cube-dimension ladder. -/