ethicsDomain
plain-language theorem explainer
EthicsDomain instantiates the DomainInstance structure for the ethics domain by setting the state space to Unit and identifying the cost embedding with the identity map on J-costs. Researchers extending Recognition Science to normative or ethical measurements would cite this construction when applying the algebra to moral imbalance. The definition proceeds by direct record construction matching the four fields of DomainInstance.
Claim. The ethics domain instance is the structure with name ``Ethics (DREAM)'', state space $Unit$, cost embedding the identity map $id:ℝ→ℝ$, and monotonicity the identity on inequalities: $∀a,b:ℝ, a≤b → id(a)≤id(b)$.
background
A DomainInstance is a functor from the Recognition Algebra (RecAlg) to a specific domain. It supplies a name string, a stateType, a costEmbed map from reals to reals, and a monotonicity proof that the embedding preserves order. This module defines several such instances for domains including ethics, qualia, and semantics. Upstream results include the defect functional, which equals J for positive arguments, and cost definitions in observer forcing and multiplicative recognizers that are likewise built from J-cost.
proof idea
The definition directly constructs the DomainInstance record by supplying the four required fields: the name string, the Unit state type, the identity function as costEmbed, and the trivial proof that the identity preserves inequalities.
why it matters
This definition supplies the ethics domain instance within the RecognitionCategory algebra, allowing the framework to extend the J-cost and defect measures to ethical contexts where harm is the externalized surcharge. It sits alongside sibling domain instances and supports future applications of the Recognition Composition Law to normative structures. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.