memorySystemCount
The memorySystemCount theorem fixes the cardinality of the MemorySystem type at five. Researchers enumerating the 125-element cognitive state space as a product of three recognition axes would cite this result to obtain the memory factor. The proof is a one-line decision procedure that verifies the Fintype instance derived from the five constructors.
claim$ |M| = 5 $, where $M$ is the inductive type whose elements are the five memory categories working, episodic, semantic, procedural, and priming.
background
The Cognitive State Space module decomposes the conscious moment into three orthogonal axes, each of cardinality five: Sense, Emotion, and MemorySystem. Their product yields the 125-element CognitiveState type. MemorySystem is introduced as an inductive type with exactly those five constructors and derives DecidableEq, Repr, BEq, and Fintype instances.
proof idea
The proof is a one-line wrapper that applies the decide tactic directly to the Fintype.card expression for MemorySystem.
why it matters in Recognition Science
This cardinality supplies the memory factor to the cognitiveStateCount theorem, which computes |CognitiveState| = 125 via the product formula. It is also invoked by the three non-collapse theorems that establish the product strictly exceeds any single factor or pairwise product. The result therefore instantiates the 5³ structure asserted in the module documentation for the conscious state space.
scope and limits
- Does not prove the five memory categories are empirically independent in neural recordings.
- Does not derive the specific choice of five elements from the Recognition forcing chain or RCL.
- Does not address dynamical transitions or superpositions among the three axes.
Lean usage
theorem cognitiveStateCount : Fintype.card CognitiveState = 125 := by simp only [CognitiveState, Fintype.card_prod, senseCount, emotionCount, memorySystemCount]formal statement (Lean)
41theorem memorySystemCount : Fintype.card MemorySystem = 5 := by decide
proof body
42