DomainInstance

formal source

 763/-- A **domain instance** is a functor from RecAlg to a specific domain.
 764    Each domain algebra (qualia, ethics, semantics, etc.) is obtained by
 765    applying such a functor to the canonical Recognition Algebra. -/
 766structure DomainInstance where
 767  /-- Name of the domain -/
 768  name : String
 769  /-- The state space of this domain -/
 770  stateType : Type
 771  /-- How to embed cost into domain-specific measurement -/
 772  costEmbed : ℝ → ℝ
 773  /-- The embedding preserves ordering (monotone) -/
 774  monotone : ∀ a b : ℝ, a ≤ b → costEmbed a ≤ costEmbed b
 775
 776/-- **Qualia domain instance**: strain = phase_mismatch × J(intensity) -/
 777noncomputable def qualiaDomain : DomainInstance where
 778  name := "Qualia (ULQ)"
 779  stateType := Unit  -- Placeholder for actual qualia state
 780  costEmbed := fun j => j  -- Identity embedding (J-cost IS qualia strain)
 781  monotone := fun _ _ h => h
 782
 783/-- **Ethics domain instance**: harm = externalized action surcharge -/
 784noncomputable def ethicsDomain : DomainInstance where
 785  name := "Ethics (DREAM)"
 786  stateType := Unit  -- Placeholder for moral state
 787  costEmbed := fun j => j  -- J-cost IS moral imbalance
 788  monotone := fun _ _ h => h
 789
 790/-- **Semantics domain instance**: defect = distance to structured set -/
 791noncomputable def semanticsDomain : DomainInstance where
 792  name := "Semantics (ULL)"
 793  stateType := Unit  -- Placeholder for semantic state
 794  costEmbed := fun j => j  -- J-cost IS semantic defect
 795  monotone := fun _ _ h => h
 796