emotionProj_surj
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not prove empirical independence of the three axes in neural data.
- Does not define dynamics or transition rules between states.
- Does not map states to physical or neural observables.
- Does not claim uniqueness of the decomposition.
Lean usage
example : Function.Surjective (fun s : CognitiveState => s.2.1) := emotionProj_surjformal statement (Lean)
53theorem emotionProj_surj :
54 Function.Surjective (fun s : CognitiveState => s.2.1) := by
proof body
Term-mode proof.
55 intro x; exact ⟨(Sense.sight, x, MemorySystem.working), rfl⟩
56
57/-- Memory projection is surjective. -/