span_at_3
The declaration proves that the reduced span at cube dimension 3 equals 7, matching the number of non-zero vectors in F₂³. Cognitive modelers of working memory limits would cite this as the structural source of Miller's 7 ± 2. The proof evaluates the definition of spanAt directly via a decision procedure.
claim$spanAt(3) = 7$, where $spanAt(d) := 2^d - 1$ counts the non-zero elements of the $d$-dimensional vector space over the field with two elements.
background
The module derives working memory capacity from the geometry of the 3-cube over F₂, stating that Miller's 7 ± 2 is the count of non-identity elements: 2³ − 1 = 7. The upstream definition spanAt(d : ℕ) := 2^d − 1 supplies the reduced spans along the cube-dimension ladder. This identity forms part of the cube-counting results that underwrite the module's predictions for integer-step span collapse under reduced recognition bandwidth.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the definition of spanAt at argument 3.
why it matters in Recognition Science
This identity anchors the module's structural claim that Miller's number arises from |F₂³ ∖ {0}|. It supports the listed predictions of span reduction 7 → 5 → 3 → 1 and the super-normal plateau at 15. The result applies the Recognition framework to cognitive limits, consistent with the eight-tick octave and D = 3 in the forcing chain.
scope and limits
- Does not address empirical validity of Miller's rule in human subjects.
- Does not extend the identity to non-integer dimensions.
- Does not prove the collapse predictions listed in the module documentation.
formal statement (Lean)
31theorem span_at_3 : spanAt 3 = 7 := by decide