Decidable Symmetric Pareto Kernel

Abstract

The symmetric kernel of weak Pareto dominance on a finite action carrier is a decidable equivalence relation.

Definition 1.1 (Five coordinate decisions decide the symmetric kernel).

$$\begin{array}{c}\forall Action,Information,Residual,Transfer,Cost,Risk:\mathrm{Type},\\ [\mathrm{DecidableEq}\left(Action\right)],[\mathrm{LE}\left(Information\right)],[\mathrm{LE}\left(Residual\right)],[\mathrm{LE}\left(Transfer\right)],[\mathrm{LE}\left(Cost\right)],[\mathrm{LE}\left(Risk\right)],\\ [\forall a,b:Information,\mathrm{Decidable}\left(a\le b\right)],[\forall a,b:Residual,\mathrm{Decidable}\left(a\le b\right)],[\forall a,b:Transfer,\mathrm{Decidable}\left(a\le b\right)],\\ [\forall a,b:Cost,\mathrm{Decidable}\left(a\le b\right)],[\forall a,b:Risk,\mathrm{Decidable}\left(a\le b\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{Decidable}\left(\mathrm{ParetoEqOn}\left(value,F,x,y\right)\right).\end{array}$$

Formalization. D5/S3/ConceptDynamics/DefinitionEscapeAdjudication/ParetoEqOnDecidableEquivalence.paretoEqOnDecidable (✓ std3).

Source. Repository-derived.

Commentary.

The decision procedure unfolds both weak-dominance directions and combines the ten resulting coordinate comparisons. It requires no enumeration of the ambient action or coordinate types.

Theorem 1.2 (The symmetric Pareto kernel obeys the three equivalence laws).

$$\begin{array}{c}\forall Action,Information,Residual,Transfer,Cost,Risk:\mathrm{Type},\\ [\mathrm{DecidableEq}\left(Action\right)],[\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),F:\mathrm{Finset}\left(Action\right),\\ (\forall x:\mathrm{ParetoCarrier}\left(F\right),\mathrm{ParetoEqOn}\left(value,F,x,x\right))\wedge \\ (\forall x,y:\mathrm{ParetoCarrier}\left(F\right),\mathrm{ParetoEqOn}\left(value,F,x,y\right)\Rightarrow \mathrm{ParetoEqOn}\left(value,F,y,x\right))\wedge \\ (\forall x,y,z:\mathrm{ParetoCarrier}\left(F\right),\mathrm{ParetoEqOn}\left(value,F,x,y\right)\Rightarrow \mathrm{ParetoEqOn}\left(value,F,y,z\right)\Rightarrow \mathrm{ParetoEqOn}\left(value,F,x,z\right)).\end{array}$$

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

Source. Repository-derived.

Commentary.

The carrier is the subtype selected by the finite action set. ParetoEqOn is defined as weak dominance in both directions; it is not defined by vector equality or an external label.

Reflexivity and transitivity reuse the frozen five-coordinate weak Pareto preorder theorem. Symmetry swaps the two kernel conjuncts; the preceding definition supplies the independent decision clause.

References

• Truth anchor: D5/S3/ConceptDynamics/DefinitionEscapeAdjudication/ParetoEqOnDecidableEquivalence.paretoEqOnDecidable
• Truth anchor: D5/S3/ConceptDynamics/DefinitionEscapeAdjudication/ParetoEqOnDecidableEquivalence.pareto_eq_on_equivalence_laws
• Dependency: D5/S3/ConceptDynamics/DefinitionEscapeAdjudication/ParetoWeakPreorder