notCollapsedToPair2
The theorem shows that the full cognitive state space of 125 elements strictly exceeds the 25-element product of the Sense and MemorySystem axes. Modelers of conscious states as a three-factor decomposition would cite it to confirm that the state space cannot collapse to any two-axis subset. The proof computes the pair cardinality via the product rule and known factor counts, then rewrites with the full product count and decides the inequality.
claim$|SENSE × EMOTION × MEMORYSYSTEM| > |SENSE × MEMORYSYSTEM|$, where each axis is a five-element set of recognition primitives.
background
The module treats the conscious moment as spanned by three orthogonal recognition axes, each of cardinality 5. Sense is the inductive type with constructors sight, hearing, touch, smell, taste. MemorySystem is the inductive type with constructors working, episodic, semantic, procedural, priming. CognitiveState is the product type Sense × Emotion × MemorySystem, whose cardinality is established as 125 by the upstream theorem cognitiveStateCount via the product rule on the three factor counts.
proof idea
The tactic proof first establishes an auxiliary equality that the Sense-MemorySystem product has cardinality 25 by simplification with the product cardinality rule and the two factor-count lemmas senseCount and memorySystemCount. It then rewrites the target inequality using the upstream result cognitiveStateCount and closes with the decide tactic on the concrete numerical comparison 125 > 25.
why it matters in Recognition Science
This result completes one of the four structural tasks listed in the module documentation: proving that the 125-element product is strictly larger than any two-factor subproduct. It thereby supports the claim that the three-axis decomposition is non-degenerate. The module documentation notes that the Lean content assumes the three-fold decomposition and derives its enumerated consequences, leaving empirical independence of the axes as a separate testable hypothesis.
scope and limits
- Does not prove that the three axes are empirically independent in neural recordings.
- Does not derive the specific five-element enumerations from a deeper dynamical principle.
- Does not address state transitions or temporal evolution within the space.
- Does not claim that the decomposition is unique or minimal among all possible factorizations.
formal statement (Lean)
81theorem notCollapsedToPair2 :
82 Fintype.card CognitiveState > Fintype.card (Sense × MemorySystem) := by
proof body
Tactic-mode proof.
83 have h : Fintype.card (Sense × MemorySystem) = 25 := by
84 simp only [Fintype.card_prod, senseCount, memorySystemCount]
85 rw [cognitiveStateCount, h]; decide
86