Sense
Sense is the inductive type enumerating five sensory modalities that supply one axis of the 5³ cognitive state space. Researchers formalizing the cross-domain decomposition would cite it when building the product CognitiveState and proving its cardinality equals 125. The declaration is a direct inductive definition that automatically equips the type with decidable equality and finite cardinality.
claimLet $S$ be the finite set whose elements are the five sensory modalities sight, hearing, touch, smell, and taste. The type $S$ is equipped with decidable equality and is a finite type of cardinality 5.
background
The module defines three factor types of cardinality 5 whose product forms the cognitive state space. Sense supplies the first factor; the other two are Emotion and MemorySystem. Their Cartesian product is declared as CognitiveState, and the module proves that this product has exactly 125 elements while each projection remains surjective. The local setting is the structural claim that the conscious moment is spanned by three orthogonal recognition axes, each of configDim 5, yielding the enumerated structure 5 × 5 × 5 = 125.
proof idea
The declaration is the inductive definition introducing the five constructors sight, hearing, touch, smell, and taste. It derives the instances DecidableEq, Repr, BEq, and Fintype in a single step with no explicit proof body.
why it matters in Recognition Science
Sense is required to form the product CognitiveState and to establish the theorem cognitiveStateCount that |CognitiveState| = 125. It appears inside the structure CognitiveStateSpaceCert that records the product cardinality, the three surjectivity statements, and the irreducibility inequalities. The construction fills the module's Wave 62 claim that the conscious moment decomposes into three orthogonal axes of dimension 5; downstream results such as defect_moat_zero_iff_sat in CircuitLedger rely on the same product structure for satisfiability arguments.
scope and limits
- Does not assert empirical independence of the three axes in neural recordings.
- Does not derive the number 5 from earlier Recognition Science forcing steps.
- Does not model dynamical interactions or transitions among states.
- Does not claim that the five modalities exhaust all possible sensory distinctions.
formal statement (Lean)
27inductive Sense where
28 | sight | hearing | touch | smell | taste
29 deriving DecidableEq, Repr, BEq, Fintype
30