PrimaryEmotion
plain-language theorem explainer
PrimaryEmotion enumerates the five basic emotions joy, sadness, fear, anger, disgust as a finite type. Cross-domain researchers cite the definition when verifying that emotional categories satisfy the D=5 cardinality pattern required for ConfigDimUniversalityCert. The declaration is a direct inductive construction that automatically derives Fintype, DecidableEq and related instances.
Claim. Let PrimaryEmotion be the finite set with elements joy, sadness, fear, anger, disgust, equipped with decidable equality and a Fintype structure of cardinality 5.
background
The module establishes that configDim D=5 appears across five domains (sensory, emotion, biological, economic, linguistic) with |T|=5 in each case. HasConfigDim5 (T : Type) is the predicate that holds precisely when Fintype.card T = 5. The local setting is the structural claim that any three D=5 types yield a product of size 125 and all five yield 3125, with equicardinality between any pair.
proof idea
The declaration is the inductive definition of the five-element type PrimaryEmotion together with the derived Fintype instance. No lemmas are applied; the Fintype.card = 5 fact used downstream is obtained by decide after unfolding HasConfigDim5.
why it matters
PrimaryEmotion supplies the emotion_5 field of ConfigDimUniversalityCert and is invoked by emotion_hasConfigDim5, three_domain_product and five_domain_product. It therefore participates in the module's demonstration that D=5 holds uniformly across domains, supporting the broader claim that configDim D=5 occurs with high frequency in the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.