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