CognitiveStateSpaceCert
plain-language theorem explainer
The declaration packages the claim that the cognitive state space is the cartesian product of three five-element sets, hence has cardinality 125, with surjective projections onto each factor and strict inequality against any proper subproduct. A neuroscientist or cognitive modeler working inside the Recognition Science cross-domain framework would cite it to fix the minimal dimensionality of a conscious moment. The structure is populated by a direct construction that invokes the Fintype cardinality of the product together with the three surject
Claim. Let $S$, $E$, $M$ be the five-element sets of sensory modalities, emotional primitives, and memory subsystems. The cognitive state space is the product $C := S × E × M$. Then $|C| = 125$, each of the three canonical projections $C → S$, $C → E$, $C → M$ is surjective, and $|C| > |S|$, $|C| > |E|$, $|C| > |M|$, $|C| > |S × E|$.
background
The module introduces three inductive types, each carrying a Fintype instance of cardinality 5: Sense with constructors sight, hearing, touch, smell, taste; Emotion with joy, sadness, fear, anger, disgust; and MemorySystem with working, episodic, semantic, procedural, priming. CognitiveState is defined as the abbreviation for their cartesian product. The local theoretical setting, stated in the module header, is the structural claim that a conscious moment is spanned by three orthogonal recognition axes each of dimension 5, so that the enumerated product space contains exactly 125 states. This rests directly on the upstream inductive definitions of the three factor types.
proof idea
The declaration is a structure definition whose fields collect the required cardinality and surjectivity statements. Concrete witnesses are supplied by the downstream definition cognitiveStateSpaceCert, which assigns the product cardinality via the Fintype instance on the triple product, the three projection-surjectivity lemmas, and the strict inequalities via the non-collapse lemmas.
why it matters
This structure encodes the core C1 claim of the cross-domain module, fixing the dimensionality of the cognitive state space at 125. It is instantiated by the downstream cognitiveStateSpaceCert and supplies the discrete configuration space used in further cross-domain arguments. Within the Recognition Science framework it provides the 5³ state count compatible with the eight-tick octave and phi-ladder scaling, while the empirical independence of the three axes remains an open hypothesis outside the formal system.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.