pith. machine review for the scientific record. sign in
def definition def or abbrev high

spanAt

show as:
view Lean formalization →

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.

claimFor 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  29def spanAt (d : ℕ) : ℕ := 2 ^ d - 1

proof body

Definition body.

  30

used by (8)

From the project-wide theorem graph. These declarations reference this one in their body.