Symmetric Pareto Kernel and Vector Equality

Abstract

Under coordinate partial orders, the symmetric Pareto kernel is equality of gain vectors.

Theorem 1.1 (The symmetric kernel is exactly gain-vector equality).

$$\begin{array}{c}\forall Action,Information,Residual,Transfer,Cost,Risk:\mathrm{Type},\\ [\mathrm{DecidableEq}\left(Action\right)],\mathrm{PartialOrder}\left(Information\right),\mathrm{PartialOrder}\left(Residual\right),\mathrm{PartialOrder}\left(Transfer\right),\\ \mathrm{PartialOrder}\left(Cost\right),\mathrm{PartialOrder}\left(Risk\right),\\ value:Action\to \mathrm{GainVector}\left(Information,Residual,Transfer,Cost,Risk\right),F:\mathrm{Finset}\left(Action\right),\\ x,y:\mathrm{ParetoCarrier}\left(F\right),\\ \mathrm{ParetoEqOn}\left(value,F,x,y\right)⟺value(x.1)=value(y.1).\end{array}$$

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

Source. Repository-derived.

Commentary.

Each benefit coordinate is compared in its given direction, while lifecycle cost and risk use the reversed burden direction inherited from weak Pareto dominance.

Antisymmetry in all five partial orders turns the two independent dominance directions into equality of every coordinate; the converse is coordinate reflexivity.

References

• Truth anchor: D5/S3/ConceptDynamics/DefinitionEscapeAdjudication/ParetoEqOnVectorEquality.pareto_eq_on_iff_vector_eq
• Dependency: D5/S3/ConceptDynamics/DefinitionEscapeAdjudication/ParetoEqOnDecidableEquivalence