spanAt
plain-language theorem explainer
spanAt d equals the count of non-zero vectors in the d-dimensional vector space over F2. Researchers modeling Miller's 7 plus or minus 2 as a geometric identity in Recognition Science cite this when deriving capacity limits from the 3-cube. The declaration is introduced as a direct one-line definition with no additional lemmas.
Claim. The reduced span at dimension $d$ is given by $2^d - 1$.
background
The module CrossDomain.WorkingMemoryFromCube frames working memory capacity via the 3-cube over F2, where the structural claim is that Miller's 7 equals the number of non-identity elements: 2^3 minus 1. The doc-comment states: 'Structural claim: Miller's 7 ± 2 is not empirical — it is the count of non-identity elements of the 3-cube F₂³. That is: 2³ − 1 = 7.' Reduced spans are the integer sequence obtained by lowering dimension along this ladder, with predicted collapses 7 to 5 to 3 to 1 under bandwidth limits and a super-normal plateau at 15.
proof idea
This is a one-line definition that directly equates spanAt d to 2^d minus 1.
why it matters
The definition supplies the counting function used by all downstream span_at theorems and by WorkingMemoryFromCubeCert. It realizes the C8 claim that 7 equals |F2^3 minus zero|, connecting the cube model to the forcing chain step T8 that fixes D equals 3 and to the eight-tick octave. The module states that the empirical predictions are testable on span-reduction protocols.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.