memoryProj_surj
The projection from the cognitive state triple onto its memory component is surjective. Researchers modeling the 125-state conscious moment would cite this to confirm the product does not collapse along any axis. The proof is a one-line term construction that pairs any memory value with fixed sense and emotion elements.
claimLet $S$, $E$, and $M$ be the sets of sense, emotion, and memory modalities. The projection map $S × E × M → M$ given by the third coordinate is surjective.
background
The module defines Sense and Emotion as inductive types with five constructors each (sight/hearing/touch/smell/taste and joy/sadness/fear/anger/disgust). CognitiveState is the product type Sense × Emotion × MemorySystem. The local setting is the claim that the conscious moment is spanned by three orthogonal recognition axes of dimension 5, yielding a 125-element state space. Upstream results supply the type definitions of Sense, Emotion, and CognitiveState; the remaining depends_on edges are unrelated is-classes from other modules.
proof idea
This is a term-mode proof. For arbitrary memory value x the construction exhibits the triple (Sense.sight, Emotion.joy, x) and closes by reflexivity on the projection.
why it matters in Recognition Science
The result is assembled into cognitiveStateSpaceCert, which records the product cardinality together with all three surjections and the non-collapse statement. It fills the structural requirement that each axis remains independently accessible inside the 125-state space. In the Recognition framework this supports the cross-domain decomposition without reducing to any single factor.
scope and limits
- Does not prove empirical independence of the three axes in neural recordings.
- Does not specify the internal structure of MemorySystem beyond its five-element cardinality.
- Does not address state transitions or temporal dynamics.
- Does not claim the decomposition matches observed brain states.
Lean usage
example : Function.Surjective (fun s : CognitiveState => s.2.2) := memoryProj_surjformal statement (Lean)
58theorem memoryProj_surj :
59 Function.Surjective (fun s : CognitiveState => s.2.2) := by
proof body
Term-mode proof.
60 intro x; exact ⟨(Sense.sight, Emotion.joy, x), rfl⟩
61
62/-- Non-reducibility: the product is strictly larger than any single factor. -/