semanticsDomain
The semanticsDomain definition supplies a concrete DomainInstance for semantic structures in the Recognition Algebra, with singleton state space and identity embedding of J-costs. Researchers extending the canonical RecAlg to domain algebras cite this when instantiating semantics. The construction is a direct record definition that satisfies the monotone requirement by reflexivity on the identity map.
claimThe semantics domain instance is the structure with name ``Semantics (ULL)'', state space the singleton set, cost embedding the identity map on the reals, and monotonicity holding for all pairs of reals.
background
A DomainInstance is a structure with four fields: a name string, a state type, a cost embedding function from reals to reals, and a proof that the embedding is monotone. This definition sits in the RecognitionCategory module, which builds domain algebras by applying functors to the canonical Recognition Algebra. Upstream results include the defect functional (equal to J for positive x) and cost definitions from multiplicative recognizers and observer forcing, all of which reduce to J-cost.
proof idea
This is a direct record definition that populates the four fields of DomainInstance. The name field receives the string literal, stateType receives Unit, costEmbed receives the identity function, and monotone receives the reflexivity proof on inequalities.
why it matters in Recognition Science
This supplies the semantics instantiation of DomainInstance, enabling the Recognition framework to treat semantic defects as distances to structured sets. It forms part of the domain algebra construction in RecognitionCategory and aligns with the monotone invariance principle that preserves argmin across different domain scales.
scope and limits
- Does not define theorems or derived properties of the semantics domain.
- Does not specify concrete semantic structures or their interactions.
- Does not connect to empirical programs or specific data.
- Does not address invariance proofs or forcing chain steps.
formal statement (Lean)
791noncomputable def semanticsDomain : DomainInstance where
792 name := "Semantics (ULL)"
proof body
Definition body.
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. -/