Pareto Weak Dominance Preorder

Abstract

Five independently preordered gain coordinates induce a preorder of actions.

Theorem 1.1 (Weak Pareto dominance is reflexive and transitive).

$$\begin{array}{c}\forall Action,Information,Residual,Transfer,Cost,Risk:\mathrm{Type},\\ \mathrm{Preorder}\left(Information\right),\mathrm{Preorder}\left(Residual\right),\mathrm{Preorder}\left(Transfer\right),\mathrm{Preorder}\left(Cost\right),\mathrm{Preorder}\left(Risk\right),\\ value:Action\to \mathrm{GainVector}\left(Information,Residual,Transfer,Cost,Risk\right),\\ (\forall a:Action,\mathrm{ParetoWeak}\left(value,a,a\right))\wedge \\ (\forall a,b,c:Action,\mathrm{ParetoWeak}\left(value,a,b\right)\Rightarrow \mathrm{ParetoWeak}\left(value,b,c\right)\Rightarrow \mathrm{ParetoWeak}\left(value,a,c\right)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/DefinitionEscapeAdjudication/ParetoWeakPreorder.pareto_weak_reflexive_transitive (✓ std3). ∎

Source. Repository-derived.

Commentary.

Information, residual capture, and transfer are benefit coordinates; lifecycle cost and risk are burden coordinates. Weak dominance therefore reverses the comparison direction on the final two coordinates.

Coordinate reflexivity proves self-dominance. Coordinate transitivity composes two dominance comparisons, independently in all five heterogeneous preorder types.

References

• Truth anchor: D5/S3/ConceptDynamics/DefinitionEscapeAdjudication/ParetoWeakPreorder.pareto_weak_reflexive_transitive