senseProj_surj
plain-language theorem explainer
Surjectivity of the projection onto Sense in the product CognitiveState = Sense × Emotion × MemorySystem guarantees every sensory value appears in some state. Researchers modeling the 125-element conscious moment cite it to confirm the three-factor product is non-degenerate. The proof is a direct term construction that supplies an explicit preimage triple for any input sense value.
Claim. The projection map from the product space $Sense × Emotion × MemorySystem$ onto $Sense$ is surjective.
background
The module defines the conscious moment as the cartesian product of three 5-element spaces whose product yields exactly 125 states. Sense is the inductive type with five constructors (sight, hearing, touch, smell, taste). Emotion enumerates joy, sadness, fear, anger, disgust. MemorySystem enumerates working, episodic, semantic, procedural, priming. CognitiveState is the abbreviation for their product type. The module states that if the three-fold decomposition holds then the state space has the enumerated structure, without claiming empirical independence in neural data.
proof idea
The proof is a one-line term-mode construction. For arbitrary sense value x it forms the triple (x, Emotion.joy, MemorySystem.working) and applies reflexivity to witness that the first projection recovers x.
why it matters
The result supplies the sense_surj field inside cognitiveStateSpaceCert, which records the full product count together with the three surjectivity statements and the irreducibility condition. It discharges the third structural requirement listed in the module documentation: each projection must be surjective so the product remains non-degenerate. In the Recognition Science setting this secures the 5 × 5 × 5 enumeration of the conscious moment as a prerequisite for cross-domain claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.