moral_ordering_trans
plain-language theorem explainer
Transitivity of the moral preference relation on ethical actions follows from the transitivity of their underlying defect measures. A researcher deriving objective ethics from Recognition Science would cite this when establishing that the preference relation is a preorder compatible with J-cost minimization. The proof is a direct one-line application of the arithmetic transitivity lemma to the moral costs.
Claim. For ethical actions $a$, $b$, $c$, if the moral cost of $a$ is at most the moral cost of $b$ and the moral cost of $b$ is at most the moral cost of $c$, then the moral cost of $a$ is at most the moral cost of $c$.
background
The module PH-004 derives objective morality from the Recognition Science cost structure. An ethical action is a structure with before and after real configurations, each positive, that maps one state to another and is evaluated by its effect on ledger defect. MorallyBetter holds between two actions precisely when the moral cost (defect of the resulting state) of the first is at most that of the second. This identification of lower defect with ethical preference dissolves Hume's guillotine by treating goodness as stability under the J-cost forced by the Recognition Composition Law.
proof idea
The proof is a one-line wrapper that applies the transitivity lemma for the ordering on LogicNat (from ArithmeticFromLogic) directly to the moral costs of the three actions.
why it matters
This result supplies the transitivity half of the preorder on ethical actions, pairing with the reflexivity theorem in the same module to underwrite the claim that moral improvement is always possible until the ideal (zero-defect) state is reached. It supports the broader PH-004 resolution of the is-ought problem and the DREAM theorem on virtue-generating transformations, all resting on the J-cost uniqueness (T5) and the eight-tick octave structure. No open scaffolding remains for this specific ordering property.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.