senseCount
The inductive type Sense, with constructors sight, hearing, touch, smell and taste, has finite cardinality exactly 5. Models that decompose conscious states into three orthogonal axes of dimension 5 cite this result to obtain the total state space size of 125. The proof is a one-line wrapper that applies the decide tactic to the Fintype instance derived from the inductive definition.
claimThe cardinality of the type Sense is five: $|Sense| = 5$, where Sense is the inductive type with constructors sight, hearing, touch, smell, and taste.
background
The module defines three factor types each of cardinality 5 to model the conscious moment as the product Sense × Emotion × MemorySystem. Sense is the inductive type generated by the five constructors sight, hearing, touch, smell, taste and carries DecidableEq, Repr, BEq, and Fintype instances. The module documentation states that this product equals 125 elements and that the Lean content is conditional on the three-fold decomposition holding.
proof idea
The proof is a one-line wrapper that invokes the decide tactic on the equality Fintype.card Sense = 5, which is decidable from the inductive definition of Sense and its derived Fintype instance.
why it matters in Recognition Science
This result is invoked directly by cognitiveStateCount to obtain Fintype.card CognitiveState = 125 and by the non-reducibility theorems notCollapsedToSense, notCollapsedToPair1, and notCollapsedToPair2. It supplies the enumeration step for the 5³ state space in the cross-domain cognitive model, consistent with the module's structural claim of three orthogonal axes each of dimension 5.
scope and limits
- Does not establish empirical independence of the three axes in neural data.
- Does not derive the number five from the Recognition Science forcing chain or J-cost.
- Does not claim that the five modalities exhaust biological senses.
- Does not address correlations among axes in actual EEG recordings.
Lean usage
theorem cognitiveStateCount : Fintype.card CognitiveState = 125 := by simp only [CognitiveState, Fintype.card_prod, senseCount, emotionCount, memorySystemCount]formal statement (Lean)
39theorem senseCount : Fintype.card Sense = 5 := by decide