spanAt
plain-language theorem explainer
The definition assigns to each natural number d the value 2^d minus 1, counting the nonzero elements of the d-dimensional vector space over the two-element field. Researchers modeling working memory via the Recognition Science cube would cite it to obtain the sequence 1, 3, 7, 15 that realizes Miller's 7. It is introduced as a direct abbreviation with no lemmas or computation steps.
Claim. Define the reduced span function by $s(d) := 2^d - 1$ for each natural number $d$.
background
The module treats Miller's 7 ± 2 as the count of non-identity elements in F₂³, since 2³ − 1 = 7. Reduced spans are the integer values obtained by restricting to lower-dimensional subcubes, yielding the collapse ladder 7 → 5 → 3 → 1 under reduced recognition bandwidth and a new plateau at 15 under super-normal conditions. The local theoretical setting is the structural claim that working memory span is governed by the geometry of the 3-cube, with the explicit formula supplied by this definition.
proof idea
This is a direct definition that computes the power 2^d and subtracts one, with no lemmas or tactics applied.
why it matters
This definition supplies the counting function used to prove spanAt 3 = 7 and spanAt 4 = 15, which realize the cube-counting identities of the C8 working memory model. It feeds the strict monotonicity theorem span_strict_mono and the certification WorkingMemoryFromCubeCert. The framework landmark is the identification of 7 with |F₂³ ∖ {0}| as the basis for the Miller-law predictions stated in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.