`MemorySystem`

definition

show as: view math explainer →

module: IndisputableMonolith.CrossDomain.CognitiveStateSpace
domain: CrossDomain
line: 35 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.CrossDomain.CognitiveStateSpace on GitHub at line 35.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

used by

formal source

  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.