memoryProj_surj
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.