spanAt
plain-language theorem explainer
spanAt d returns the integer 2^d - 1, which counts the nonzero vectors in the d-dimensional vector space over F_2. Cognitive modelers formalizing Miller's 7 ± 2 law from finite-field geometry cite this for the exact ladder 0, 1, 3, 7, 15. The declaration is a direct arithmetic definition with no lemmas or tactics.
Claim. For each natural number $d$, the reduced span at dimension $d$ equals $2^d - 1$.
background
The module treats Miller's working-memory capacity as the count of non-identity elements in the 3-cube $F_2^3$, so that $2^3 - 1 = 7$. The definition spanAt extends this count to arbitrary dimension, producing the integer sequence that governs predicted collapse steps 7 → 5 → 3 → 1 under reduced bandwidth and the super-normal plateau at 15. Module documentation states: 'Structural claim: Miller's 7 ± 2 is not empirical — it is the count of non-identity elements of the 3-cube $F_2^3$.'
proof idea
This is a direct definition that expands the standard exponentiation and subtraction on natural numbers. It is applied verbatim by the decision-procedure theorems span_at_0 through span_at_4 and by the monotonicity argument that unfolds the expression to compare successive powers of two.
why it matters
The definition supplies the concrete sequence that realizes the cube-counting identity central to the working-memory claim. It is used by span_at_3 (value 7 at d=3), span_at_4 (value 15 at d=4), and the strict monotonicity theorem. In the Recognition framework it instantiates the T8 landmark of three spatial dimensions as the source of the canonical seven-item span, with the super-normal extension following from the same formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.