span_at_1
plain-language theorem explainer
span_at_1 establishes that the reduced span function evaluates to 1 at dimension 1. Cognitive modelers deriving Miller's 7 ± 2 from the 3-cube would reference this base case in the reduction sequence. The proof proceeds by a direct decision procedure on the defining equation of spanAt.
Claim. Let $spanAt(d) := 2^d - 1$. Then $spanAt(1) = 1$.
background
The CrossDomain module treats working memory as the count of non-identity elements in the vector space F_2^d. For d = 3 this yields 7, matching Miller's 7 ± 2; the module encodes the predicted collapse under reduced bandwidth as the integer ladder 7 → 5 → 3 → 1, corresponding to successive lower-dimensional cubes. The upstream definition spanAt supplies the explicit formula spanAt(d) := 2^d - 1 that generates these counts along the dimension ladder.
proof idea
One-line wrapper that applies the decide tactic to evaluate the defining equation of spanAt at d = 1.
why it matters
The result supplies the reduced_to_3 field inside workingMemoryFromCubeCert, completing the integer reduction sequence required by the module's structural claim. It operationalizes the cube-counting identity 2^d - 1 that the module uses to ground Miller's number in F_2^3. The declaration therefore anchors the cross-domain prediction that span contracts in discrete steps when recognition bandwidth is limited.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.