canonicalSpan
CanonicalSpan sets the natural number 7 equal to the count of nonzero vectors in the three-dimensional vector space over F₂. Cognitive modelers deriving working-memory limits from geometry would cite this constant when linking Miller's 7 ± 2 range to the structure of F₂³. The declaration is a direct constant assignment with no computation or lemmas.
claimDefine the canonical span to be the natural number 7, satisfying the identity $7 = 2^3 - 1$.
background
The module treats working memory span as the cardinality of nonzero elements in the 3-cube over the field with two elements. Canonical span therefore equals |F₂³ ∖ {0}|, which is exactly 2³ − 1. This supplies the central integer in the Miller 7 ± 2 corridor under the Recognition Science claim C8.
proof idea
This declaration is a direct definition that assigns the constant 7. No lemmas, tactics, or reduction steps are present.
why it matters in Recognition Science
The definition anchors the cube-derived working-memory model and is referenced by canonicalSpan_eq, miller_bracket, super_normal_jump, and WorkingMemoryFromCubeCert. It realizes the eight-tick octave at spatial dimension 3 (T7, T8) by fixing the normal plateau at 7 before the super-normal extension to 15 = 2⁴ − 1. The value closes the structural claim that Miller's number is geometrically forced rather than empirical.
scope and limits
- Does not prove the empirical validity of the 7 ± 2 rule.
- Does not derive the collapse sequence 7 → 5 → 3 → 1 from dynamics.
- Does not address extensions beyond the stated super-normal plateau at 15.
- Does not connect to the J-function or the forcing chain T0–T8.
Lean usage
theorem miller_bracket : 5 ≤ canonicalSpan ∧ canonicalSpan ≤ 9 := by unfold canonicalSpan; decideformal statement (Lean)
25def canonicalSpan : ℕ := 7