span_at_4
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not establish empirical validity of the predicted span collapses.
- Does not extend the span function to dimensions other than 4.
- Does not connect to the phi-ladder or Recognition Composition Law.
- Does not address J-cost, defectDist, or the forcing chain T0-T8.
Lean usage
have super_normal : spanAt 4 = 15 := span_at_4formal statement (Lean)
35theorem span_at_4 : spanAt 4 = 15 := by decide
proof body
Term-mode proof.
36
37/-- The span ladder is strictly increasing in d. -/