span_at_2
span_at_2 establishes that the reduced span at cube dimension 2 equals 3. Researchers modeling Miller's 7 ± 2 as the punctured 3-cube count would cite this identity when verifying the collapse sequence 7 → 5 → 3 → 1. The proof is a direct arithmetic evaluation via the decide tactic on the definition of spanAt.
claimThe reduced span function satisfies $2^2 - 1 = 3$.
background
The module develops the structural claim that Miller's 7 ± 2 equals the count of non-identity elements in F₂³, written 2³ − 1 = 7. Reduced spans along the cube-dimension ladder are given by the upstream definition spanAt d := 2^d − 1, which supplies the integer sizes of the punctured d-cubes F₂^d ∖ {0}.
proof idea
One-line wrapper that applies the decide tactic to evaluate the arithmetic expression 2^2 − 1 directly.
why it matters in Recognition Science
The identity supplies the reduced_to_3 field inside workingMemoryFromCubeCert, which assembles the full certificate for the cube model of working memory. It realizes one explicit step in the module's predicted collapse sequence under reduced bandwidth. In the Recognition framework this counting supports the eight-tick octave and the emergence of D = 3 spatial dimensions from the phi-ladder.
scope and limits
- Does not establish empirical validity of the 7 ± 2 rule.
- Does not address super-normal plateaus at 15.
- Does not derive the F₂ vector space from the forcing chain T0–T8.
- Does not supply error bounds or probabilistic extensions.
formal statement (Lean)
32theorem span_at_2 : spanAt 2 = 3 := by decide