cognitiveStateCount
plain-language theorem explainer
The theorem establishes that the cognitive state space formed as the Cartesian product of three five-element sets has cardinality 125. Researchers constructing discrete models of conscious states as orthogonal recognition axes would cite this count when enumerating the space. The proof is a one-line simplification that substitutes the product cardinality formula together with the three factor cardinality theorems.
Claim. Let $S$, $E$, and $M$ be the sets of sense modalities, emotion types, and memory systems, each of cardinality 5. Then $|S × E × M| = 125$.
background
The module introduces three inductive types, each with five constructors and deriving Fintype: Sense (sight, hearing, touch, smell, taste), Emotion, and MemorySystem. CognitiveState is defined as their Cartesian product. The module proves the product cardinality equals 125, shows each projection is surjective, and establishes that the product is strictly larger than any factor or pair of factors. The local setting is the structural claim that a conscious moment is spanned by three orthogonal recognition axes each of configDim 5, with the explicit disclaimer that empirical independence of the axes is a testable hypothesis outside the Lean content.
proof idea
The term proof applies simp to unfold the product definition of CognitiveState and to invoke Fintype.card_prod together with the three upstream cardinality theorems senseCount, emotionCount, and memorySystemCount.
why it matters
This result supplies the product_count field of cognitiveStateSpaceCert and is invoked by the six irreducibility theorems that establish the product is strictly larger than any single factor or pairwise product. It realizes the C1 module claim that the conscious moment is spanned by three orthogonal axes of dimension 5. The cardinality 125 = 5³ aligns with the five-fold structure recurring across cross-domain constructions in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.