IndisputableMonolith.CrossDomain.CognitiveStateSpace

   1import Mathlib
   2
   3/-!
   4# C1: Cognitive State Space — 5³ = 125 — Wave 62 Cross-Domain
   5
   6Structural claim: the conscious moment is spanned by three orthogonal
   7recognition axes, each of configDim D = 5:
   8
   9  Sense × Emotion × MemorySystem  =  5 × 5 × 5  =  125.
  10
  11This module does four things:
  121. Defines the three factor types, each of cardinality 5.
  132. Defines the product type `CognitiveState` and proves `|CognitiveState| = 125`.
  143. Proves each projection is surjective (the product is non-degenerate).
  154. Proves non-reducibility: the product is strictly larger than any factor.
  16
  17What this does NOT prove: that these three axes are empirically independent
  18in neural data. That is a testable hypothesis about EEG decoders, not a Lean
  19theorem. The Lean content here is: IF the three-fold decomposition holds,
  20THEN the state space has the enumerated structure.
  21
  22Lean status: 0 sorry, 0 axiom.
  23-/
  24
  25namespace IndisputableMonolith.CrossDomain.CognitiveStateSpace
  26
  27inductive Sense where
  28  | sight | hearing | touch | smell | taste
  29  deriving DecidableEq, Repr, BEq, Fintype
  30
  31inductive Emotion where
  32  | joy | sadness | fear | anger | disgust
  33  deriving DecidableEq, Repr, BEq, Fintype
  34
  35inductive MemorySystem where
  36  | working | episodic | semantic | procedural | priming
  37  deriving DecidableEq, Repr, BEq, Fintype
  38
  39theorem senseCount : Fintype.card Sense = 5 := by decide
  40theorem emotionCount : Fintype.card Emotion = 5 := by decide
  41theorem memorySystemCount : Fintype.card MemorySystem = 5 := by decide
  42
  43abbrev CognitiveState : Type := Sense × Emotion × MemorySystem
  44
  45theorem cognitiveStateCount : Fintype.card CognitiveState = 125 := by
  46  simp only [CognitiveState, Fintype.card_prod, senseCount, emotionCount, memorySystemCount]
  47
  48/-- Sense projection is surjective. -/
  49theorem senseProj_surj : Function.Surjective (fun s : CognitiveState => s.1) := by
  50  intro x; exact ⟨(x, Emotion.joy, MemorySystem.working), rfl⟩
  51
  52/-- Emotion projection is surjective. -/
  53theorem emotionProj_surj :
  54    Function.Surjective (fun s : CognitiveState => s.2.1) := by
  55  intro x; exact ⟨(Sense.sight, x, MemorySystem.working), rfl⟩
  56
  57/-- Memory projection is surjective. -/
  58theorem memoryProj_surj :
  59    Function.Surjective (fun s : CognitiveState => s.2.2) := by
  60  intro x; exact ⟨(Sense.sight, Emotion.joy, x), rfl⟩
  61
  62/-- Non-reducibility: the product is strictly larger than any single factor. -/
  63theorem notCollapsedToSense : Fintype.card CognitiveState > Fintype.card Sense := by
  64  rw [cognitiveStateCount, senseCount]; decide
  65
  66theorem notCollapsedToEmotion :
  67    Fintype.card CognitiveState > Fintype.card Emotion := by
  68  rw [cognitiveStateCount, emotionCount]; decide
  69
  70theorem notCollapsedToMemory :
  71    Fintype.card CognitiveState > Fintype.card MemorySystem := by
  72  rw [cognitiveStateCount, memorySystemCount]; decide
  73
  74/-- The product is strictly larger than any pairwise factor too. -/
  75theorem notCollapsedToPair1 :
  76    Fintype.card CognitiveState > Fintype.card (Sense × Emotion) := by
  77  have h : Fintype.card (Sense × Emotion) = 25 := by
  78    simp only [Fintype.card_prod, senseCount, emotionCount]
  79  rw [cognitiveStateCount, h]; decide
  80
  81theorem notCollapsedToPair2 :
  82    Fintype.card CognitiveState > Fintype.card (Sense × MemorySystem) := by
  83  have h : Fintype.card (Sense × MemorySystem) = 25 := by
  84    simp only [Fintype.card_prod, senseCount, memorySystemCount]
  85  rw [cognitiveStateCount, h]; decide
  86
  87theorem notCollapsedToPair3 :
  88    Fintype.card CognitiveState > Fintype.card (Emotion × MemorySystem) := by
  89  have h : Fintype.card (Emotion × MemorySystem) = 25 := by
  90    simp only [Fintype.card_prod, emotionCount, memorySystemCount]
  91  rw [cognitiveStateCount, h]; decide
  92
  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
 104def cognitiveStateSpaceCert : CognitiveStateSpaceCert where
 105  product_count := cognitiveStateCount
 106  sense_surj := senseProj_surj
 107  emotion_surj := emotionProj_surj
 108  memory_surj := memoryProj_surj
 109  irreducible_1 := notCollapsedToSense
 110  irreducible_2 := notCollapsedToEmotion
 111  irreducible_3 := notCollapsedToMemory
 112  irreducible_pair := notCollapsedToPair1
 113
 114end IndisputableMonolith.CrossDomain.CognitiveStateSpace
 115