PrimaryEmotion
PrimaryEmotion is the inductive type whose five constructors are joy, sadness, fear, anger and disgust. Cross-domain researchers cite it to witness the D=5 pattern in the emotional domain, completing the set of five domain instances required for the universality certificate. The declaration is a plain inductive definition that derives DecidableEq, Repr, BEq and Fintype automatically.
claimLet $E$ be the finite set of primary emotions given by $E = $ {joy, sadness, fear, anger, disgust}, equipped with decidable equality and a Fintype structure of cardinality 5.
background
The ConfigDim Universality module formalises the observation that configuration dimension D=5 occurs across domains, with HasConfigDim5 (T : Type) the predicate that holds precisely when the cardinality of T equals 5. PrimaryEmotion supplies the concrete instance for the emotional domain, parallel to the sensory, biological, economic and linguistic instances defined in the same file. The module states that any three such types multiply to cardinality 125 and all five multiply to 3125.
proof idea
The declaration is an inductive definition with five constructors. The deriving clause installs DecidableEq, Repr, BEq and Fintype instances without further proof obligations.
why it matters in Recognition Science
PrimaryEmotion is required by ConfigDimUniversalityCert, which assembles the five HasConfigDim5 facts, and by the product theorems three_domain_product and five_domain_product that compute 125 and 3125 respectively. It therefore supplies one of the five domain witnesses needed to establish the structural claim that D=5 is the universal configuration dimension in the Recognition Science framework.
scope and limits
- Does not claim these five constructors exhaust all emotional phenomena.
- Does not map the constructors to any physical or biological observables.
- Does not prove that D=5 is the only possible configuration dimension.
- Does not connect the type to the J-cost function or the forcing chain.
formal statement (Lean)
30inductive PrimaryEmotion where
31 | joy | sadness | fear | anger | disgust
32 deriving DecidableEq, Repr, BEq, Fintype
33