prefer_trans
plain-language theorem explainer
Transitivity holds for ethical preferences under a cost model: if action a is at least as good as b and b as good as c, then a is at least as good as c. Modelers of ethical decision systems or preference orders cite this to equip action sets with preorder structure. The proof is a one-line term reduction that unfolds Prefer to the cost inequality and invokes transitivity of ≤ on the reals.
Claim. Let $M$ be a cost model over actions of type $A$. If $a ≼ b$ and $b ≼ c$ under $M$, then $a ≼ c$, where $a ≼ b$ means cost$_M(a) ≤$ cost$_M(b)$.
background
In the Ethics.CostModel module a CostModel is a structure supplying a cost function from actions to nonnegative reals together with the nonnegativity axiom. The relation Prefer M a b is defined exactly as cost(a) ≤ cost(b), with lower cost interpreted as better; the infix ≼ is introduced for this relation. The module imports ArithmeticFromLogic for the underlying order on reals and draws on upstream preference definitions such as the negation of J-cost in SymmetryGroupPreference.
proof idea
The proof is a term-mode one-liner. It applies dsimp to unfold Prefer in the two hypotheses and the goal, reducing everything to inequalities on the cost function, then invokes exact le_trans from the arithmetic foundations to obtain the conclusion.
why it matters
This lemma supplies the transitivity axiom required by the Preorder instance declared immediately below, which sets le := Prefer M and wires prefer_trans into le_trans. It thereby enables monotonicity and subadditivity arguments in the Composable structure. Within the Recognition framework the result furnishes the order-theoretic substrate for cost-based ethics, aligning with J-cost minimization from aesthetics and the preference ordering implicit in the phi-ladder and forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.