notCollapsedToSense
plain-language theorem explainer
The theorem shows that the cognitive state space formed as the product of three five-element sets has strictly more states than the sense component alone. Researchers modeling conscious moments via a non-degenerate three-axis decomposition would cite this to confirm the space does not collapse onto any single factor. The proof is a one-line wrapper that rewrites using the precomputed cardinalities and lets decide resolve the inequality.
Claim. $|S| > 5$ where $S$ is the Cartesian product of three sets each of cardinality 5.
background
The module defines three inductive types, each with five constructors, that represent orthogonal recognition axes of dimension 5. CognitiveState is the product of these three types. The upstream theorem cognitiveStateCount establishes that the product has cardinality 125 by multiplying the individual factor counts, while senseCount fixes the sense factor at cardinality 5.
proof idea
One-line wrapper that rewrites the goal using cognitiveStateCount and senseCount, then applies decide to resolve the numerical comparison.
why it matters
This supplies the irreducible_1 field inside cognitiveStateSpaceCert, completing the non-reducibility clause of the C1 structural claim. It guarantees the enumerated 125-state space is strictly larger than any single axis, consistent with the module's emphasis on non-degenerate products. The module explicitly leaves empirical independence of the axes as a separate testable hypothesis outside the Lean content.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.