emotionCount
emotionCount establishes that the Emotion inductive type, with constructors joy, sadness, fear, anger and disgust, has cardinality exactly 5. Researchers assembling the Recognition Science cognitive model cite this when forming the 125-element CognitiveState as the product of three five-element factors. The proof is a one-line decide tactic that exhausts the finite enumeration supplied by the derived Fintype instance.
claimLet Emotion be the finite set with elements joy, sadness, fear, anger, disgust. Then $|$Emotion$| = 5$.
background
The CrossDomain.CognitiveStateSpace module models the conscious moment as the product Sense × Emotion × MemorySystem, each axis of cardinality 5, for a total of 125 states. Emotion is introduced as an inductive type whose five constructors derive DecidableEq, Repr, BEq and Fintype, enabling direct cardinality calculations. The module documentation states that this supplies the enumerated structure under the assumption of the three-fold decomposition, without claiming empirical independence of the axes in neural data.
proof idea
The proof is a one-line wrapper that invokes the decide tactic on the goal Fintype.card Emotion = 5. The tactic uses the derived Fintype instance on the five-constructor inductive to compute the cardinality by exhaustive enumeration and confirms the equality.
why it matters in Recognition Science
This cardinality is invoked by cognitiveStateCount to obtain |CognitiveState| = 125 via the product formula, and by the non-collapse results notCollapsedToEmotion, notCollapsedToPair1 and notCollapsedToPair3 that establish the full state space strictly exceeds any factor or pair. It supplies the enumeration step required by the module's 5³ = 125 structural claim. Within the Recognition framework the result contributes the configDim = 5 factor to the cross-domain cognitive model, separate from the spatial D = 3 derived in the T0-T8 forcing chain.
scope and limits
- Does not assert that the five listed emotions exhaust any empirical classification.
- Does not prove independence or orthogonality among Sense, Emotion and MemorySystem.
- Does not supply dynamics, transitions or a metric on the 125 states.
- Does not map the states to physical observables or EEG signatures.
Lean usage
rw [emotionCount]formal statement (Lean)
40theorem emotionCount : Fintype.card Emotion = 5 := by decide