Emotion
The Emotion inductive type enumerates five discrete emotional states as the second factor in the cognitive state space. Researchers modeling the Recognition Science decomposition of conscious states would cite this when establishing the 5×5×5 product structure. The declaration is a plain inductive definition with no proof obligations, automatically deriving decidable equality and finite type structure for downstream cardinality and surjectivity results.
claimLet $E$ denote the set of emotions. Then $E = $ {joy, sadness, fear, anger, disgust}, a finite set of cardinality 5 equipped with decidable equality.
background
The Cognitive State Space module defines three orthogonal recognition axes, each of cardinality 5: Sense, Emotion, and MemorySystem. Their Cartesian product yields the CognitiveState type whose total cardinality is 125. The module establishes that each projection is surjective and that the product is strictly larger than any factor or pairwise subproduct. This construction supplies the discrete state space required for the cross-domain recognition claim that a conscious moment decomposes into three independent 5-element components.
proof idea
This is an inductive definition that introduces five constructors. It derives DecidableEq, Repr, BEq, and Fintype automatically, which directly enables the sibling theorem emotionCount establishing Fintype.card Emotion = 5.
why it matters in Recognition Science
Emotion supplies the middle factor for the CognitiveState abbrev and the CognitiveStateSpaceCert structure. The certificate records the product cardinality 125, the three surjective projections, and the irreducibility inequalities. It therefore anchors the 5³ = 125 enumeration inside the Recognition Science framework, where the conscious moment is required to be a finite discrete space spanned by three recognition axes.
scope and limits
- Does not claim these five emotions exhaust all affective states.
- Does not assert empirical independence of the three axes in neural data.
- Does not derive transition dynamics or stability conditions among emotions.
- Does not link to the phi-ladder, J-cost, or forcing chain T0-T8.
formal statement (Lean)
31inductive Emotion where
32 | joy | sadness | fear | anger | disgust
33 deriving DecidableEq, Repr, BEq, Fintype
34