MemorySystem
plain-language theorem explainer
MemorySystem enumerates five memory variants that serve as one coordinate axis in the 125-element cognitive state space. Modelers of the Recognition Science cross-domain decomposition cite the type when constructing the product Sense × Emotion × MemorySystem. The declaration is a direct inductive definition that automatically supplies the Fintype instance used by downstream cardinality theorems.
Claim. Let $M$ be the finite set whose elements are the five memory types working, episodic, semantic, procedural, and priming.
background
The module models the conscious moment as the Cartesian product of three orthogonal axes, each of cardinality 5, so that Sense × Emotion × MemorySystem yields exactly 125 states. MemorySystem supplies the third factor; its five constructors are listed explicitly and the type is equipped with DecidableEq, Repr, BEq, and Fintype. The module doc states that the Lean content is conditional on the three-fold decomposition: if the axes are adopted, then the enumerated product structure follows.
proof idea
The declaration is the inductive definition itself; no separate proof body exists. The deriving clause directly installs the four type-class instances required by later cardinality and surjectivity statements.
why it matters
MemorySystem is the concrete type used to form the abbrev CognitiveState and the structure CognitiveStateSpaceCert, which records the product cardinality 125 together with the three surjectivity theorems and the irreducibility inequalities. It therefore supplies the memory axis required by the module's structural claim for the 5³ state space. The same type appears in the non-collapse results notCollapsedToMemory and notCollapsedToPair2.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.