cognitiveStateCount
plain-language theorem explainer
The theorem establishes that the cognitive state space, formed as the product of three five-element types, has cardinality exactly 125. Researchers modeling conscious moments via three orthogonal recognition axes would cite this to fix the discrete size of the state space at 5³. The proof is a one-line simplification that applies the product cardinality rule to the precomputed counts of each factor.
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 of cardinality 5: Sense with constructors sight, hearing, touch, smell, taste; Emotion; and MemorySystem. CognitiveState is defined as the product Sense × Emotion × MemorySystem. Upstream theorems senseCount, emotionCount, and memorySystemCount each establish Fintype.card = 5 by direct decision. The local setting is the structural claim that a conscious moment is spanned by three orthogonal recognition axes of configDim D = 5, so that the state space is the enumerated product 5 × 5 × 5 = 125.
proof idea
The proof is a one-line term-mode wrapper. It applies simp to the definition of CognitiveState, the lemma Fintype.card_prod, and the three cardinality theorems senseCount, emotionCount, memorySystemCount, which together evaluate the product 5 * 5 * 5 directly to 125.
why it matters
This supplies the product_count field inside cognitiveStateSpaceCert and is invoked by the family of notCollapsedTo* theorems that prove the product is strictly larger than any factor or pairwise subproduct. It realizes the C1 structural claim of the module: under the three-axis decomposition the conscious moment has enumerated structure 5³ = 125. The framework treats the count as a necessary discrete anchor before any empirical test of axis independence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.