Explicit Finite Pareto Quotient

Abstract

The symmetric weak-Pareto kernel on a finite carrier has explicit finite classes, a complete class enumeration, and the required empty and singleton laws.

Definition 1.1 (Explicit symmetric-kernel class).

$$\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:\mathrm{ParetoCarrier}\left(F\right),\\ \mathrm{paretoClass}\left(value,F,x\right)=\mathrm{filter}\left(\mathrm{carrierEnum}\left(F\right),\lambda y,\mathrm{ParetoEqOn}\left(value,F,y,x\right)\right).\end{array}$$

Formalization. D5/S3/ConceptDynamics/DefinitionEscapeAdjudication/FiniteParetoQuotient.paretoClass (✓ std3).

Source. Repository-derived.

Commentary.

The class is computed by filtering the attached finite carrier with the decidable symmetric weak-Pareto kernel.

Definition 1.2 (Finite image of all Pareto classes).

$$\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),\\ \mathrm{paretoClassImage}\left(value,F\right)=\mathrm{image}\left(\mathrm{carrierEnum}\left(F\right),\mathrm{paretoClass}\left(value,F\right)\right).\end{array}$$

Formalization. D5/S3/ConceptDynamics/DefinitionEscapeAdjudication/FiniteParetoQuotient.paretoClassImage (✓ std3).

Source. Repository-derived.

Commentary.

Taking the finite image removes duplicate classes while retaining an explicit representative-produced enumeration.

Definition 1.3 (Finite Pareto quotient carrier).

$$\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),\\ \mathrm{FiniteParetoQuotient}\left(value,F\right)=\{C:\mathrm{Finset}\left(\mathrm{ParetoCarrier}\left(F\right)\right)\mid C\in \mathrm{paretoClassImage}\left(value,F\right)\}.\end{array}$$

Formalization. D5/S3/ConceptDynamics/DefinitionEscapeAdjudication/FiniteParetoQuotient.FiniteParetoQuotient (✓ std3).

Source. Repository-derived.

Commentary.

The quotient carrier is the subtype of finite classes in the class image; it does not invoke Lean’s abstract Quotient type.

Definition 1.4 (Complete explicit quotient enumeration).

$$\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),\\ \mathrm{quotientEnum}\left(value,F\right)=\mathrm{attach}\left(\mathrm{paretoClassImage}\left(value,F\right)\right).\end{array}$$

Formalization. D5/S3/ConceptDynamics/DefinitionEscapeAdjudication/FiniteParetoQuotient.quotientEnum (✓ std3).

Source. Repository-derived.

Commentary.

Attaching image-membership proofs turns the class image into an enumeration whose elements already have the quotient subtype.

Definition 1.5 (Fintype from the explicit class image).

$$\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),\\ \mathrm{finiteParetoQuotientFintype}\left(value,F\right):\mathrm{Fintype}\left(\mathrm{FiniteParetoQuotient}\left(value,F\right)\right).\end{array}$$

Formalization. D5/S3/ConceptDynamics/DefinitionEscapeAdjudication/FiniteParetoQuotient.finiteParetoQuotientFintype (✓ std3).

Source. Repository-derived.

Commentary.

The class image supplies a finite type structure directly, including when the quotient is empty; no Nonempty premise is introduced.

Theorem 1.6 (Classes are exact and their enumeration is complete).

$$\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 x:\mathrm{ParetoCarrier}\left(F\right),x\in \mathrm{carrierEnum}\left(F\right))\wedge \\ (\forall x,y:\mathrm{ParetoCarrier}\left(F\right),y\in \mathrm{paretoClass}\left(value,F,x\right)⟺\mathrm{ParetoEqOn}\left(value,F,y,x\right))\wedge \\ (\forall x:\mathrm{ParetoCarrier}\left(F\right),x\in \mathrm{paretoClass}\left(value,F,x\right))\wedge \\ (\forall x,y:\mathrm{ParetoCarrier}\left(F\right),\mathrm{paretoClass}\left(value,F,x\right)=\mathrm{paretoClass}\left(value,F,y\right)⟺\mathrm{ParetoEqOn}\left(value,F,x,y\right))\wedge \\ (\forall C:\mathrm{FiniteParetoQuotient}\left(value,F\right),\mathrm{Nonempty}\left(\mathrm{val}\left(C\right)\right))\wedge \\ (\forall C:\mathrm{FiniteParetoQuotient}\left(value,F\right),\forall z:\mathrm{ParetoCarrier}\left(F\right),z\in \mathrm{val}\left(C\right)\Rightarrow \mathrm{paretoClass}\left(value,F,z\right)=\mathrm{val}\left(C\right))\wedge \\ (\forall C:\mathrm{FiniteParetoQuotient}\left(value,F\right),C\in \mathrm{quotientEnum}\left(value,F\right))\wedge \\ (F=\varnothing \Rightarrow \forall C:\mathrm{FiniteParetoQuotient}\left(value,F\right),False)\wedge \\ (\mathrm{card}\left(F\right)=1\Rightarrow \exists C:\mathrm{FiniteParetoQuotient}\left(value,F\right),\forall D:\mathrm{FiniteParetoQuotient}\left(value,F\right),D=C).\end{array}$$

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

Source. Repository-derived.

Commentary.

Every carrier element is enumerated; class membership is exactly ParetoEqOn; classes are reflexive, equal exactly for equivalent representatives, nonempty, stable under reclassification, and all occur in quotientEnum.

The same declaration verifies both boundary cases: an empty carrier has no quotient element, while a one-element carrier has exactly one quotient class.

References

• Truth anchor: D5/S3/ConceptDynamics/DefinitionEscapeAdjudication/FiniteParetoQuotient.FiniteParetoQuotient
• Truth anchor: D5/S3/ConceptDynamics/DefinitionEscapeAdjudication/FiniteParetoQuotient.finiteParetoQuotientFintype
• Truth anchor: D5/S3/ConceptDynamics/DefinitionEscapeAdjudication/FiniteParetoQuotient.finite_pareto_quotient_exact_and_complete
• Truth anchor: D5/S3/ConceptDynamics/DefinitionEscapeAdjudication/FiniteParetoQuotient.paretoClass
• Truth anchor: D5/S3/ConceptDynamics/DefinitionEscapeAdjudication/FiniteParetoQuotient.paretoClassImage
• Truth anchor: D5/S3/ConceptDynamics/DefinitionEscapeAdjudication/FiniteParetoQuotient.quotientEnum
• Dependency: D5/S3/ConceptDynamics/DefinitionEscapeAdjudication/ParetoEqOnDecidableEquivalence