notCollapsedToPair3
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 in Recognition Science
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.
scope and limits
- Does not prove that the three axes are empirically independent in neural data.
- Does not specify the internal structure or dynamics of state transitions.
- Does not claim that these cardinalities correspond to measurable quantities in physical systems.
formal statement (Lean)
87theorem notCollapsedToPair3 :
88 Fintype.card CognitiveState > Fintype.card (Emotion × MemorySystem) := by
proof body
Tactic-mode proof.
89 have h : Fintype.card (Emotion × MemorySystem) = 25 := by
90 simp only [Fintype.card_prod, emotionCount, memorySystemCount]
91 rw [cognitiveStateCount, h]; decide
92