notCollapsedToPair3
plain-language theorem explainer
The theorem establishes that the cardinality of the full cognitive state space exceeds the cardinality of the emotion-memory product. Researchers constructing three-axis models of conscious states cite this to confirm the space is irreducible to any pair of factors. The proof computes the two-factor product cardinality as 25 from the component counts, substitutes the known 125 for the three-factor product, and decides the inequality.
Claim. $|Sense × Emotion × MemorySystem| > |Emotion × MemorySystem|$ where each factor is an inductive type of cardinality 5.
background
The module defines three inductive types of cardinality 5: Emotion with constructors joy, sadness, fear, anger, disgust; MemorySystem with working, episodic, semantic, procedural, priming; and the omitted Sense. Their Cartesian product is the cognitive state space, whose cardinality equals 125 by the upstream theorem cognitiveStateCount. The module proves each projection is surjective and that the full product is strictly larger than any two-factor subproduct.
proof idea
The proof first sets the emotion-memory product cardinality to 25 by simplifying the product cardinality expression with the known counts of 5 for each factor. It then rewrites the target inequality using the established count of 125 for the full cognitive state space and applies a decision procedure to confirm the numerical comparison.
why it matters
This result completes the non-reducibility section of the module, showing the 125-state space cannot collapse to any pair of axes. It directly supports the structural claim that a conscious moment is spanned by three orthogonal recognition axes of dimension 5. The module leaves empirical independence of the axes as an open hypothesis outside the formal system.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.