semanticsDomain

formal source

 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
 797/-! ## §4. The Invariance Principle -/
 798
 799/-- **Monotone invariance**: Strictly monotone transforms preserve argmin.
 800    This is the key principle that allows different domains to measure
 801    the same underlying structure with different scales. -/
 802theorem monotone_preserves_argmin {α : Type} [Fintype α] [Nonempty α]
 803    (f : α → ℝ) (g : ℝ → ℝ) (hg : StrictMono g)
 804    (x₀ : α) (hmin : ∀ x, f x₀ ≤ f x) :
 805    ∀ x, g (f x₀) ≤ g (f x) := by
 806  intro x
 807  exact hg.monotone (hmin x)
 808
 809/-! ## §5. Summary -/
 810
 811/-- **RECOGNITION CATEGORY CERTIFICATE**
 812
 813    1. Category RecAlg defined (objects, morphisms, id, comp) ✓
 814    2. Composition is associative ✓
 815    3. Identity is neutral ✓
 816    4. Initial object exists (canonical J) ✓
 817    5. Morphism from initial to calibrated objects ✓
 818    6. Domain instances defined (qualia, ethics, semantics) ✓
 819    7. Monotone invariance principle ✓
 820
 821    This provides the categorical foundation for RS: