Primitive sets and the slack-vector form of Scarf's lemma

This file reformulates rooms and doors of an IndexedLOrder in terms of primitive sets over the enlarged good set T ⊕ I, the "slack-vector" language of Scarf's algorithm. It relates the room/door combinatorics developed in Scarf to this primitive-set picture used by the path-following termination argument.

@[reducible, inline]

abbrev IndexedLOrder.ExtendedGoods (T : Type u_3) (I : Type u_4) : Type (max u_3 u_4)

The abstract enlargement T ∪ I used for Scarf's slack-vector language.

Equations

• IndexedLOrder.ExtendedGoods T I = (T ⊕ I)

def IndexedLOrder.toPrimitiveSet {T : Type u_1} {I : Type u_2} [Fintype I] [DecidableEq T] [DecidableEq I] (σ : Finset T) (C : Finset I) : Finset (ExtendedGoods T I)

Turn a room (σ, C) into the corresponding primitive set σ ∪ (I \ C).

Equations

• IndexedLOrder.toPrimitiveSet σ C = Finset.image Sum.inl σ ∪ Finset.image Sum.inr (Finset.univ \ C)

def IndexedLOrder.toAlmostPrimitive {T : Type u_1} {I : Type u_2} [Fintype I] [DecidableEq T] [DecidableEq I] (τ : Finset T) (D : Finset I) : Finset (ExtendedGoods T I)

Turn a door (τ, D) into the corresponding almost primitive set τ ∪ (I \ D).

Equations

• IndexedLOrder.toAlmostPrimitive τ D = IndexedLOrder.toPrimitiveSet τ D

def IndexedLOrder.fromGoods {T : Type u_1} {I : Type u_2} [Fintype T] [DecidableEq T] [DecidableEq I] (X : Finset (ExtendedGoods T I)) : Finset T

The goods part of a subset of T ∪ I.

Equations

• IndexedLOrder.fromGoods X = {t : T | Sum.inl t ∈ X}

def IndexedLOrder.fromMissing {T : Type u_1} {I : Type u_2} [Fintype I] [DecidableEq T] [DecidableEq I] (X : Finset (ExtendedGoods T I)) : Finset I

The indices whose slack vectors are missing from a subset of T ∪ I.

Equations

• IndexedLOrder.fromMissing X = {i : I | Sum.inr i ∉ X}

def IndexedLOrder.associatedCell {T : Type u_1} {I : Type u_2} [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] (X : Finset (ExtendedGoods T I)) : GiCell T I

The room/door cell associated to a subset of T ∪ I.

Equations

• IndexedLOrder.associatedCell X = (IndexedLOrder.fromGoods X, IndexedLOrder.fromMissing X)

@[simp]

theorem IndexedLOrder.associatedCell_fst {T : Type u_1} {I : Type u_2} [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] (X : Finset (ExtendedGoods T I)) : (associatedCell X).1 = fromGoods X

@[simp]

theorem IndexedLOrder.associatedCell_snd {T : Type u_1} {I : Type u_2} [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] (X : Finset (ExtendedGoods T I)) : (associatedCell X).2 = fromMissing X

@[simp]

theorem IndexedLOrder.mem_toPrimitiveSet_inl {T : Type u_1} {I : Type u_2} [Fintype I] [DecidableEq T] [DecidableEq I] {σ : Finset T} {C : Finset I} {t : T} : Sum.inl t ∈ toPrimitiveSet σ C ↔ t ∈ σ

@[simp]

theorem IndexedLOrder.mem_toPrimitiveSet_inr {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype I] [DecidableEq T] [DecidableEq I] {σ : Finset T} {C : Finset I} {i : I} : Sum.inr i ∈ toPrimitiveSet σ C ↔ i ∉ C

@[simp]

theorem IndexedLOrder.mem_toAlmostPrimitive_inl {T : Type u_1} {I : Type u_2} [Fintype I] [DecidableEq T] [DecidableEq I] {τ : Finset T} {D : Finset I} {t : T} : Sum.inl t ∈ toAlmostPrimitive τ D ↔ t ∈ τ

@[simp]

theorem IndexedLOrder.mem_toAlmostPrimitive_inr {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype I] [DecidableEq T] [DecidableEq I] {τ : Finset T} {D : Finset I} {i : I} : Sum.inr i ∈ toAlmostPrimitive τ D ↔ i ∉ D

@[simp]

theorem IndexedLOrder.mem_fromGoods {T : Type u_1} {I : Type u_2} [Fintype T] [DecidableEq T] [DecidableEq I] {X : Finset (ExtendedGoods T I)} {t : T} : t ∈ fromGoods X ↔ Sum.inl t ∈ X

@[simp]

theorem IndexedLOrder.mem_fromMissing {T : Type u_1} {I : Type u_2} [Fintype I] [DecidableEq T] [DecidableEq I] {X : Finset (ExtendedGoods T I)} {i : I} : i ∈ fromMissing X ↔ Sum.inr i ∉ X

@[simp]

theorem IndexedLOrder.fromGoods_toPrimitiveSet {T : Type u_1} {I : Type u_2} [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] (σ : Finset T) (C : Finset I) : fromGoods (toPrimitiveSet σ C) = σ

@[simp]

theorem IndexedLOrder.fromMissing_toPrimitiveSet {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype I] [DecidableEq T] [DecidableEq I] (σ : Finset T) (C : Finset I) : fromMissing (toPrimitiveSet σ C) = C

@[simp]

theorem IndexedLOrder.fromGoods_toAlmostPrimitive {T : Type u_1} {I : Type u_2} [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] (τ : Finset T) (D : Finset I) : fromGoods (toAlmostPrimitive τ D) = τ

@[simp]

theorem IndexedLOrder.fromMissing_toAlmostPrimitive {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype I] [DecidableEq T] [DecidableEq I] (τ : Finset T) (D : Finset I) : fromMissing (toAlmostPrimitive τ D) = D

theorem IndexedLOrder.goods_slacks_disjoint {T : Type u_1} {I : Type u_2} [Fintype I] [DecidableEq T] [DecidableEq I] (σ : Finset T) (C : Finset I) : Disjoint (Finset.image Sum.inl σ) (Finset.image Sum.inr (Finset.univ \ C))

theorem IndexedLOrder.card_toPrimitiveSet {T : Type u_1} {I : Type u_2} [Fintype I] [DecidableEq T] [DecidableEq I] (σ : Finset T) (C : Finset I) : (toPrimitiveSet σ C).card = σ.card + (Finset.univ \ C).card

theorem IndexedLOrder.eq_toPrimitive_from_parts {T : Type u_1} {I : Type u_2} [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] (X : Finset (ExtendedGoods T I)) : X = toPrimitiveSet (fromGoods X) (fromMissing X)

theorem IndexedLOrder.eq_toAlmost_from_parts {T : Type u_1} {I : Type u_2} [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] (X : Finset (ExtendedGoods T I)) : X = toAlmostPrimitive (fromGoods X) (fromMissing X)

theorem IndexedLOrder.card_toPrimitiveSet_of_room {T : Type u_1} {I : Type u_2} [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {σ : Finset T} {C : Finset I} (hRoom : isRoom σ C) : (toPrimitiveSet σ C).card = Fintype.card I

theorem IndexedLOrder.card_toAlmostPrimitive_of_door {T : Type u_1} {I : Type u_2} [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {τ : Finset T} {D : Finset I} (hDoor : isDoor τ D) : (toAlmostPrimitive τ D).card + 1 = Fintype.card I

theorem IndexedLOrder.exists_insert_eq_of_subset_card_eq_succ {α : Type u_3} [DecidableEq α] {s t : Finset α} (hsub : s ⊆ t) (hcard : t.card = s.card + 1) : ∃ x ∉ s, insert x s = t

def IndexedLOrder.isRoomPrimitive {T : Type u_1} {I : Type u_2} [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] (X : Finset (ExtendedGoods T I)) : Prop

Primitive sets stated through the equivalent room language.

Equations

• IndexedLOrder.isRoomPrimitive X = ∃ (σ : Finset T) (C : Finset I), IndexedLOrder.isRoom σ C ∧ X = IndexedLOrder.toPrimitiveSet σ C

def IndexedLOrder.isPrimitive {T : Type u_1} {I : Type u_2} [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] (X : Finset (ExtendedGoods T I)) : Prop

Scarf primitive sets in the paper's native dominance form, using the characterization X primitive iff X ∩ T is dominant with respect to the missing slack indices.

Equations

• IndexedLOrder.isPrimitive X = (X.card = Fintype.card I ∧ IndexedLOrder.isDominant (IndexedLOrder.fromGoods X) (IndexedLOrder.fromMissing X))

@[reducible, inline]

abbrev IndexedLOrder.isPrimitiveNative {T : Type u_1} {I : Type u_2} [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] (X : Finset (ExtendedGoods T I)) : Prop

Backwards-compatible name for the paper's native primitive definition.

Equations

• IndexedLOrder.isPrimitiveNative X = IndexedLOrder.isPrimitive X

def IndexedLOrder.isAlmostPrimitive {T : Type u_1} {I : Type u_2} [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] (Y : Finset (ExtendedGoods T I)) : Prop

Almost primitive sets, stated through the equivalent door language.

Equations

• IndexedLOrder.isAlmostPrimitive Y = ∃ (τ : Finset T) (D : Finset I) (σ : Finset T) (C : Finset I), IndexedLOrder.isDoorof τ D σ C ∧ Y = IndexedLOrder.toAlmostPrimitive τ D

def IndexedLOrder.isAlmostPrimitiveNative {T : Type u_1} {I : Type u_2} [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] (Y : Finset (ExtendedGoods T I)) : Prop

Almost primitive sets in the paper's native form: an (n-1)-face contained in a primitive set.

Equations

• IndexedLOrder.isAlmostPrimitiveNative Y = (Y.card + 1 = Fintype.card I ∧ ∃ (X : Finset (IndexedLOrder.ExtendedGoods T I)), IndexedLOrder.isPrimitiveNative X ∧ Y ⊆ X)

theorem IndexedLOrder.room_to_roomPrimitive {T : Type u_1} {I : Type u_2} [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {σ : Finset T} {C : Finset I} (h : isRoom σ C) : isRoomPrimitive (toPrimitiveSet σ C)

A room gives the equivalent room-language primitive set.

theorem IndexedLOrder.primitive_to_room {T : Type u_1} {I : Type u_2} [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {X : Finset (ExtendedGoods T I)} (h : isPrimitive X) : isRoom (fromGoods X) (fromMissing X)

Extract the room corresponding to a primitive set.

theorem IndexedLOrder.room_to_primitive {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {σ : Finset T} {C : Finset I} (h : isRoom σ C) : isPrimitive (toPrimitiveSet σ C)

A room gives a primitive set in the paper's native sense.

theorem IndexedLOrder.isPrimitive_toPrimitiveSet_iff_room {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {σ : Finset T} {C : Finset I} : isPrimitive (toPrimitiveSet σ C) ↔ isRoom σ C

For sets written in room coordinates, being primitive is exactly being a room. This is the cardinality condition implicit in the paper's comparison between dominant sets and primitive sets.

theorem IndexedLOrder.primitive_eq_toPrimitive_from_parts {T : Type u_1} {I : Type u_2} [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {X : Finset (ExtendedGoods T I)} (_h : isPrimitive X) : X = toPrimitiveSet (fromGoods X) (fromMissing X)

theorem IndexedLOrder.primitive_from_parts {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {X : Finset (ExtendedGoods T I)} (h : isPrimitive X) : isPrimitive (toPrimitiveSet (fromGoods X) (fromMissing X))

A room recovered from a primitive set is again primitive.

theorem IndexedLOrder.primitive_to_nativePrimitive {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {X : Finset (ExtendedGoods T I)} (h : isRoomPrimitive X) : isPrimitiveNative X

theorem IndexedLOrder.nativePrimitive_to_primitive {T : Type u_1} {I : Type u_2} [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {X : Finset (ExtendedGoods T I)} (h : isPrimitiveNative X) : isRoomPrimitive X

theorem IndexedLOrder.isPrimitive_iff_native {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {X : Finset (ExtendedGoods T I)} : isRoomPrimitive X ↔ isPrimitiveNative X

theorem IndexedLOrder.door_to_almostPrimitive {T : Type u_1} {I : Type u_2} [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {τ σ : Finset T} {D C : Finset I} (h : isDoorof τ D σ C) : isAlmostPrimitive (toAlmostPrimitive τ D)

A door of a room gives an almost primitive set.

theorem IndexedLOrder.almostPrimitive_to_door {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {Y : Finset (ExtendedGoods T I)} (h : isAlmostPrimitive Y) : isDoor (fromGoods Y) (fromMissing Y)

Recover the door represented by an almost primitive set.

theorem IndexedLOrder.almostPrimitive_incident_room {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {Y : Finset (ExtendedGoods T I)} (h : isAlmostPrimitive Y) : ∃ (σ : Finset T) (C : Finset I), isDoorof (fromGoods Y) (fromMissing Y) σ C

Recover a room incident to an almost primitive set.

theorem IndexedLOrder.doorof_toAlmost_subset_toPrimitive {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {τ σ : Finset T} {D C : Finset I} (h : isDoorof τ D σ C) : toAlmostPrimitive τ D ⊆ toPrimitiveSet σ C

Incidence of doors and rooms becomes subset inclusion of the corresponding sets.

theorem IndexedLOrder.doorof_iff_subset_primitive {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {τ σ : Finset T} {D C : Finset I} : isDoorof τ D σ C → isRoom σ C ∧ isAlmostPrimitive (toAlmostPrimitive τ D) ∧ isPrimitive (toPrimitiveSet σ C) ∧ toAlmostPrimitive τ D ⊆ toPrimitiveSet σ C

A useful packaged form of the door/primitive-set incidence correspondence.

theorem IndexedLOrder.almostPrimitive_eq_toAlmost_from_parts {T : Type u_1} {I : Type u_2} [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {Y : Finset (ExtendedGoods T I)} (_h : isAlmostPrimitive Y) : Y = toAlmostPrimitive (fromGoods Y) (fromMissing Y)

theorem IndexedLOrder.subset_toPrimitive_toAlmost_doorof {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {τ σ : Finset T} {D C : Finset I} (hDoor : isDoor τ D) (hRoom : isRoom σ C) (hsub : toAlmostPrimitive τ D ⊆ toPrimitiveSet σ C) : isDoorof τ D σ C

theorem IndexedLOrder.nativeAlmostPrimitive_to_almostPrimitive {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {Y : Finset (ExtendedGoods T I)} (h : isAlmostPrimitiveNative Y) : isAlmostPrimitive Y

theorem IndexedLOrder.almostPrimitive_to_nativeAlmostPrimitive {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {Y : Finset (ExtendedGoods T I)} (h : isAlmostPrimitive Y) : isAlmostPrimitiveNative Y

theorem IndexedLOrder.isAlmostPrimitive_iff_native {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {Y : Finset (ExtendedGoods T I)} : isAlmostPrimitive Y ↔ isAlmostPrimitiveNative Y

theorem IndexedLOrder.internal_almostPrimitive_two_incident_primitives {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {Y : Finset (ExtendedGoods T I)} (hY : isAlmostPrimitive Y) (hInternal : (fromGoods Y).Nonempty) : ∃ (X₁ : Finset (ExtendedGoods T I)) (X₂ : Finset (ExtendedGoods T I)), X₁ ≠ X₂ ∧ isPrimitive X₁ ∧ isPrimitive X₂ ∧ Y ⊆ X₁ ∧ Y ⊆ X₂

Scarf's main lemma for internal almost primitive sets, in the room/door language: an internal almost primitive face is contained in two distinct primitive sets.

theorem IndexedLOrder.internal_almostPrimitive_exactly_two_incident_primitives {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {Y : Finset (ExtendedGoods T I)} (hY : isAlmostPrimitive Y) (hInternal : (fromGoods Y).Nonempty) : ∃ (X₁ : Finset (ExtendedGoods T I)) (X₂ : Finset (ExtendedGoods T I)), X₁ ≠ X₂ ∧ isPrimitive X₁ ∧ isPrimitive X₂ ∧ Y ⊆ X₁ ∧ Y ⊆ X₂ ∧ ∀ (X : Finset (ExtendedGoods T I)), isPrimitive X → Y ⊆ X → X = X₁ ∨ X = X₂

theorem IndexedLOrder.native_internal_almostPrimitive_exactly_two_incident_primitives {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {Y : Finset (ExtendedGoods T I)} (hY : isAlmostPrimitiveNative Y) (hInternal : (fromGoods Y).Nonempty) : ∃ (X₁ : Finset (ExtendedGoods T I)) (X₂ : Finset (ExtendedGoods T I)), X₁ ≠ X₂ ∧ isPrimitiveNative X₁ ∧ isPrimitiveNative X₂ ∧ Y ⊆ X₁ ∧ Y ⊆ X₂ ∧ ∀ (X : Finset (ExtendedGoods T I)), isPrimitiveNative X → Y ⊆ X → X = X₁ ∨ X = X₂

theorem IndexedLOrder.native_primitive_erase_mainLemma {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {X : Finset (ExtendedGoods T I)} (hX : isPrimitiveNative X) {x : ExtendedGoods T I} (hx : x ∈ X) : ¬(fromGoods (X.erase x)).Nonempty ∨ ∃! X' : Finset (ExtendedGoods T I), isPrimitiveNative X' ∧ X.erase x ⊆ X' ∧ X' ≠ X

Native Scarf main lemma in the "remove one point" form: after removing a point from a primitive set, either the resulting face lies in the slack boundary, or there is a unique other primitive set containing that face.

theorem IndexedLOrder.native_primitive_erase_replacement_mainLemma {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {X : Finset (ExtendedGoods T I)} (hX : isPrimitiveNative X) {x : ExtendedGoods T I} (hx : x ∈ X) : ¬(fromGoods (X.erase x)).Nonempty ∨ ∃! y : ExtendedGoods T I, y ∉ X ∧ isPrimitiveNative (insert y (X.erase x))

Scarf's main lemma in the paper's replacement form: after removing x from a primitive set X, either only slack vectors remain, or there is a unique new element y ∉ X such that X - x + y is primitive.

def IndexedLOrder.slackBoundary {T : Type u_1} {I : Type u_2} [Fintype I] [DecidableEq T] [DecidableEq I] (i : I) : Finset (ExtendedGoods T I)

The boundary almost primitive set made only of slacks, missing i.

Equations

• IndexedLOrder.slackBoundary i = IndexedLOrder.toAlmostPrimitive Finset.empty {i}

@[simp]

theorem IndexedLOrder.fromGoods_slackBoundary {T : Type u_1} {I : Type u_2} [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] (i : I) : fromGoods (slackBoundary i) = Finset.empty

@[simp]

theorem IndexedLOrder.fromMissing_slackBoundary {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype I] [DecidableEq T] [DecidableEq I] (i : I) : fromMissing (slackBoundary i) = {i}

@[simp]

theorem IndexedLOrder.associatedCell_slackBoundary {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] (i : I) : associatedCell (slackBoundary i) = (Finset.empty, {i})

theorem IndexedLOrder.slackBoundary_isAlmostPrimitive {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] [Finite T] (i : I) : isAlmostPrimitive (slackBoundary i)

Each slack boundary is an almost primitive set.

theorem IndexedLOrder.slackBoundary_isAlmostPrimitiveNative {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] (i : I) : isAlmostPrimitiveNative (slackBoundary i)

theorem IndexedLOrder.slackBoundary_unique_incident_primitive {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] (i : I) : ∃! X : Finset (ExtendedGoods T I), isPrimitive X ∧ slackBoundary i ⊆ X

theorem IndexedLOrder.slackBoundary_unique_incident_nativePrimitive {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] (i : I) : ∃! X : Finset (ExtendedGoods T I), isPrimitiveNative X ∧ slackBoundary i ⊆ X

theorem IndexedLOrder.boundary_almostPrimitive_eq_slackBoundary {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {Y : Finset (ExtendedGoods T I)} (hY : isAlmostPrimitive Y) (hBoundary : ¬(fromGoods Y).Nonempty) : ∃ (i : I), Y = slackBoundary i

Every almost primitive face made only of slack vectors is one of the boundary faces I - i.

theorem IndexedLOrder.boundary_almostPrimitive_unique_incident_primitive {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {Y : Finset (ExtendedGoods T I)} (hY : isAlmostPrimitive Y) (hBoundary : ¬(fromGoods Y).Nonempty) : ∃! X : Finset (ExtendedGoods T I), isPrimitive X ∧ Y ⊆ X

Boundary almost primitive faces are incident to exactly one primitive set.

theorem IndexedLOrder.native_boundary_almostPrimitive_unique_incident_primitive {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {Y : Finset (ExtendedGoods T I)} (hY : isAlmostPrimitiveNative Y) (hBoundary : ¬(fromGoods Y).Nonempty) : ∃! X : Finset (ExtendedGoods T I), isPrimitiveNative X ∧ Y ⊆ X

theorem IndexedLOrder.almostPrimitive_incident_primitives_boundary_or_internal {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {Y : Finset (ExtendedGoods T I)} (hY : isAlmostPrimitive Y) : (¬(fromGoods Y).Nonempty ∧ ∃! X : Finset (ExtendedGoods T I), isPrimitive X ∧ Y ⊆ X) ∨ (fromGoods Y).Nonempty ∧ ∃ (X₁ : Finset (ExtendedGoods T I)) (X₂ : Finset (ExtendedGoods T I)), X₁ ≠ X₂ ∧ isPrimitive X₁ ∧ isPrimitive X₂ ∧ Y ⊆ X₁ ∧ Y ⊆ X₂ ∧ ∀ (X : Finset (ExtendedGoods T I)), isPrimitive X → Y ⊆ X → X = X₁ ∨ X = X₂

The full Scarf incidence dichotomy for almost primitive faces: a boundary face is incident to one primitive set, while an internal face is incident to exactly two primitive sets.

theorem IndexedLOrder.native_almostPrimitive_incident_primitives_boundary_or_internal {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {Y : Finset (ExtendedGoods T I)} (hY : isAlmostPrimitiveNative Y) : (¬(fromGoods Y).Nonempty ∧ ∃! X : Finset (ExtendedGoods T I), isPrimitiveNative X ∧ Y ⊆ X) ∨ (fromGoods Y).Nonempty ∧ ∃ (X₁ : Finset (ExtendedGoods T I)) (X₂ : Finset (ExtendedGoods T I)), X₁ ≠ X₂ ∧ isPrimitiveNative X₁ ∧ isPrimitiveNative X₂ ∧ Y ⊆ X₁ ∧ Y ⊆ X₂ ∧ ∀ (X : Finset (ExtendedGoods T I)), isPrimitiveNative X → Y ⊆ X → X = X₁ ∨ X = X₂

theorem IndexedLOrder.almostPrimitive_subset_primitive_iff_doorof {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {Y X : Finset (ExtendedGoods T I)} (hY : isAlmostPrimitive Y) (hX : isPrimitive X) : Y ⊆ X ↔ isDoorof (fromGoods Y) (fromMissing Y) (fromGoods X) (fromMissing X)

Incidence between an almost primitive face and a primitive set is exactly the old room-door incidence after translating both sides back to (goods, indices).

def IndexedLOrder.primitiveReplacementStep {T : Type u_1} {I : Type u_2} [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] (X X' : Finset (ExtendedGoods T I)) : Prop

A Scarf replacement step: two primitive sets are adjacent if they share an almost primitive face. This is the primitive-set version of walking through a door from one room to another.

Equations

• One or more equations did not get rendered due to their size.

theorem IndexedLOrder.primitiveReplacementStep.symm {T : Type u_1} {I : Type u_2} [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {X X' : Finset (ExtendedGoods T I)} (h : primitiveReplacementStep X X') : primitiveReplacementStep X' X

theorem IndexedLOrder.replacementStep_has_common_door {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {X X' : Finset (ExtendedGoods T I)} (h : primitiveReplacementStep X X') : ∃ (Y : Finset (ExtendedGoods T I)), isAlmostPrimitive Y ∧ Y ⊆ X ∧ Y ⊆ X' ∧ isDoorof (fromGoods Y) (fromMissing Y) (fromGoods X) (fromMissing X) ∧ isDoorof (fromGoods Y) (fromMissing Y) (fromGoods X') (fromMissing X')

theorem IndexedLOrder.common_door_gives_replacementStep {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {τ : Finset T} {D : Finset I} {σ₁ σ₂ : Finset T} {C₁ C₂ : Finset I} (hDoor₁ : isDoorof τ D σ₁ C₁) (hDoor₂ : isDoorof τ D σ₂ C₂) (hNe : (σ₁, C₁) ≠ (σ₂, C₂)) : primitiveReplacementStep (toPrimitiveSet σ₁ C₁) (toPrimitiveSet σ₂ C₂)

theorem IndexedLOrder.internal_almostPrimitive_replacementStep {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {Y : Finset (ExtendedGoods T I)} (hY : isAlmostPrimitive Y) (hInternal : (fromGoods Y).Nonempty) : ∃ (X₁ : Finset (ExtendedGoods T I)) (X₂ : Finset (ExtendedGoods T I)), primitiveReplacementStep X₁ X₂ ∧ Y ⊆ X₁ ∧ Y ⊆ X₂

def IndexedLOrder.extendedColoring {T : Type u_1} {I : Type u_2} (c : T → I) : ExtendedGoods T I → I

Extend a coloring of goods by coloring each slack vector by its own index.

Equations

• IndexedLOrder.extendedColoring c (Sum.inl t) = c t
• IndexedLOrder.extendedColoring c (Sum.inr i) = i

@[simp]

theorem IndexedLOrder.extendedColoring_inl {T : Type u_1} {I : Type u_2} (c : T → I) (t : T) : extendedColoring c (Sum.inl t) = c t

@[simp]

theorem IndexedLOrder.extendedColoring_inr {T : Type u_1} {I : Type u_2} (c : T → I) (i : I) : extendedColoring c (Sum.inr i) = i

theorem IndexedLOrder.image_extendedColoring_toPrimitiveSet {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype I] [DecidableEq T] [DecidableEq I] (c : T → I) (σ : Finset T) (C : Finset I) : Finset.image (extendedColoring c) (toPrimitiveSet σ C) = Finset.image c σ ∪ Finset.univ \ C

theorem IndexedLOrder.full_color_primitive_iff_colorful_room {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] (c : T → I) {σ : Finset T} {C : Finset I} (hRoom : isRoom σ C) : Finset.image (extendedColoring c) (toPrimitiveSet σ C) = Finset.univ ↔ isColorful c σ C

For a room, Scarf's statement that a primitive set has all colors is exactly the Section 1 statement that the corresponding room is colorful.

def IndexedLOrder.isFullyColoredPrimitive {T : Type u_1} {I : Type u_2} [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] (c : T → I) (X : Finset (ExtendedGoods T I)) : Prop

Scarf's primitive-set coloring condition c(X) = I.

Equations

• IndexedLOrder.isFullyColoredPrimitive c X = (IndexedLOrder.isPrimitive X ∧ Finset.image (IndexedLOrder.extendedColoring c) X = Finset.univ)

theorem IndexedLOrder.full_color_primitive_iff_colorful_associated_room {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] (c : T → I) {X : Finset (ExtendedGoods T I)} (hX : isPrimitive X) : Finset.image (extendedColoring c) X = Finset.univ ↔ isColorful c (fromGoods X) (fromMissing X)

For an arbitrary primitive set, Scarf's condition c(X) = I is exactly the colorful-room condition for the associated room (X ∩ T, I \ X).

theorem IndexedLOrder.image_extendedColoring_toAlmostPrimitive {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype I] [DecidableEq T] [DecidableEq I] (c : T → I) (τ : Finset T) (D : Finset I) : Finset.image (extendedColoring c) (toAlmostPrimitive τ D) = Finset.image c τ ∪ Finset.univ \ D

theorem IndexedLOrder.diff_image_eq_singleton_iff_allButColor_toPrimitiveSet {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype I] [DecidableEq T] [DecidableEq I] (c : T → I) (i : I) (σ : Finset T) (C : Finset I) : C \ Finset.image c σ = {i} ↔ Finset.image (extendedColoring c) (toPrimitiveSet σ C) = Finset.univ.erase i

theorem IndexedLOrder.diff_image_eq_singleton_iff_allButColor_toAlmostPrimitive {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype I] [DecidableEq T] [DecidableEq I] (c : T → I) (i : I) (τ : Finset T) (D : Finset I) : D \ Finset.image c τ = {i} ↔ Finset.image (extendedColoring c) (toAlmostPrimitive τ D) = Finset.univ.erase i

theorem IndexedLOrder.allButColor_primitive_iff_typed_associated_room {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] (c : T → I) (i : I) {X : Finset (ExtendedGoods T I)} (hX : isPrimitive X) : Finset.image (extendedColoring c) X = Finset.univ.erase i ↔ isTypedNC c i (fromGoods X) (fromMissing X)

theorem IndexedLOrder.allButColor_almostPrimitive_iff_typed_associated_door {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] (c : T → I) (i : I) {Y : Finset (ExtendedGoods T I)} (hY : isAlmostPrimitive Y) : Finset.image (extendedColoring c) Y = Finset.univ.erase i ↔ isTypedNC c i (fromGoods Y) (fromMissing Y)

@[simp]

theorem IndexedLOrder.image_extendedColoring_slackBoundary {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype I] [DecidableEq T] [DecidableEq I] (c : T → I) (i : I) : Finset.image (extendedColoring c) (slackBoundary i) = Finset.univ.erase i

theorem IndexedLOrder.slackBoundary_GiDoorVertex {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] (c : T → I) (i : I) : GiDoorVertex c i (associatedCell (slackBoundary i))

theorem IndexedLOrder.fullyColoredPrimitive_GiRoomVertex {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {c : T → I} {i : I} {X : Finset (ExtendedGoods T I)} (hX : isFullyColoredPrimitive c X) : GiRoomVertex c i (associatedCell X)

theorem IndexedLOrder.allButColorPrimitive_GiRoomVertex {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {c : T → I} {i : I} {X : Finset (ExtendedGoods T I)} (hPrim : isPrimitive X) (hColor : Finset.image (extendedColoring c) X = Finset.univ.erase i) : GiRoomVertex c i (associatedCell X)

theorem IndexedLOrder.allButColorAlmostPrimitive_GiDoorVertex {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {c : T → I} {i : I} {Y : Finset (ExtendedGoods T I)} (hY : isAlmostPrimitive Y) (hColor : Finset.image (extendedColoring c) Y = Finset.univ.erase i) : GiDoorVertex c i (associatedCell Y)

theorem IndexedLOrder.algorithm_incidence_to_GiEdge {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {c : T → I} {i : I} {Y X : Finset (ExtendedGoods T I)} (hY : isAlmostPrimitive Y) (hYColor : Finset.image (extendedColoring c) Y = Finset.univ.erase i) (hX : isPrimitive X) (hXColor : Finset.image (extendedColoring c) X = Finset.univ.erase i ∨ Finset.image (extendedColoring c) X = Finset.univ) (hSub : Y ⊆ X) : GiEdge c i (associatedCell X) (associatedCell Y)

def IndexedLOrder.scarfSplitReplacementStep {T : Type u_1} {I : Type u_2} [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] (c : T → I) (i : I) (X Y X' : Finset (ExtendedGoods T I)) : Prop

A split Scarf replacement step, matching §3: an all-but-i primitive set moves through an all-but-i almost primitive face to another primitive set, which is either still all-but-i or already fully colored.

Equations

• One or more equations did not get rendered due to their size.

theorem IndexedLOrder.scarfSplitReplacementStep_replacementStep {T : Type u_1} {I : Type u_2} [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {c : T → I} {i : I} {X Y X' : Finset (ExtendedGoods T I)} (h : scarfSplitReplacementStep c i X Y X') : primitiveReplacementStep X X'

theorem IndexedLOrder.scarfSplitReplacementStep_GiEdges {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {c : T → I} {i : I} {X Y X' : Finset (ExtendedGoods T I)} (h : scarfSplitReplacementStep c i X Y X') : GiEdge c i (associatedCell X) (associatedCell Y) ∧ GiEdge c i (associatedCell X') (associatedCell Y)

def IndexedLOrder.scarfSplitReplacementStepWalk {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {c : T → I} {i : I} {X Y X' : Finset (ExtendedGoods T I)} (h : scarfSplitReplacementStep c i X Y X') : (GiGraph c i).Walk (associatedCell X) (associatedCell X')

The graph-walk segment represented by one split Scarf replacement step: X → Y → X'.

Equations

• IndexedLOrder.scarfSplitReplacementStepWalk h = SimpleGraph.Walk.cons ⋯ (SimpleGraph.Walk.cons ⋯ SimpleGraph.Walk.nil)

theorem IndexedLOrder.initial_scarf_step_to_GiEdge {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] (c : T → I) (i : I) : ∃ (X : Finset (ExtendedGoods T I)), isPrimitive X ∧ slackBoundary i ⊆ X ∧ GiEdge c i (associatedCell X) (associatedCell (slackBoundary i))

theorem IndexedLOrder.initial_scarf_step_walk {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] (c : T → I) (i : I) : ∃ (X : Finset (ExtendedGoods T I)) (_p : (GiGraph c i).Walk (associatedCell (slackBoundary i)) (associatedCell X)), isPrimitive X ∧ slackBoundary i ⊆ X

The first graph-walk segment of Scarf's algorithm, from I - i into the building.

structure IndexedLOrder.ScarfAlgorithmTrace {T : Type u_1} {I : Type u_2} [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] (c : T → I) (i : I) : Type (max u_1 u_2)

A complete primitive-language Scarf algorithm trace of type i. It starts at the boundary face I - i, follows G_i, and terminates at a fully colored primitive set. The local lemmas above build such walks from initial and split replacement segments.

• terminal : Finset (ExtendedGoods T I)

  The terminal room of a Scarf-algorithm trace.

• terminal_fullyColored : isFullyColoredPrimitive c self.terminal
• walk : (GiGraph c i).Walk (associatedCell (slackBoundary i)) (associatedCell self.terminal)

  The graph walk recorded by a Scarf-algorithm trace.

theorem IndexedLOrder.ScarfAlgorithmTrace.terminal_colorful_room {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {c : T → I} {i : I} (trace : ScarfAlgorithmTrace c i) : isColorful c (fromGoods trace.terminal) (fromMissing trace.terminal)

theorem IndexedLOrder.scarfAlgorithmTrace_of_reachable_fullyColoredPrimitive {T : Type u_1} {I : Type u_2} [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {c : T → I} {i : I} {X : Finset (ExtendedGoods T I)} (hX : isFullyColoredPrimitive c X) (hReach : (GiGraph c i).Reachable (associatedCell (slackBoundary i)) (associatedCell X)) : Nonempty (ScarfAlgorithmTrace c i)

A reachable fully colored primitive set gives a complete Scarf trace.

theorem IndexedLOrder.scarfAlgorithmTrace_of_component_fullyColoredPrimitive {T : Type u_1} {I : Type u_2} [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {c : T → I} {i : I} {X : Finset (ExtendedGoods T I)} (hX : isFullyColoredPrimitive c X) (hComponent : (GiGraph c i).connectedComponentMk (associatedCell X) = (GiGraph c i).connectedComponentMk (associatedCell (slackBoundary i))) : Nonempty (ScarfAlgorithmTrace c i)

It is enough to find a fully colored primitive set in the connected component of the outside door. This is the component-level form of the path-following argument in §3.

theorem IndexedLOrder.scarfAlgorithmTrace_nonempty_iff_component_fullyColoredPrimitive {T : Type u_1} {I : Type u_2} [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] (c : T → I) (i : I) : Nonempty (ScarfAlgorithmTrace c i) ↔ ∃ (X : Finset (ExtendedGoods T I)), isFullyColoredPrimitive c X ∧ (GiGraph c i).connectedComponentMk (associatedCell X) = (GiGraph c i).connectedComponentMk (associatedCell (slackBoundary i))

Existence of a complete Scarf trace is equivalent to finding a fully colored primitive set in the connected component of the outside door. This isolates the remaining graph-theoretic endpoint argument from the primitive-set translation.

theorem IndexedLOrder.outsideDoor_endpoint_cell_eq_slackBoundary {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {c : T → I} {i : I} {v : GiCell T I} (hDoor : GiDoorVertex c i v) (hOutside : isOutsideDoor v.1 v.2) : v = associatedCell (slackBoundary i)

theorem IndexedLOrder.giVertex_of_GiDegree_eq_one {T : Type u_1} {I : Type u_2} [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {c : T → I} {i : I} {v : GiCell T I} (hdeg : GiDegree c i v = 1) : GiVertex c i v

def IndexedLOrder.reachableComponentGraph {α : Type u_3} (G : SimpleGraph α) (v₀ : α) : SimpleGraph { v : α // G.Reachable v₀ v }

The induced subgraph on the vertices reachable from a fixed base vertex.

Equations

• IndexedLOrder.reachableComponentGraph G v₀ = { Adj := fun (a b : { v : α // G.Reachable v₀ v }) => G.Adj ↑a ↑b, symm := ⋯, loopless := ⋯ }

theorem IndexedLOrder.reachableComponentGraph_degree_eq {α : Type u_3} [Fintype α] (G : SimpleGraph α) (v₀ : α) (x : { v : α // G.Reachable v₀ v }) : (reachableComponentGraph G v₀).degree x = G.degree ↑x

theorem IndexedLOrder.scarfAlgorithmTrace_exists {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] [Inhabited I] (c : T → I) (i : I) : Nonempty (ScarfAlgorithmTrace c i)

theorem IndexedLOrder.scarf_fullyColoredPrimitive_exists_via_trace {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] [Inhabited I] (c : T → I) : ∃ (X : Finset (ExtendedGoods T I)), isFullyColoredPrimitive c X

Scarf's combinatorial theorem in the primitive-set language from §3: after extending a coloring by the identity on slack vectors, some primitive set has all colors, obtained by following the Scarf trace from the boundary door.

theorem IndexedLOrder.scarf_fullyColoredPrimitive_exists {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] [Inhabited I] (c : T → I) : ∃ (X : Finset (ExtendedGoods T I)), isFullyColoredPrimitive c X

Scarf's combinatorial theorem in the primitive-set language from §3. The proof is routed through the path-following trace, matching the narrative of the paper.

theorem IndexedLOrder.initial_scarf_primitive_from_boundary {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] (i : I) : ∃! X : Finset (ExtendedGoods T I), isPrimitive X ∧ slackBoundary i ⊆ X

The unique primitive set incident to the boundary face I - i, in the same language used to start Scarf's replacement path.

theorem IndexedLOrder.replacementStep_splits_through_almostPrimitive {T : Type u_1} {I : Type u_2} [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {X X' : Finset (ExtendedGoods T I)} (h : primitiveReplacementStep X X') : ∃ (Y : Finset (ExtendedGoods T I)), isAlmostPrimitive Y ∧ Y ⊆ X ∧ Y ⊆ X' ∧ X ≠ X'

Splitting a replacement step gives exactly the alternating primitive / almost-primitive pattern described in §3.

structure IndexedLOrder.UtilityRealization {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] (u : I → T → ℝ) : Prop

Utility functions realize the abstract preference orders when they preserve and reflect each indexed strict order.

• order_iff (i : I) (x y : T) : x < y ↔ u i x < u i y

structure IndexedLOrder.PositiveUtilityRealization {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] (u : I → T → ℝ) extends IndexedLOrder.UtilityRealization u : Prop

Positive utility functions, matching the economic convention in §3.

• order_iff (i : I) (x y : T) : x < y ↔ u i x < u i y
• positive (i : I) (x : T) : 0 < u i x

noncomputable def IndexedLOrder.orderLowerSet {T : Type u_1} {I : Type u_2} [Fintype T] [IST : IndexedLOrder I T] (i : I) (x : T) : Finset T

The lower contour set of x in the order indexed by i.

Equations

• IndexedLOrder.orderLowerSet i x = {y : T | y ≤ x}

noncomputable def IndexedLOrder.orderUtility {T : Type u_1} {I : Type u_2} [Fintype T] [IST : IndexedLOrder I T] (i : I) (x : T) : ℝ

The finite rank utility associated to an indexed order. Adding 1 makes it positive, matching the economic convention in the paper.

Equations

• IndexedLOrder.orderUtility i x = ↑(IndexedLOrder.orderLowerSet i x).card + 1

theorem IndexedLOrder.orderUtility_positive {T : Type u_1} {I : Type u_2} [Fintype T] [IST : IndexedLOrder I T] (i : I) (x : T) : 0 < orderUtility i x

theorem IndexedLOrder.orderUtility_order_iff {T : Type u_1} {I : Type u_2} [Fintype T] [IST : IndexedLOrder I T] (i : I) (x y : T) : x < y ↔ orderUtility i x < orderUtility i y

theorem IndexedLOrder.orderUtility_realization {T : Type u_1} {I : Type u_2} [Fintype T] [IST : IndexedLOrder I T] : UtilityRealization fun (i : I) (x : T) => orderUtility i x

theorem IndexedLOrder.positiveOrderUtility_realization {T : Type u_1} {I : Type u_2} [Fintype T] [IST : IndexedLOrder I T] : PositiveUtilityRealization fun (i : I) (x : T) => orderUtility i x

def IndexedLOrder.utilityVector {T : Type u_1} {I : Type u_2} (u : I → T → ℝ) (x : T) : I → ℝ

A utility vector embeds a good into ℝ^I.

Equations

• IndexedLOrder.utilityVector u x i = u i x

theorem IndexedLOrder.utilityVector_injective_of_realization {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] [Inhabited I] {u : I → T → ℝ} (hu : UtilityRealization u) : Function.Injective (utilityVector u)

noncomputable def IndexedLOrder.utilityImage {T : Type u_1} {I : Type u_2} [Fintype T] [Fintype I] (u : I → T → ℝ) : Finset (I → ℝ)

The finite coordinate image u(T) used when identifying goods with utility vectors.

Equations

• IndexedLOrder.utilityImage u = Finset.image (IndexedLOrder.utilityVector u) Finset.univ

noncomputable def IndexedLOrder.utilityImageEquiv {T : Type u_1} {I : Type u_2} [Fintype T] [Fintype I] [IST : IndexedLOrder I T] [Inhabited I] (u : I → T → ℝ) (hu : UtilityRealization u) : T ≃ ↥(utilityImage u)

The paper's "identify T with its image u(T)" step, formalized as an equivalence once the utility realization separates points.

Equations

• One or more equations did not get rendered due to their size.

def IndexedLOrder.slackVector {I : Type u_2} [DecidableEq I] (M : I → ℝ) (i : I) : I → ℝ

The coordinate model of Scarf's slack vector for face i: the ith coordinate is zero and all other coordinates are the chosen large value M i.

Equations

• IndexedLOrder.slackVector M i j = if j = i then 0 else M i

def IndexedLOrder.extendedCoordinatePoint {T : Type u_1} {I : Type u_2} [DecidableEq I] (u : I → T → ℝ) (M : I → ℝ) : ExtendedGoods T I → I → ℝ

Interpret the enlarged set T ∪ I as points in ℝ^I.

Equations

• IndexedLOrder.extendedCoordinatePoint u M (Sum.inl t) = IndexedLOrder.utilityVector u t
• IndexedLOrder.extendedCoordinatePoint u M (Sum.inr i) = IndexedLOrder.slackVector M i

def IndexedLOrder.uniformSlackHeight {T : Type u_1} {I : Type u_2} [Fintype T] : I → ℝ

A uniform choice of slack heights for a finite utility realization.

Equations

• IndexedLOrder.uniformSlackHeight = Function.const I (↑(Fintype.card T) + 2)

@[simp]

theorem IndexedLOrder.slackVector_self {I : Type u_2} [DecidableEq I] (M : I → ℝ) (i : I) : slackVector M i i = 0

@[simp]

theorem IndexedLOrder.slackVector_of_ne {I : Type u_2} [DecidableEq I] (M : I → ℝ) {i j : I} (h : j ≠ i) : slackVector M i j = M i

theorem IndexedLOrder.slackVector_other_coordinate_gt {I : Type u_2} [DecidableEq I] {M : I → ℝ} {i j : I} (hji : j ≠ i) {r : ℝ} (hr : r < M i) : r < slackVector M i j

def IndexedLOrder.SlackHeightsDominateGoodsCoordinates {T : Type u_1} {I : Type u_2} (u : I → T → ℝ) (M : I → ℝ) : Prop

Slack-height condition for Scarf's slack vectors: the nonzero coordinate coord of the slack vector s(slack) is above the corresponding coordinate of every good. Since s(slack) coord = M slack when coord ≠ slack, this is the condition needed for the coordinate model to match the abstract room/primitive-set model.

Equations

• IndexedLOrder.SlackHeightsDominateGoodsCoordinates u M = ∀ (slack coord : I) (x : T), coord ≠ slack → u coord x < M slack

@[reducible, inline]

abbrev IndexedLOrder.SlackBounds {T : Type u_1} {I : Type u_2} (u : I → T → ℝ) (M : I → ℝ) : Prop

Backwards-compatible short name for the slack-height condition.

Equations

• IndexedLOrder.SlackBounds u M = IndexedLOrder.SlackHeightsDominateGoodsCoordinates u M

theorem IndexedLOrder.slackBounds_iff_heights_gt_coordinates {T : Type u_1} {I : Type u_2} {u : I → T → ℝ} {M : I → ℝ} : SlackBounds u M ↔ ∀ (i j : I) (x : T), j ≠ i → u j x < M i

theorem IndexedLOrder.slackBounds_of_global_coordinate_bound {T : Type u_1} {I : Type u_2} {u : I → T → ℝ} {M : I → ℝ} {B : ℝ} (hGoods : ∀ (coord : I) (x : T), u coord x < B) (hHeights : ∀ (slack : I), B ≤ M slack) : SlackBounds u M

noncomputable def IndexedLOrder.slackImage {I : Type u_2} [Fintype I] [DecidableEq I] (M : I → ℝ) : Finset (I → ℝ)

The finite set of Scarf slack vectors.

Equations

• IndexedLOrder.slackImage M = Finset.image (IndexedLOrder.slackVector M) Finset.univ

noncomputable def IndexedLOrder.coordinateEnlargedSet {T : Type u_1} {I : Type u_2} [Fintype T] [Fintype I] [DecidableEq I] (u : I → T → ℝ) (M : I → ℝ) : Finset (I → ℝ)

The actual coordinate enlarged set u(T) ∪ {s(i) | i ∈ I} from §3.

Equations

• IndexedLOrder.coordinateEnlargedSet u M = IndexedLOrder.utilityImage u ∪ IndexedLOrder.slackImage M

theorem IndexedLOrder.extendedCoordinatePoint_mem_coordinateEnlargedSet {T : Type u_1} {I : Type u_2} [Fintype T] [Fintype I] [DecidableEq I] (u : I → T → ℝ) (M : I → ℝ) (z : ExtendedGoods T I) : extendedCoordinatePoint u M z ∈ coordinateEnlargedSet u M

theorem IndexedLOrder.slackVector_injective_of_bounds {T : Type u_1} {I : Type u_2} [Inhabited T] [DecidableEq I] [IST : IndexedLOrder I T] {u : I → T → ℝ} {M : I → ℝ} (hu : PositiveUtilityRealization u) (hM : SlackBounds u M) : Function.Injective (slackVector M)

theorem IndexedLOrder.utilityVector_ne_slackVector_of_positive {T : Type u_1} {I : Type u_2} [DecidableEq I] [IST : IndexedLOrder I T] {u : I → T → ℝ} {M : I → ℝ} (hu : PositiveUtilityRealization u) (x : T) (i : I) : utilityVector u x ≠ slackVector M i

theorem IndexedLOrder.extendedCoordinatePoint_injective_of_realization {T : Type u_1} {I : Type u_2} [Inhabited T] [DecidableEq I] [IST : IndexedLOrder I T] [Inhabited I] {u : I → T → ℝ} {M : I → ℝ} (hu : PositiveUtilityRealization u) (hM : SlackBounds u M) : Function.Injective (extendedCoordinatePoint u M)

theorem IndexedLOrder.coordinateEnlargedSet_exists_preimage {T : Type u_1} {I : Type u_2} [Fintype T] [Fintype I] [DecidableEq I] (u : I → T → ℝ) (M : I → ℝ) {v : I → ℝ} (hv : v ∈ coordinateEnlargedSet u M) : ∃ (z : ExtendedGoods T I), extendedCoordinatePoint u M z = v

noncomputable def IndexedLOrder.extendedCoordinateEquivCoordinateEnlargedSet {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq I] [IST : IndexedLOrder I T] [Inhabited I] {u : I → T → ℝ} {M : I → ℝ} (hu : PositiveUtilityRealization u) (hM : SlackBounds u M) : ExtendedGoods T I ≃ ↥(coordinateEnlargedSet u M)

The abstract T ∪ I representation is equivalent to the actual coordinate enlarged set u(T) ∪ {s(i)} under the paper's positivity/slack hypotheses.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem IndexedLOrder.extendedCoordinatePoint_good {T : Type u_1} {I : Type u_2} [DecidableEq I] (u : I → T → ℝ) (M : I → ℝ) (x : T) : extendedCoordinatePoint u M (Sum.inl x) = utilityVector u x

@[simp]

theorem IndexedLOrder.extendedCoordinatePoint_slack {T : Type u_1} {I : Type u_2} [DecidableEq I] (u : I → T → ℝ) (M : I → ℝ) (i : I) : extendedCoordinatePoint u M (Sum.inr i) = slackVector M i

theorem IndexedLOrder.slackBounds_lt_slack_coordinate {T : Type u_1} {I : Type u_2} [DecidableEq I] {u : I → T → ℝ} {M : I → ℝ} (hM : SlackBounds u M) {i j : I} (hji : j ≠ i) (x : T) : extendedCoordinatePoint u M (Sum.inl x) j < extendedCoordinatePoint u M (Sum.inr i) j

theorem IndexedLOrder.orderUtility_lt_uniformSlackHeight {T : Type u_1} {I : Type u_2} [Fintype T] [IST : IndexedLOrder I T] (i : I) (x : T) : orderUtility i x < uniformSlackHeight i

theorem IndexedLOrder.orderUtility_slackBounds {T : Type u_1} {I : Type u_2} [Fintype T] [IST : IndexedLOrder I T] : SlackBounds (fun (i : I) (x : T) => orderUtility i x) uniformSlackHeight

def IndexedLOrder.extendedCoordinateLt {T : Type u_1} {I : Type u_2} [DecidableEq I] (u : I → T → ℝ) (M : I → ℝ) (i : I) (x y : ExtendedGoods T I) : Prop

The coordinate-induced strict relation on T ∪ I: one point is smaller exactly when its ith coordinate is smaller. To match the paper, linearity is kept as an explicit hypothesis below rather than enforced by a tie-breaker.

Equations

• IndexedLOrder.extendedCoordinateLt u M i x y = (IndexedLOrder.extendedCoordinatePoint u M x i < IndexedLOrder.extendedCoordinatePoint u M y i)

def IndexedLOrder.CoordinateValuesDefineLinearOrders {T : Type u_1} {I : Type u_2} [DecidableEq I] (u : I → T → ℝ) (M : I → ℝ) : Prop

The paper assumes, after perturbing if necessary, that coordinate values define linear orders on the enlarged set.

Equations

• IndexedLOrder.CoordinateValuesDefineLinearOrders u M = ∀ (i : I), IsStrictTotalOrder (IndexedLOrder.ExtendedGoods T I) (IndexedLOrder.extendedCoordinateLt u M i)

def IndexedLOrder.SlackHeightsPairwiseDistinct {I : Type u_2} (M : I → ℝ) : Prop

The paper's "the M_i are pairwise different" assumption.

Equations

• IndexedLOrder.SlackHeightsPairwiseDistinct M = Function.Injective M

noncomputable def IndexedLOrder.utilityCoordinateValues {T : Type u_1} {I : Type u_2} [Fintype T] [Fintype I] (u : I → T → ℝ) : Finset ℝ

All utility coordinates, as a finite set of real numbers.

Equations

• IndexedLOrder.utilityCoordinateValues u = Finset.image (fun (p : I × T) => u p.1 p.2) (Finset.univ.product Finset.univ)

theorem IndexedLOrder.utilityCoordinateValues_nonempty {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [Inhabited I] (u : I → T → ℝ) : (utilityCoordinateValues u).Nonempty

noncomputable def IndexedLOrder.utilityCoordinateBound {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [Inhabited I] (u : I → T → ℝ) : ℝ

A strict upper bound for all utility coordinates. This packages the finite maximum used to make the slack heights dominate the goods coordinates.

Equations

• IndexedLOrder.utilityCoordinateBound u = (IndexedLOrder.utilityCoordinateValues u).max' ⋯ + 1

theorem IndexedLOrder.utility_lt_utilityCoordinateBound {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [Inhabited I] (u : I → T → ℝ) (j : I) (x : T) : u j x < utilityCoordinateBound u

noncomputable def IndexedLOrder.perturbedSlackHeight {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [Inhabited I] (u : I → T → ℝ) : I → ℝ

An explicit version of the paper's "perturb the slack heights" step: start above every utility coordinate and then add the finite index of each trader.

Equations

• IndexedLOrder.perturbedSlackHeight u i = IndexedLOrder.utilityCoordinateBound u + ↑↑((Fintype.equivFin I) i)

theorem IndexedLOrder.perturbedSlackHeight_slackBounds {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [Inhabited I] (u : I → T → ℝ) : SlackBounds u (perturbedSlackHeight u)

theorem IndexedLOrder.perturbedSlackHeight_pairwiseDistinct {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [Inhabited I] (u : I → T → ℝ) : SlackHeightsPairwiseDistinct (perturbedSlackHeight u)

theorem IndexedLOrder.utility_coordinate_injective {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] {u : I → T → ℝ} (hu : UtilityRealization u) (i : I) : Function.Injective fun (x : T) => u i x

theorem IndexedLOrder.extendedCoordinatePoint_coordinate_injective {T : Type u_1} {I : Type u_2} [Inhabited T] [DecidableEq I] [IST : IndexedLOrder I T] {u : I → T → ℝ} {M : I → ℝ} (hu : PositiveUtilityRealization u) (hM : SlackBounds u M) (hM_inj : SlackHeightsPairwiseDistinct M) (i : I) : Function.Injective fun (z : ExtendedGoods T I) => extendedCoordinatePoint u M z i

theorem IndexedLOrder.coordinateValuesDefineLinearOrders_of_realization {T : Type u_1} {I : Type u_2} [Inhabited T] [DecidableEq I] [IST : IndexedLOrder I T] {u : I → T → ℝ} {M : I → ℝ} (hu : PositiveUtilityRealization u) (hM : SlackBounds u M) (hM_inj : SlackHeightsPairwiseDistinct M) : CoordinateValuesDefineLinearOrders u M

Under the hypotheses stated in §3 (positive utilities realizing the preferences, slack bounds, and pairwise different slack heights), coordinate values themselves define linear orders on T ∪ I.

theorem IndexedLOrder.exists_perturbedSlackHeights_for_coordinate_orders {T : Type u_1} {I : Type u_2} [Inhabited T] [DecidableEq I] [IST : IndexedLOrder I T] [Inhabited I] [Finite T] [Finite I] {u : I → T → ℝ} (hu : PositiveUtilityRealization u) : ∃ (M : I → ℝ), SlackBounds u M ∧ SlackHeightsPairwiseDistinct M ∧ CoordinateValuesDefineLinearOrders u M

The fully formalized perturbation step from §3: for every positive utility realization on a finite, nonempty index set, there are slack heights that dominate all goods coordinates, are pairwise distinct, and therefore make coordinate comparison into linear orders on T ∪ I.

theorem IndexedLOrder.exists_coordinateUtilityModel {T : Type u_1} {I : Type u_2} [Inhabited T] [DecidableEq I] [IST : IndexedLOrder I T] [Inhabited I] [Finite T] [Finite I] : ∃ (u : I → T → ℝ) (M : I → ℝ), PositiveUtilityRealization u ∧ SlackBounds u M ∧ SlackHeightsPairwiseDistinct M ∧ CoordinateValuesDefineLinearOrders u M

The §3 utility-and-perturbation passage as a single existence statement: starting only from the abstract indexed linear orders, choose positive utility functions realizing the orders and pairwise distinct slack heights large enough to make coordinate comparison linear on the enlarged set.

@[reducible]

noncomputable def IndexedLOrder.coordinateIndexedLOrder {T : Type u_1} {I : Type u_2} [DecidableEq I] (u : I → T → ℝ) (M : I → ℝ) (hCoord : CoordinateValuesDefineLinearOrders u M) : IndexedLOrder I (ExtendedGoods T I)

The indexed family of coordinate-induced orders on the enlarged set.

Equations

• IndexedLOrder.coordinateIndexedLOrder u M hCoord = { IST := fun (i : I) => linearOrderOfSTO (IndexedLOrder.extendedCoordinateLt u M i) }

theorem IndexedLOrder.extendedCoordinateLt_of_coord_lt {T : Type u_1} {I : Type u_2} [DecidableEq I] {u : I → T → ℝ} {M : I → ℝ} {i : I} {x y : ExtendedGoods T I} (h : extendedCoordinatePoint u M x i < extendedCoordinatePoint u M y i) : extendedCoordinateLt u M i x y

theorem IndexedLOrder.extendedCoordinateLt_goods_of_original_lt {T : Type u_1} {I : Type u_2} [DecidableEq I] [IST : IndexedLOrder I T] {u : I → T → ℝ} {M : I → ℝ} (hu : UtilityRealization u) {i : I} {x y : T} (hxy : x < y) : extendedCoordinateLt u M i (Sum.inl x) (Sum.inl y)

theorem IndexedLOrder.original_lt_of_extendedCoordinateLt_goods {T : Type u_1} {I : Type u_2} [DecidableEq I] [IST : IndexedLOrder I T] {u : I → T → ℝ} {M : I → ℝ} (hu : UtilityRealization u) {i : I} {x y : T} (hxy : extendedCoordinateLt u M i (Sum.inl x) (Sum.inl y)) : x < y

theorem IndexedLOrder.extendedCoordinateLt_goods_iff {T : Type u_1} {I : Type u_2} [DecidableEq I] [IST : IndexedLOrder I T] {u : I → T → ℝ} {M : I → ℝ} (hu : UtilityRealization u) (i : I) (x y : T) : extendedCoordinateLt u M i (Sum.inl x) (Sum.inl y) ↔ x < y

theorem IndexedLOrder.coordinateGoods_le_of_original_le {T : Type u_1} {I : Type u_2} [DecidableEq I] [IST : IndexedLOrder I T] {u : I → T → ℝ} {M : I → ℝ} (hCoord : CoordinateValuesDefineLinearOrders u M) (hu : UtilityRealization u) {i : I} {x y : T} (hxy : x ≤ y) : Sum.inl x ≤ Sum.inl y

theorem IndexedLOrder.original_le_of_coordinateGoods_le {T : Type u_1} {I : Type u_2} [DecidableEq I] [IST : IndexedLOrder I T] {u : I → T → ℝ} {M : I → ℝ} (hCoord : CoordinateValuesDefineLinearOrders u M) (hu : UtilityRealization u) {i : I} {x y : T} (hxy : Sum.inl x ≤ Sum.inl y) : x ≤ y

theorem IndexedLOrder.coordinateGood_lt_slack_of_ne {T : Type u_1} {I : Type u_2} [DecidableEq I] {u : I → T → ℝ} {M : I → ℝ} (hM : SlackBounds u M) {i k : I} (hik : i ≠ k) (x : T) : extendedCoordinateLt u M i (Sum.inl x) (Sum.inr k)

theorem IndexedLOrder.coordinateSlack_lt_good {T : Type u_1} {I : Type u_2} [DecidableEq I] [IST : IndexedLOrder I T] {u : I → T → ℝ} {M : I → ℝ} (hu : PositiveUtilityRealization u) (i : I) (x : T) : extendedCoordinateLt u M i (Sum.inr i) (Sum.inl x)

theorem IndexedLOrder.coordinateSlack_lt_slack_of_ne {T : Type u_1} {I : Type u_2} [Inhabited T] [DecidableEq I] [IST : IndexedLOrder I T] {u : I → T → ℝ} {M : I → ℝ} (hu : PositiveUtilityRealization u) (hM : SlackBounds u M) {i k : I} (hik : i ≠ k) : extendedCoordinateLt u M i (Sum.inr i) (Sum.inr k)

def IndexedLOrder.isCoordinatePrimitive {T : Type u_1} {I : Type u_2} [Fintype I] [DecidableEq I] (u : I → T → ℝ) (M : I → ℝ) (hCoord : CoordinateValuesDefineLinearOrders u M) (X : Finset (ExtendedGoods T I)) : Prop

The literal coordinate-dominance primitive definition on the enlarged ordered set.

Equations

• IndexedLOrder.isCoordinatePrimitive u M hCoord X = (X.card = Fintype.card I ∧ IndexedLOrder.isDominant X Finset.univ)

theorem IndexedLOrder.nativePrimitive_to_coordinatePrimitive {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {u : I → T → ℝ} {M : I → ℝ} {hCoord : CoordinateValuesDefineLinearOrders u M} (hu : PositiveUtilityRealization u) (hM : SlackBounds u M) {X : Finset (ExtendedGoods T I)} (hX : isPrimitiveNative X) : isCoordinatePrimitive u M hCoord X

theorem IndexedLOrder.coordinatePrimitive_to_nativePrimitive {T : Type u_1} {I : Type u_2} [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {u : I → T → ℝ} {M : I → ℝ} {hCoord : CoordinateValuesDefineLinearOrders u M} (hu : PositiveUtilityRealization u) {X : Finset (ExtendedGoods T I)} (hX : isCoordinatePrimitive u M hCoord X) : isPrimitiveNative X

theorem IndexedLOrder.coordinatePrimitive_iff_native {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {u : I → T → ℝ} {M : I → ℝ} {hCoord : CoordinateValuesDefineLinearOrders u M} (hu : PositiveUtilityRealization u) (hM : SlackBounds u M) {X : Finset (ExtendedGoods T I)} : isCoordinatePrimitive u M hCoord X ↔ isPrimitiveNative X

theorem IndexedLOrder.coordinatePrimitive_erase_replacement_mainLemma {T : Type u_1} {I : Type u_2} [Inhabited T] [Fintype T] [Fintype I] [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {u : I → T → ℝ} {M : I → ℝ} {hCoord : CoordinateValuesDefineLinearOrders u M} (hu : PositiveUtilityRealization u) (hM : SlackBounds u M) {X : Finset (ExtendedGoods T I)} (hX : isCoordinatePrimitive u M hCoord X) {x : ExtendedGoods T I} (hx : x ∈ X) : ¬(fromGoods (X.erase x)).Nonempty ∨ ∃! y : ExtendedGoods T I, y ∉ X ∧ isCoordinatePrimitive u M hCoord (insert y (X.erase x))

Scarf's main lemma for the literal coordinate-dominance definition of primitive sets on T ∪ I.