notCollapsedToEmotion
plain-language theorem explainer
The theorem shows that the product space of Sense, Emotion and MemorySystem has cardinality strictly larger than Emotion alone. Cross-domain modelers of conscious states cite it to confirm the three-axis decomposition is irreducible to any single factor. The proof is a one-line wrapper that substitutes the precomputed cardinalities 125 and 5 then decides the inequality.
Claim. Let $S$, $E$ and $M$ be the sets of sense, emotion and memory states, each of cardinality 5. Then $|S × E × M| > |E|$.
background
The module asserts that the conscious moment is spanned by three orthogonal recognition axes, each of configuration dimension 5, so that the product Sense × Emotion × MemorySystem equals 125 states. CognitiveState is defined as the product type of these three factors. Upstream results supply the cardinalities: cognitiveStateCount proves the product equals 125 by applying the Fintype product rule to the three factor counts, while emotionCount proves Emotion has exactly five elements by direct decision on its inductive definition.
proof idea
The proof is a one-line wrapper. It rewrites the goal with the lemmas cognitiveStateCount and emotionCount to obtain the concrete numerical comparison 125 > 5, then applies decide to resolve the decidable inequality.
why it matters
The result is referenced inside cognitiveStateSpaceCert as one of the three irreducibility witnesses (alongside notCollapsedToSense). It completes the module's non-reducibility claims and thereby supports the enumerated 125-element structure asserted in the module documentation. The declaration touches the open empirical question whether the three axes remain independent when measured in neural data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.