notCollapsedToMemory
plain-language theorem explainer
The theorem shows the cognitive state space has strictly more elements than the memory subsystem. Researchers constructing recognition models from orthogonal axes cite it to enforce non-collapse of the product. The proof is a one-line rewrite that substitutes the product cardinality and memory count theorems, then decides the numerical comparison.
Claim. The cardinality of the product space $Sense × Emotion × MemorySystem$ is strictly greater than the cardinality of $MemorySystem$.
background
CognitiveState is the product type Sense × Emotion × MemorySystem. MemorySystem is the five-element inductive type whose constructors are working, episodic, semantic, procedural and priming, each equipped with DecidableEq and Fintype instances. The module proves |CognitiveState| = 125 under the three-axis decomposition and separately records |MemorySystem| = 5. Upstream theorems cognitiveStateCount and memorySystemCount supply these exact cardinalities.
proof idea
One-line wrapper that rewrites the goal with cognitiveStateCount and memorySystemCount, then invokes decide on the resulting numerical inequality.
why it matters
The result is assembled into cognitiveStateSpaceCert together with the three projection surjectivity lemmas and the companion non-collapse statement notCollapsedToSense. It discharges the fourth structural requirement listed in the module header: that the 5³ product remains strictly larger than any single factor. This cardinality separation supports the Recognition framework claim that conscious states cannot be reduced to any one recognition axis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.