memorySystemCount
plain-language theorem explainer
The declaration fixes the memory factor of the cognitive state space at cardinality five. Researchers enumerating the 125-element conscious state space as a product of three recognition axes cite this result to anchor the total count. The proof is a direct decidable computation over the five-constructor inductive definition.
Claim. The finite type MemorySystem has cardinality five: $Fintype.card(MemorySystem) = 5$, where MemorySystem is the inductive type with constructors working, episodic, semantic, procedural, and priming.
background
The Cognitive State Space module models the conscious moment as the product Sense × Emotion × MemorySystem, each axis of cardinality 5, for a total of 125 states. MemorySystem is introduced as an inductive type with exactly those five constructors and derives the Fintype instance needed for cardinality arithmetic. The module states that if the three-fold decomposition holds then the state space possesses this enumerated structure; empirical independence of the axes is left as a testable hypothesis outside the formal content.
proof idea
The proof is a one-line wrapper that applies the decide tactic to compute the cardinality directly from the inductive enumeration and its derived Fintype instance.
why it matters
The result is invoked by cognitiveStateCount to obtain the product cardinality 125 and by the three non-collapse theorems that establish the full space strictly exceeds any factor or pair. It supplies the memory-axis enumeration step in the cross-domain structural claim. The module leaves open whether the five-element choice and axis independence hold in neural data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.