PrimaryEmotion
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.