notCollapsedToSense
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 in Recognition Science
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.
scope and limits
- Does not prove empirical independence of the three axes in neural recordings.
- Does not derive the specific dimension 5 from Recognition Science forcing steps.
- Does not address state transitions or temporal dynamics.
Lean usage
irreducible_1 := notCollapsedToSenseformal statement (Lean)
63theorem notCollapsedToSense : Fintype.card CognitiveState > Fintype.card Sense := by
proof body
One-line wrapper that applies rw.
64 rw [cognitiveStateCount, senseCount]; decide
65