WorkingMemoryFromCubeCert
plain-language theorem explainer
The structure bundles six properties that certify the cube-derived span equals 7 with integer collapses to 5, 3, 1 and extension to 15, together with the Miller bracket and strict monotonicity. Cognitive modelers or recognition theorists working on capacity limits would cite the certificate. It is a plain record definition that packages the listed equalities and inequalities drawn from the spanAt and canonicalSpan definitions.
Claim. A record asserting $canonicalSpan = 2^3 - 1$, $spanAt(2) = 3$, $spanAt(1) = 1$, $spanAt(4) = 15$, $5 ≤ canonicalSpan ≤ 9$, and $∀ d, spanAt(d) < spanAt(d+1)$, where $canonicalSpan$ denotes the count of nonzero elements in the 3-dimensional vector space over $F_2$ and $spanAt(d)$ denotes the analogous count in dimension $d$.
background
The module states that Miller's 7 ± 2 arises as the count of nonzero vectors in $F_2^3$, written $2^3 - 1 = 7$. canonicalSpan is defined as the constant 7. spanAt is the function sending dimension $d$ to $2^d - 1$. The miller_bracket theorem already establishes the interval 5 to 9 around canonicalSpan. The local setting is the C8 claim that reduced recognition bandwidth produces integer collapses of this count while super-normal bandwidth produces the next plateau at 15.
proof idea
The declaration is a structure definition with no body. It simply declares a record type whose six fields are the required equalities, inequalities, and the universal statement. Construction of an inhabitant occurs downstream by supplying the lemmas canonicalSpan_eq, span_at_2, span_at_1, span_at_4, and miller_bracket.
why it matters
The record supplies the certificate consumed by workingMemoryFromCubeCert. It directly encodes the structural claim in the module doc that 7 equals the nonzero count in the 3-cube and that span reduction follows the ladder $7 → 5 → 3 → 1$ while super-normal conditions reach 15. The construction closes the C8 prediction inside the Recognition framework without introducing new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.