span_at_3
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.