WorkingMemoryFromCubeCert
The structure bundles the geometric identities that realize Miller's 7±2 as the count of nonzero vectors in F₂³. Cognitive and information theorists cite the record when modeling working-memory capacity as a direct consequence of three-dimensional binary geometry. It is assembled as a plain record of the fixed canonical value, the integer-step reductions, the super-normal extension, the bracket, and monotonicity.
claimLet $S$ be the structure whose fields assert that the canonical span equals $7$, that spanAt$(2)=3$, spanAt$(1)=1$, spanAt$(4)=15$, that $5≤7≤9$, and that $d↦$spanAt$(d)$ is strictly increasing.
background
The module treats working memory capacity as the number of nonzero elements in the vector space F₂³, written $2^3-1=7$. canonicalSpan is the constant definition equal to 7. spanAt is the function $d↦2^d-1$ that counts nonzero vectors in $d$ dimensions. miller_bracket is the theorem that places the canonical value inside the interval [5,9].
proof idea
The declaration is a structure definition whose fields are populated directly from the definitions of canonicalSpan and spanAt, the miller_bracket theorem, and the monotonicity of the map $d↦2^d-1$. No separate tactic script is required; the record simply packages the already-proved identities.
why it matters in Recognition Science
The structure supplies the certificate instantiated by workingMemoryFromCubeCert, which in turn witnesses the C8 claim that Miller's law follows from the cube geometry. It thereby connects the eight-tick octave and the emergence of three spatial dimensions to a concrete cognitive count. The construction closes the structural half of the wave; empirical span-reduction tests remain open.
scope and limits
- Does not derive the Miller interval bounds from the recognition composition law.
- Does not supply numerical predictions for non-integer bandwidth reductions.
- Does not address stability under perturbations of the underlying field.
- Does not incorporate the J-cost function or the phi-ladder mass formula.
formal statement (Lean)
53structure WorkingMemoryFromCubeCert where
54 canonical : canonicalSpan = 2 ^ 3 - 1
55 reduced_to_5 : spanAt 2 = 3 -- collapse one dimension
56 reduced_to_3 : spanAt 1 = 1 -- collapse two
57 super_normal : spanAt 4 = 15 -- add one dimension
58 miller_bracket : 5 ≤ canonicalSpan ∧ canonicalSpan ≤ 9
59 monotone : ∀ d, spanAt d < spanAt (d + 1)
60