notCollapsedToMemory
The theorem shows that the full cognitive state space, defined as the product of sense, emotion, and memory factors each of size 5, has cardinality strictly larger than the memory factor alone. Researchers modeling conscious states via orthogonal recognition axes would cite it to confirm the space is irreducible to memory. The proof is a one-line term wrapper that substitutes the precomputed cardinalities 125 and 5 then invokes decide.
claim$|S × E × M| > |M|$, where $S$, $E$, and $M$ are the sense, emotion, and memory factor spaces each of cardinality 5.
background
The module models the conscious moment as the product of three orthogonal recognition axes, each of configuration dimension 5, so that Sense × Emotion × MemorySystem equals 125 states. CognitiveState is the product type of these three factors, while MemorySystem is the inductive type with five constructors (working, episodic, semantic, procedural, priming). The local setting is the structural claim that if the three-fold decomposition holds then the enumerated state space follows, with non-reducibility proved for each factor.
proof idea
The term-mode proof rewrites the inequality via the upstream theorems cognitiveStateCount (which sets the product cardinality to 125 by multiplying the three factor counts) and memorySystemCount (which sets the memory cardinality to 5 by decision), then applies decide to verify the numerical comparison.
why it matters in Recognition Science
It supplies one of the irreducibility conditions collected in the downstream cognitiveStateSpaceCert definition, which bundles the product cardinality, the three surjective projections, and the three non-collapse statements. This completes the non-reducibility clause of the module's C1 claim that the 125-state space is non-degenerate. In the broader framework it reinforces the three-axis decomposition as a structural prerequisite before any empirical test of independence.
scope and limits
- Does not prove that the three axes are empirically independent in neural recordings.
- Does not supply dynamics, transition rules, or time evolution on the state space.
- Does not address physical realization or embedding of the factors in hardware.
- Assumes the factorization into exactly these three axes holds.
formal statement (Lean)
70theorem notCollapsedToMemory :
71 Fintype.card CognitiveState > Fintype.card MemorySystem := by
proof body
Term-mode proof.
72 rw [cognitiveStateCount, memorySystemCount]; decide
73
74/-- The product is strictly larger than any pairwise factor too. -/