span_at_2
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.