emotionProj_surj
plain-language theorem explainer
The theorem establishes surjectivity of the projection from the product CognitiveState onto its Emotion factor. Researchers working with the 125-element state space decomposition would cite it to confirm the product does not collapse any coordinate. The proof is a direct term-mode construction that supplies an explicit preimage triple for every target emotion value.
Claim. The map $pi_E : text{Sense} times text{Emotion} times text{MemorySystem} to text{Emotion}$ defined by $pi_E(s, e, m) := e$ is surjective.
background
The module defines CognitiveState as the product Sense × Emotion × MemorySystem, where each factor is an inductive type of cardinality 5. Sense enumerates sight, hearing, touch, smell, taste; Emotion enumerates joy, sadness, fear, anger, disgust; MemorySystem enumerates working, episodic, semantic, procedural, priming. This yields the enumerated 125-element space whose non-degenerate structure is certified by the three projection surjectivities.
proof idea
The proof is a one-line term-mode construction. It introduces an arbitrary target emotion x and returns the concrete witness (Sense.sight, x, MemorySystem.working) whose emotion component equals x by reflexivity.
why it matters
The result is invoked inside cognitiveStateSpaceCert to assemble the product cardinality with the three surjectivity statements and the irreducibility lemma. It completes the module's structural claim that the conscious moment is spanned by the full non-degenerate product of three orthogonal recognition axes each of dimension 5. In the Recognition Science setting this supports the C1 enumeration without addressing empirical independence of the axes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.