notCollapsedToPair1
plain-language theorem explainer
The theorem shows that the cardinality of the full cognitive state space strictly exceeds the cardinality of any two-factor product. Researchers formalizing the three-axis decomposition of conscious states would cite it to confirm that the space cannot be reduced to a pairwise subspace. The proof is a short tactic sequence that substitutes the known finite cardinalities for each component and decides the resulting numerical inequality.
Claim. Let $S$, $E$, and $M$ be the finite sets of sense modalities, emotional states, and memory systems, each of cardinality 5. Let $C = S × E × M$. Then $|C| > |S × E|$.
background
The module formalizes a conscious moment as the product of three orthogonal recognition axes, each of configuration dimension 5, yielding the 125-element space $C = S × E × M$. Sense is the inductive type with constructors sight, hearing, touch, smell, taste; Emotion has joy, sadness, fear, anger, disgust; MemorySystem is the remaining factor of equal size. Upstream results establish senseCount = 5, emotionCount = 5, and cognitiveStateCount = 125 via direct application of Fintype.card_prod.
proof idea
The proof first reduces the pair cardinality to 25 by simp on Fintype.card_prod together with senseCount and emotionCount. It then rewrites the goal using cognitiveStateCount and applies decide to confirm 125 > 25.
why it matters
The result is referenced inside cognitiveStateSpaceCert as the irreducible_1 field, completing the non-reducibility clause of the module's four tasks. It supports the structural claim that the state space is strictly 5³-dimensional once the three-fold decomposition is assumed, without addressing empirical independence of the axes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.