MemorySystem
plain-language theorem explainer
MemorySystem enumerates five memory categories as one axis in the 5×5×5 cognitive state space. Modelers of recognition-based cognition cite it when constructing the product type whose cardinality is fixed at 125. The declaration is a direct inductive definition that derives the Fintype instance with no separate proof steps.
Claim. Let $M$ be the finite type whose elements are the five memory categories working, episodic, semantic, procedural and priming. Then $|M|=5$.
background
The module establishes a three-axis decomposition of the conscious moment: Sense × Emotion × MemorySystem, each factor of cardinality 5, yielding the product of 125 states. MemorySystem supplies the third axis. The local setting is the structural claim that IF the three-fold decomposition holds THEN the enumerated state space follows; empirical independence of the axes is left as a testable hypothesis outside the Lean content.
proof idea
The declaration is the inductive definition introducing the five constructors and deriving DecidableEq, Repr, BEq and Fintype automatically.
why it matters
MemorySystem supplies the third factor for the abbrev CognitiveState and for the structure CognitiveStateSpaceCert that records the product cardinality 125 together with the three surjectivity statements and the irreducibility inequalities. It thereby fills the cross-domain enumeration step in the 5³=125 claim. The open question left explicit is whether the three axes remain empirically independent in neural data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.