semanticsDomain
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.