pith. machine review for the scientific record. sign in
structure definition def or abbrev high

CognitiveStateSpaceCert

show as:
view Lean formalization →

The declaration packages the claim that the cognitive state space is the cartesian product of three five-element sets, hence has cardinality 125, with surjective projections onto each factor and strict inequality against any proper subproduct. A neuroscientist or cognitive modeler working inside the Recognition Science cross-domain framework would cite it to fix the minimal dimensionality of a conscious moment. The structure is populated by a direct construction that invokes the Fintype cardinality of the product together with the three surject

claimLet $S$, $E$, $M$ be the five-element sets of sensory modalities, emotional primitives, and memory subsystems. The cognitive state space is the product $C := S × E × M$. Then $|C| = 125$, each of the three canonical projections $C → S$, $C → E$, $C → M$ is surjective, and $|C| > |S|$, $|C| > |E|$, $|C| > |M|$, $|C| > |S × E|$.

background

The module introduces three inductive types, each carrying a Fintype instance of cardinality 5: Sense with constructors sight, hearing, touch, smell, taste; Emotion with joy, sadness, fear, anger, disgust; and MemorySystem with working, episodic, semantic, procedural, priming. CognitiveState is defined as the abbreviation for their cartesian product. The local theoretical setting, stated in the module header, is the structural claim that a conscious moment is spanned by three orthogonal recognition axes each of dimension 5, so that the enumerated product space contains exactly 125 states. This rests directly on the upstream inductive definitions of the three factor types.

proof idea

The declaration is a structure definition whose fields collect the required cardinality and surjectivity statements. Concrete witnesses are supplied by the downstream definition cognitiveStateSpaceCert, which assigns the product cardinality via the Fintype instance on the triple product, the three projection-surjectivity lemmas, and the strict inequalities via the non-collapse lemmas.

why it matters in Recognition Science

This structure encodes the core C1 claim of the cross-domain module, fixing the dimensionality of the cognitive state space at 125. It is instantiated by the downstream cognitiveStateSpaceCert and supplies the discrete configuration space used in further cross-domain arguments. Within the Recognition Science framework it provides the 5³ state count compatible with the eight-tick octave and phi-ladder scaling, while the empirical independence of the three axes remains an open hypothesis outside the formal system.

scope and limits

formal statement (Lean)

  93structure CognitiveStateSpaceCert where
  94  product_count : Fintype.card CognitiveState = 125
  95  sense_surj : Function.Surjective (fun s : CognitiveState => s.1)
  96  emotion_surj : Function.Surjective (fun s : CognitiveState => s.2.1)
  97  memory_surj : Function.Surjective (fun s : CognitiveState => s.2.2)
  98  irreducible_1 : Fintype.card CognitiveState > Fintype.card Sense
  99  irreducible_2 : Fintype.card CognitiveState > Fintype.card Emotion
 100  irreducible_3 : Fintype.card CognitiveState > Fintype.card MemorySystem
 101  irreducible_pair : Fintype.card CognitiveState >
 102    Fintype.card (Sense × Emotion)
 103

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (4)

Lean names referenced from this declaration's body.