workingMemoryFromCubeCert
plain-language theorem explainer
The declaration constructs a single certificate structure that collects the F₂³ counting identities for working memory capacity. Cognitive modelers deriving Miller's 7±2 from finite-field geometry would cite the packaged result when testing span-reduction predictions. The definition is a direct field-by-field assignment that pulls in the pre-proved equalities and inequalities without further reasoning.
Claim. Let $W$ be the certificate asserting that the canonical span equals $2^3-1$, the span function evaluated at 2 equals 3, at 1 equals 1, at 4 equals 15, the canonical span lies in the interval $[5,9]$, and the span function is strictly increasing.
background
Module C8 derives working memory capacity from the count of nonzero vectors in F₂³, giving exactly seven elements. The structure WorkingMemoryFromCubeCert packages the required identities: canonical span equals $2^3-1$, reduced spans under dimension collapse, super-normal extension to 15, the Miller bracket, and strict monotonicity of the span function.
proof idea
The definition populates the certificate by direct assignment of each field to an upstream theorem: canonical to canonicalSpan_eq, reduced_to_5 to span_at_2, reduced_to_3 to span_at_1, super_normal to span_at_4, miller_bracket to miller_bracket, and monotone to span_strict_mono.
why it matters
The definition supplies the single object that realizes the C8 structural claim linking Miller's 7±2 to |F₂³ {0}|. It completes the local module by bundling the cube-counting results that support the predicted collapse sequence 7→5→3→1 and the super-normal plateau at 15. The construction aligns with the Recognition Science assignment of D=3 spatial dimensions but does not invoke the forcing chain or Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.