CognitiveState
plain-language theorem explainer
The cognitive state is the Cartesian product of three five-element sets: sensory modalities, emotional categories, and memory subsystems. Modelers of discrete cognitive architectures cite this to anchor the total state count at 125 before proving projection properties. The declaration is introduced as a direct type abbreviation from the three inductive factor definitions.
Claim. Let $S$ be the set of five sense modalities, $E$ the set of five emotional states, and $M$ the set of five memory systems. The cognitive state space is the product type $S × E × M$.
background
This module formalizes the cognitive state space as the product of three orthogonal axes, each carrying five elements and yielding a discrete space of cardinality 125. The factor types are introduced inductively: Sense enumerates sight, hearing, touch, smell, taste; Emotion lists joy, sadness, fear, anger, disgust; MemorySystem covers working, episodic, semantic, procedural, priming. Each carries DecidableEq, Repr, BEq, and Fintype instances from Mathlib.
proof idea
The declaration is a direct abbreviation that constructs the product type from the three factor definitions Sense, Emotion, and MemorySystem. No lemmas or tactics are invoked beyond the built-in Cartesian product constructor.
why it matters
This definition supplies the core type for the cardinality theorem cognitiveStateCount and the certification structure CognitiveStateSpaceCert that records the 125 count together with surjectivity of the three projections. It constitutes the opening step of the module's C1 claim that the conscious moment is spanned by three recognition axes of dimension 5. Downstream results then establish non-collapse to any single factor or pair.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.