span_at_2
plain-language theorem explainer
The theorem asserts that the span function at input 2 equals 3. Researchers modeling working memory capacity from the nonzero elements of F₂³ would cite this identity when verifying one step of the predicted integer collapse under reduced bandwidth. The proof is a one-line computational check that evaluates the explicit formula for the span function.
Claim. Define the function $s(d) = 2^d - 1$ for $d$ a natural number. Then $s(2) = 3$.
background
The module C8 establishes that Miller's 7 ± 2 equals the count of nonzero elements in the three-dimensional vector space over F₂, satisfying 2³ − 1 = 7. The function spanAt is defined by spanAt(d) := 2^d − 1 and therefore supplies the counts for the lower-dimensional cases appearing in the collapse predictions 7 → 5 → 3 → 1 (corresponding to F₂³∖{0} → F₂²∖{0} → F₂∖{0} → {}).
proof idea
The proof is a one-line wrapper that applies the decide tactic to the equality 2^2 − 1 = 3.
why it matters
The result is referenced inside workingMemoryFromCubeCert as the witness for the reduced_to_5 field. It thereby supports the structural claim that working memory limits arise from the cube-counting identity 2³ − 1 = 7. The module situates the identity among the testable predictions for span reduction under limited recognition bandwidth.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.