workingMemoryFromCubeCert
This definition assembles an instance of the WorkingMemoryFromCubeCert structure by directly assigning pre-proved theorems to each of its six fields. Cognitive modelers seeking a geometric account of Miller's 7±2 capacity limit would cite it as the explicit certificate that 2³-1 equals seven with the predicted integer collapses. The construction is a pure record literal that records the values of canonicalSpan_eq, span_at_2, span_at_1, span_at_4, miller_bracket and span_strict_mono.
claimDefine the certificate $W$ for working memory derived from the 3-cube by the structure whose canonical field asserts $2^3-1=7$, whose reduced-to-5 field asserts spanAt(2)=3, whose reduced-to-3 field asserts spanAt(1)=1, whose super-normal field asserts spanAt(4)=15, whose Miller-bracket field asserts $5≤7≤9$, and whose monotone field asserts that spanAt($d$)<spanAt($d+1$) for every natural number $d$.
background
The module treats Miller's 7±2 as the order of the nonzero vectors in the three-dimensional vector space over F₂. canonicalSpan is therefore defined to be 2³-1. The auxiliary function spanAt($d$) returns 2^d-1, the number of nonzero elements in F₂^d; this yields the reduction ladder 7→5→3→1 when dimension is successively lowered and the super-normal plateau 15 when dimension is raised to four. The module documentation states the structural claim directly: 'Miller's 7 ± 2 is not empirical — it is the count of non-identity elements of the 3-cube F₂³. That is: 2³ − 1 = 7.' Upstream lemmas supply the concrete equalities: canonicalSpan_eq proves the canonical value by decide, span_at_2 and span_at_1 give the reduced spans, span_at_4 gives the super-normal value, miller_bracket confirms the 5-to-9 corridor, and span_strict_mono establishes strict increase via Nat.one_le_two_pow and omega.
proof idea
The declaration is a structure literal that populates WorkingMemoryFromCubeCert by naming the six upstream theorems already established in the same module. canonical receives canonicalSpan_eq, reduced_to_5 receives span_at_2, reduced_to_3 receives span_at_1, super_normal receives span_at_4, miller_bracket receives miller_bracket, and monotone receives span_strict_mono. No further tactics or reductions occur; the definition simply records the existing proofs.
why it matters in Recognition Science
The declaration supplies the terminal certificate that realizes the C8 structural claim inside the Recognition Science cross-domain layer, converting the geometric count |F₂³∖{0}|=7 into an explicit, machine-checked object. It thereby closes the cube-counting identities required by the module and supplies the concrete data for the predicted span reductions and the Miller corridor. The parent context is the module's proof of the 2³-1 identity together with its dimension-ladder properties; no downstream uses are recorded yet. The construction instantiates the framework's D=3 landmark as the binary cube whose nonzero count yields the working-memory number.
scope and limits
- Does not supply empirical measurements of human working-memory capacity.
- Does not derive spanAt from the J-cost functional or the Recognition Composition Law.
- Does not treat cubes of dimension other than 1, 2, 3 or 4.
- Does not connect the span values to the phi-ladder or mass formulas.
- Does not claim that the 7±2 corridor is the only possible bracket under reduced bandwidth.
formal statement (Lean)
61def workingMemoryFromCubeCert : WorkingMemoryFromCubeCert where
62 canonical := canonicalSpan_eq
proof body
Definition body.
63 reduced_to_5 := span_at_2
64 reduced_to_3 := span_at_1
65 super_normal := span_at_4
66 miller_bracket := miller_bracket
67 monotone := span_strict_mono
68
69end IndisputableMonolith.CrossDomain.WorkingMemoryFromCube