pith. machine review for the scientific record. sign in
abbrev definition def or abbrev high

CognitiveState

show as:
view Lean formalization →

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.

claimLet $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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  43abbrev CognitiveState : Type := Sense × Emotion × MemorySystem

proof body

Definition body.

  44

used by (11)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.