senseProj_surj
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not establish empirical independence of the three axes in neural data.
- Does not derive the cardinality 5 from the forcing chain or Recognition Composition Law.
- Does not model dynamics or transitions between states.
- Does not connect the state space to physical constants or the phi-ladder.
Lean usage
example (x : Sense) : ∃ s : CognitiveState, s.1 = x := senseProj_surj xformal statement (Lean)
49theorem senseProj_surj : Function.Surjective (fun s : CognitiveState => s.1) := by
proof body
Term-mode proof.
50 intro x; exact ⟨(x, Emotion.joy, MemorySystem.working), rfl⟩
51
52/-- Emotion projection is surjective. -/