ethicsCost
plain-language theorem explainer
The ethicsCost definition returns a natural number measuring distinction between two moral improvement steps, zero on equality and one otherwise. Researchers formalizing ethical structures inside Universal Forcing would cite it when building LogicRealization instances. The body is a direct conditional on equality of the underlying natural numbers.
Claim. For $a, b$ moral improvement steps (i.e., elements of $Nat$), define $ethicsCost(a,b) = 0$ if $a = b$ and $1$ otherwise.
background
MoralImprovementStep is defined as the type of natural numbers and serves as the carrier set counting morally meaningful improvement steps. The module supplies only the minimal identity and comparison structure required by Universal Forcing; it does not reconstruct any broader domain theory of ethics. This definition therefore supplies the compare operation for the subsequent ethicsRealization instance of LogicRealization.
proof idea
The definition is realized by a single conditional expression that branches on equality of the two natural-number arguments. No auxiliary lemmas are applied; the implementation is a primitive case distinction.
why it matters
ethicsCost supplies the cost function inside ethicsRealization, which instantiates LogicRealization with MoralImprovementStep as carrier and Nat as cost type. It is invoked directly by the self-equality and symmetry theorems for the cost function and thereby participates in the chain that embeds ethical counting into the Universal Forcing framework. The construction remains consistent with the Recognition Science pattern of realizing abstract structures through countable step comparisons.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.