span_at_4
plain-language theorem explainer
span_at_4 establishes that the span function at dimension 4 equals 15, the count of nonzero vectors in four-dimensional space over F_2. Cognitive modelers working on working-memory limits in Recognition Science cite it for the super-normal plateau. The proof is a direct decision on the defining equation of spanAt.
Claim. The reduced span function along the cube-dimension ladder satisfies $spanAt(4) = 15$.
background
In the module on Working Memory from the Cube, spanAt is defined by spanAt d := 2^d - 1 and counts the nonzero elements of the d-dimensional vector space over F_2. The module formalizes Miller's 7 as 2^3 - 1 and predicts integer collapses under reduced bandwidth together with a super-normal extension to 15 at d = 4. The theorem depends only on this definition and the decide procedure.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the equality obtained directly from the definition spanAt d = 2^d - 1.
why it matters
This result supplies the super_normal field inside workingMemoryFromCubeCert, completing the certificate for the cube-based model. It realizes the module prediction of a new plateau at 15 = F_2^4 minus the zero vector under super-normal conditions, extending the structural identity 2^3 - 1 = 7.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.