cognitiveStateCount
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not establish empirical independence of the three axes in neural data.
- Does not derive the dimension 5 from deeper recognition axioms.
- Does not address continuous embeddings or limits of the state space.
Lean usage
rw [cognitiveStateCount] at hformal statement (Lean)
45theorem cognitiveStateCount : Fintype.card CognitiveState = 125 := by
proof body
Term-mode proof.
46 simp only [CognitiveState, Fintype.card_prod, senseCount, emotionCount, memorySystemCount]
47
48/-- Sense projection is surjective. -/