DomainInstance
plain-language theorem explainer
DomainInstance structures a functor from the canonical Recognition Algebra to a concrete domain via a name, state type, monotone cost embedding from reals to reals, and the ordering preservation axiom. Algebraists constructing domain-specific instances cite it when building qualia, ethics, or semantics algebras from the base J-cost structure. The definition is a direct structure declaration with no lemmas or tactics required.
Claim. A domain instance consists of a string name $n$, a state space type $S$, a cost embedding $c : ℝ → ℝ$, and a monotonicity condition asserting that $∀ a,b ∈ ℝ, a ≤ b → c(a) ≤ c(b)$.
background
The RecognitionCategory module assembles a category over the Recognition Algebra (RecAlg) from CostAlgebra, PhiRing, LedgerAlgebra, and OctaveAlgebra. DomainInstance supplies the functor interface that maps the algebra's J-cost to domain-specific measurements while preserving order. Upstream results supply the necessary cost primitives: MultiplicativeRecognizerL4.cost derives the J-cost on positive ratios, ObserverForcing.cost equates recognition cost to J-cost, and ArithmeticFromLogic.embed maps logical generators into the reals.
proof idea
Direct structure definition introducing the four fields name, stateType, costEmbed, and monotone. No lemmas are invoked and no tactics are used.
why it matters
DomainInstance supplies the uniform interface that produces the concrete domain algebras ethicsDomain, qualiaDomain, and semanticsDomain. It realizes the functorial step from the canonical Recognition Algebra to domain-specific cost interpretations, linking directly to the J-cost uniqueness (T5) and the Recognition Composition Law. The construction leaves open the choice of concrete stateType beyond the Unit placeholder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.