memorySystemCount
plain-language theorem explainer
The theorem establishes that the memory factor in the cognitive state space has cardinality five. Researchers constructing the 125-element product space for conscious moments would cite this cardinality when assembling the three-axis decomposition. The proof is a one-line wrapper that invokes the decide tactic on the Fintype instance derived from the five-constructor inductive definition.
Claim. Let MemorySystem be the finite type whose elements are the five memory categories working, episodic, semantic, procedural and priming. Then $|$MemorySystem$| = 5$.
background
The module defines the conscious moment as the product Sense × Emotion × MemorySystem, each factor of cardinality 5, yielding the enumerated space of 125 states. MemorySystem is introduced as an inductive type with exactly those five constructors and derives DecidableEq, Repr, BEq and Fintype. The local claim is conditional: if the three-fold decomposition holds, then the state space has this enumerated structure; empirical independence of the axes is left as a testable hypothesis outside Lean.
proof idea
one-line wrapper that applies the decide tactic to compute Fintype.card directly from the Fintype instance on the inductive type.
why it matters
The result supplies the memory cardinality to the product theorem that yields |CognitiveState| = 125 and to the three non-collapse theorems that establish the product strictly exceeds each factor or pairwise product. It completes the enumeration step inside the C1 structural claim that the conscious moment is spanned by three orthogonal axes of dimension 5. No open scaffolding is closed here; the module reports zero sorry overall.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.