emotionProj_surj

formal source

  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