Decidable Weak Pareto Order on the Finite Quotient

Abstract

Existential weak Pareto dominance on explicit finite classes is representative-independent, decidable by a finite scan, and a partial order.

Definition 1.1 (Existential representative relation).

$$\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),\\ C,D:\mathrm{FiniteParetoQuotient}\left(value,F\right),\\ \mathrm{QuotientParetoWeak}\left(value,F,C,D\right)⟺\exists x:\mathrm{ParetoCarrier}\left(F\right),x\in \mathrm{val}\left(C\right)\wedge \exists y:\mathrm{ParetoCarrier}\left(F\right),y\in \mathrm{val}\left(D\right)\wedge \mathrm{ParetoWeakOn}\left(value,F,x,y\right).\end{array}$$

Formalization. D5/S3/ConceptDynamics/DefinitionEscapeAdjudication/QuotientParetoWeakOrder.QuotientParetoWeak (✓ std3).

Source. Repository-derived.

Commentary.

A class weakly dominates another when one representative pair satisfies the existing carrier-level ParetoWeakOn relation.

Definition 1.2 (Finite product scan).

$$\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),\\ C,D:\mathrm{FiniteParetoQuotient}\left(value,F\right),\\ \mathrm{quotientParetoWeakScan}\left(value,F,C,D\right)=\mathrm{decide}\left(\mathrm{Nonempty}\left(\mathrm{filter}\left(\mathrm{product}\left(\mathrm{val}\left(C\right),\mathrm{val}\left(D\right)\right),\lambda p,\mathrm{ParetoWeakOn}\left(value,F,\mathrm{fst}\left(p\right),\mathrm{snd}\left(p\right)\right)\right)\right)\right).\end{array}$$

Formalization. D5/S3/ConceptDynamics/DefinitionEscapeAdjudication/QuotientParetoWeakOrder.quotientParetoWeakScan (✓ std3).

Source. Repository-derived.

Commentary.

The decision procedure forms the finite product of the two explicit classes, filters it by ParetoWeakOn, and decides nonemptiness.

Definition 1.3 (Finite-scan decidability).

$$\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)],\\ [\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),\\ C,D:\mathrm{FiniteParetoQuotient}\left(value,F\right),\\ \mathrm{quotientParetoWeakDecidable}\left(value,F,C,D\right):\mathrm{Decidable}\left(\mathrm{QuotientParetoWeak}\left(value,F,C,D\right)\right).\end{array}$$

Formalization. D5/S3/ConceptDynamics/DefinitionEscapeAdjudication/QuotientParetoWeakOrder.quotientParetoWeakDecidable (✓ std3).

Source. Repository-derived.

Commentary.

Correctness of the product scan supplies a Decidable term for the quotient relation.

Theorem 1.4 (Representative-independent decidable partial order).

$$\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)],\\ [\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),\\ (\forall C,D:\mathrm{FiniteParetoQuotient}\left(value,F\right),\mathrm{QuotientParetoWeak}\left(value,F,C,D\right)⟺\forall x:\mathrm{ParetoCarrier}\left(F\right),x\in \mathrm{val}\left(C\right)\Rightarrow \forall y:\mathrm{ParetoCarrier}\left(F\right),y\in \mathrm{val}\left(D\right)\Rightarrow \mathrm{ParetoWeakOn}\left(value,F,x,y\right))\wedge \\ (\forall C,D:\mathrm{FiniteParetoQuotient}\left(value,F\right),\mathrm{quotientParetoWeakScan}\left(value,F,C,D\right)=true⟺\mathrm{QuotientParetoWeak}\left(value,F,C,D\right))\wedge \\ (\forall C,D:\mathrm{FiniteParetoQuotient}\left(value,F\right),\mathrm{Nonempty}\left(\mathrm{Decidable}\left(\mathrm{QuotientParetoWeak}\left(value,F,C,D\right)\right)\right))\wedge \\ (\forall C:\mathrm{FiniteParetoQuotient}\left(value,F\right),\mathrm{QuotientParetoWeak}\left(value,F,C,C\right))\wedge \\ (\forall C,D,E:\mathrm{FiniteParetoQuotient}\left(value,F\right),\mathrm{QuotientParetoWeak}\left(value,F,C,D\right)\Rightarrow \mathrm{QuotientParetoWeak}\left(value,F,D,E\right)\Rightarrow \mathrm{QuotientParetoWeak}\left(value,F,C,E\right))\wedge \\ (\forall C,D:\mathrm{FiniteParetoQuotient}\left(value,F\right),\mathrm{QuotientParetoWeak}\left(value,F,C,D\right)\Rightarrow \mathrm{QuotientParetoWeak}\left(value,F,D,C\right)\Rightarrow C=D)\wedge \\ (F=\varnothing \Rightarrow \forall C,D:\mathrm{FiniteParetoQuotient}\left(value,F\right),\mathrm{QuotientParetoWeak}\left(value,F,C,D\right)).\end{array}$$

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

Source. Repository-derived.

Commentary.

One dominating representative pair implies that every pair dominates: members of one explicit class are related by the symmetric Pareto kernel, so the frozen weak-preorder laws transport the comparison between representatives.

The same transport proves transitivity and antisymmetry. Reflexivity uses the proved nonemptiness of every quotient class. If the action carrier is empty, the quotient has no element and the quantified relation statement is vacuous; no artificial element is introduced.

References

• Truth anchor: D5/S3/ConceptDynamics/DefinitionEscapeAdjudication/QuotientParetoWeakOrder.QuotientParetoWeak
• Truth anchor: D5/S3/ConceptDynamics/DefinitionEscapeAdjudication/QuotientParetoWeakOrder.quotientParetoWeakDecidable
• Truth anchor: D5/S3/ConceptDynamics/DefinitionEscapeAdjudication/QuotientParetoWeakOrder.quotientParetoWeakScan
• Truth anchor: D5/S3/ConceptDynamics/DefinitionEscapeAdjudication/QuotientParetoWeakOrder.quotient_pareto_weak_finite_decidable_partial_order
• Dependency: D5/S3/ConceptDynamics/DefinitionEscapeAdjudication/FiniteParetoQuotient