notCollapsedToSense
plain-language theorem explainer
The theorem establishes that the cardinality of the product type Sense × Emotion × MemorySystem exceeds the cardinality of Sense. Researchers working with three-axis models of conscious states cite it to confirm the state space is irreducible to any single factor. The proof is a one-line wrapper that rewrites the two cardinality theorems and decides the numerical inequality.
Claim. $|Sense × Emotion × MemorySystem| > |Sense|$, where Sense, Emotion, and MemorySystem are each finite types of cardinality 5.
background
The module sets out the C1 structural claim that a conscious moment is spanned by three orthogonal recognition axes, each of configDim 5, so that the product equals 125 states. CognitiveState is defined as the product Sense × Emotion × MemorySystem. Sense is the inductive type with five constructors (sight, hearing, touch, smell, taste) and derives Fintype. The upstream theorems cognitiveStateCount and senseCount establish the respective cardinalities 125 and 5.
proof idea
One-line wrapper that applies rw on cognitiveStateCount and senseCount, then decide to verify 125 > 5.
why it matters
The result supplies the irreducible_1 field of cognitiveStateSpaceCert, completing the non-reducibility clause of the module's enumerated structure. It fills the fourth item listed in the module doc-comment: proving the product is strictly larger than any factor. The claim aligns with Recognition Science emphasis on non-degenerate product structures under the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.