The Scarf path graph

This file builds the graph G_i whose vertices are the colorful and typed nearly-colorful rooms and doors of a fixed type i, and whose edges are room-door incidences. Following a path in this graph between odd-degree vertices is the combinatorial heart of the path-following proof of Scarf's lemma.

@[reducible, inline]

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

A room/door cell, represented as the pair (σ, C).

Equations

• IndexedLOrder.GiCell T I = (Finset T × Finset I)

def IndexedLOrder.GiRoomVertex {T : Type u_1} {I : Type u_2} [DecidableEq I] [IST : IndexedLOrder I T] (c : T → I) (i : I) (v : GiCell T I) : Prop

The room-type vertices of the graph G_i: colorful rooms and typed nearly-colorful rooms.

Equations

• IndexedLOrder.GiRoomVertex c i v = (IndexedLOrder.isColorful c v.1 v.2 ∨ IndexedLOrder.isRoom v.1 v.2 ∧ IndexedLOrder.isTypedNC c i v.1 v.2)

def IndexedLOrder.GiDoorVertex {T : Type u_1} {I : Type u_2} [DecidableEq I] [IST : IndexedLOrder I T] (c : T → I) (i : I) (v : GiCell T I) : Prop

The door-type vertices of the graph G_i: typed nearly-colorful doors.

Equations

• IndexedLOrder.GiDoorVertex c i v = (IndexedLOrder.isDoor v.1 v.2 ∧ IndexedLOrder.isTypedNC c i v.1 v.2)

def IndexedLOrder.GiVertex {T : Type u_1} {I : Type u_2} [DecidableEq I] [IST : IndexedLOrder I T] (c : T → I) (i : I) (v : GiCell T I) : Prop

Vertices of G_i: the relevant rooms and doors of fixed type i.

Equations

• IndexedLOrder.GiVertex c i v = (IndexedLOrder.GiRoomVertex c i v ∨ IndexedLOrder.GiDoorVertex c i v)

def IndexedLOrder.GiEdge {T : Type u_1} {I : Type u_2} [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] (c : T → I) (i : I) (v w : GiCell T I) : Prop

Edges of G_i: room-door incidence, made symmetric.

Equations

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

theorem IndexedLOrder.GiEdge.symm {T : Type u_1} {I : Type u_2} [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {c : T → I} {i : I} {v w : GiCell T I} (h : GiEdge c i v w) : GiEdge c i w v

theorem IndexedLOrder.GiEdge.left_vertex {T : Type u_1} {I : Type u_2} [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {c : T → I} {i : I} {v w : GiCell T I} (h : GiEdge c i v w) : GiVertex c i v

theorem IndexedLOrder.GiEdge.right_vertex {T : Type u_1} {I : Type u_2} [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {c : T → I} {i : I} {v w : GiCell T I} (h : GiEdge c i v w) : GiVertex c i w

theorem IndexedLOrder.GiRoomVertex.room {T : Type u_1} {I : Type u_2} [DecidableEq I] [IST : IndexedLOrder I T] {c : T → I} {i : I} {v : GiCell T I} (h : GiRoomVertex c i v) : isRoom v.1 v.2

theorem IndexedLOrder.GiDoorVertex.door {T : Type u_1} {I : Type u_2} [DecidableEq I] [IST : IndexedLOrder I T] {c : T → I} {i : I} {v : GiCell T I} (h : GiDoorVertex c i v) : isDoor v.1 v.2

theorem IndexedLOrder.GiEdge.irrefl {T : Type u_1} {I : Type u_2} [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {c : T → I} {i : I} (v : GiCell T I) : ¬GiEdge c i v v

def IndexedLOrder.GiGraph {T : Type u_1} {I : Type u_2} [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] (c : T → I) (i : I) : SimpleGraph (GiCell T I)

The Mathlib SimpleGraph whose vertices and edges are the graph G_i.

Equations

• IndexedLOrder.GiGraph c i = { Adj := IndexedLOrder.GiEdge c i, symm := ⋯, loopless := ⋯ }

noncomputable def IndexedLOrder.GiNeighbors {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) : Finset (GiCell T I)

The finite neighbor set of a vertex in G_i.

Equations

• IndexedLOrder.GiNeighbors c i v = (IndexedLOrder.GiGraph c i).neighborFinset v

theorem IndexedLOrder.mem_GiNeighbors {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 w : GiCell T I} : w ∈ GiNeighbors c i v ↔ GiEdge c i v w

noncomputable def IndexedLOrder.GiDegree {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) : ℕ

Degree in G_i.

Equations

• IndexedLOrder.GiDegree c i v = (IndexedLOrder.GiNeighbors c i v).card

def IndexedLOrder.GiEndpoint {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) : Prop

Endpoint vertices of G_i.

Equations

• IndexedLOrder.GiEndpoint c i v = (IndexedLOrder.GiVertex c i v ∧ IndexedLOrder.GiDegree c i v = 1)

theorem IndexedLOrder.not_room_of_door {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] {τ : Finset T} {D : Finset I} (hDoor : isDoor τ D) : ¬isRoom τ D

theorem IndexedLOrder.not_colorful_of_door {T : Type u_1} {I : Type u_2} [DecidableEq I] [IST : IndexedLOrder I T] {c : T → I} {τ : Finset T} {D : Finset I} (hDoor : isDoor τ D) : ¬isColorful c τ D

theorem IndexedLOrder.not_GiRoomVertex_of_door {T : Type u_1} {I : Type u_2} [DecidableEq I] [IST : IndexedLOrder I T] {c : T → I} {i : I} {τ : Finset T} {D : Finset I} (hDoor : isDoor τ D) : ¬GiRoomVertex c i (τ, D)

theorem IndexedLOrder.not_door_of_room {T : Type u_1} {I : Type u_2} [IST : IndexedLOrder I T] {σ : Finset T} {C : Finset I} (hRoom : isRoom σ C) : ¬isDoor σ C

theorem IndexedLOrder.not_GiDoorVertex_of_room {T : Type u_1} {I : Type u_2} [DecidableEq I] [IST : IndexedLOrder I T] {c : T → I} {i : I} {σ : Finset T} {C : Finset I} (hRoom : isRoom σ C) : ¬GiDoorVertex c i (σ, C)

theorem IndexedLOrder.isDoor_of_Doorof {T : Type u_1} {I : Type u_2} [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {τ σ : Finset T} {D C : Finset I} (hDoorof : isDoorof τ D σ C) : isDoor τ D

theorem IndexedLOrder.GiRoomVertex_of_incident_typed_door {T : Type u_1} {I : Type u_2} [DecidableEq T] [DecidableEq I] [IST : IndexedLOrder I T] {c : T → I} {i : I} {τ σ : Finset T} {D C : Finset I} (hTypedDoor : isTypedNC c i τ D) (hDoorof : isDoorof τ D σ C) : GiRoomVertex c i (σ, C)

theorem IndexedLOrder.GiDegree_internalDoor {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} {τ : Finset T} {D : Finset I} (hInternal : isInternalDoor τ D) (hTyped : isTypedNC c i τ D) : GiDegree c i (τ, D) = 2

theorem IndexedLOrder.GiDegree_typedNCRoom {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} {σ : Finset T} {C : Finset I} (hRoom : isRoom σ C) (hTyped : isTypedNC c i σ C) : GiDegree c i (σ, C) = 2

theorem IndexedLOrder.GiDegree_outsideDoor {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} {τ : Finset T} {D : Finset I} (hOutside : isOutsideDoor τ D) (hTyped : isTypedNC c i τ D) : GiDegree c i (τ, D) = 1

theorem IndexedLOrder.GiDegree_colorfulRoom {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} {σ : Finset T} {C : Finset I} (hColorful : isColorful c σ C) : GiDegree c i (σ, C) = 1

def IndexedLOrder.simpleGraphDegreeAtMostTwo {α : Type u_3} [Fintype α] (G : SimpleGraph α) : Prop

A graph has degree at most two at each vertex.

Equations

• IndexedLOrder.simpleGraphDegreeAtMostTwo G = ∀ (v : α), G.degree v ≤ 2

def IndexedLOrder.simpleGraphPathComponent {α : Type u_3} (G : SimpleGraph α) (component : G.ConnectedComponent) : Prop

A connected component is represented by a Mathlib graph path.

Equations

• IndexedLOrder.simpleGraphPathComponent G component = ∃ (u : α) (v : α) (p : G.Walk u v), p.IsPath ∧ {x : α | x ∈ p.support} = component.supp

def IndexedLOrder.simpleGraphCycleComponent {α : Type u_3} (G : SimpleGraph α) (component : G.ConnectedComponent) : Prop

A connected component is represented by a Mathlib graph cycle.

Equations

• IndexedLOrder.simpleGraphCycleComponent G component = ∃ (u : α) (p : G.Walk u u), p.IsCycle ∧ {x : α | x ∈ p.support} = component.supp

def IndexedLOrder.simpleGraphComponentsArePathsOrCycles {α : Type u_3} (G : SimpleGraph α) : Prop

The literal "disjoint paths and cycles" component statement for a finite SimpleGraph.

Equations

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

def IndexedLOrder.GiDegreeCharacterization {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) : Prop

The degree characterization of G_i: every vertex has degree one or two, and the degree-one vertices are exactly the unique outside door of type i and the colorful rooms.

Equations

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

theorem IndexedLOrder.GiDegreeCharacterization_holds {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) : GiDegreeCharacterization c i

def IndexedLOrder.GiPathStructure {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) : Prop

The path-structure target for G_i: degree characterization plus the local degree-at-most-two property used by path-following.

Equations

• IndexedLOrder.GiPathStructure c i = (IndexedLOrder.GiDegreeCharacterization c i ∧ IndexedLOrder.simpleGraphDegreeAtMostTwo (IndexedLOrder.GiGraph c i))

def IndexedLOrder.GiComponentStructure {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) : Prop

The faithful component-level target for G_i: its connected components are paths or cycles, and the endpoints of path components are exactly colorful rooms except for the unique outside door of type i.

Equations

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

theorem IndexedLOrder.GiPathStructure_of_degreeCharacterization {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} (hdegStmt : GiDegreeCharacterization c i) : GiPathStructure c i

theorem IndexedLOrder.GiComponentStructure_of_components_are_paths_or_cycles {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} (hdegStmt : GiDegreeCharacterization c i) (hcomponents : simpleGraphComponentsArePathsOrCycles (GiGraph c i)) : GiComponentStructure c i

theorem IndexedLOrder.exists_maximal_component_path_of_degree_le_two {α : Type u_3} [Fintype α] (G : SimpleGraph α) (_hdeg : simpleGraphDegreeAtMostTwo G) (component : G.ConnectedComponent) : ∃ (u : α) (v : α) (p : G.Walk u v), p.IsPath ∧ {x : α | x ∈ p.support} ⊆ component.supp ∧ ∀ (u' v' : α) (p' : G.Walk u' v'), p'.IsPath → {x : α | x ∈ p'.support} ⊆ component.supp → p'.length ≤ p.length

Generic graph-theoretic step 1: in a finite connected component of a graph of degree at most two, choose a path whose support is maximal inside that component.

theorem IndexedLOrder.maximal_component_path_no_escape_of_degree_le_two {α : Type u_3} [Fintype α] (G : SimpleGraph α) (hdeg : simpleGraphDegreeAtMostTwo G) {component : G.ConnectedComponent} {u v : α} {p : G.Walk u v} (hp : p.IsPath) (hp_sub : {x : α | x ∈ p.support} ⊆ component.supp) (hmax : ∀ (u' v' : α) (p' : G.Walk u' v'), p'.IsPath → {x : α | x ∈ p'.support} ⊆ component.supp → p'.length ≤ p.length) {x y : α} (hx : x ∈ p.support) (hxy : G.Adj x y) (hycomp : y ∈ component.supp) : y ∈ p.support

Generic graph-theoretic step 2a: in a graph of degree at most two, a maximal component path has no neighbor outside its support. This is the point that rules out T-shaped components.

theorem IndexedLOrder.component_path_support_eq_component_of_no_escape {α : Type u_3} (G : SimpleGraph α) {component : G.ConnectedComponent} {u v : α} {p : G.Walk u v} (hp_sub : {x : α | x ∈ p.support} ⊆ component.supp) (hend : ∀ ⦃x y : α⦄, x ∈ p.support → G.Adj x y → y ∈ component.supp → y ∈ p.support) : {x : α | x ∈ p.support} = component.supp

Generic graph-theoretic step 2b: if a component path has no edge escaping its support inside the component, then its support is the whole component.

theorem IndexedLOrder.component_cycle_of_maximal_path_closes {α : Type u_3} (G : SimpleGraph α) {component : G.ConnectedComponent} {u v : α} {p : G.Walk u v} (hp : p.IsPath) (hsupp : {x : α | x ∈ p.support} = component.supp) (hclose : G.Adj v u) (hnew : s(v, u) ∉ p.edges) : simpleGraphCycleComponent G component

theorem IndexedLOrder.component_path_of_support_eq_component {α : Type u_3} (G : SimpleGraph α) {component : G.ConnectedComponent} {u v : α} {p : G.Walk u v} (hp : p.IsPath) (hsupp : {x : α | x ∈ p.support} = component.supp) : simpleGraphPathComponent G component

A path whose support is exactly a component represents that component as a path.

theorem IndexedLOrder.simpleGraph_components_path_or_cycle_of_degree_le_two {α : Type u_3} [Fintype α] (G : SimpleGraph α) (hdeg : simpleGraphDegreeAtMostTwo G) : simpleGraphComponentsArePathsOrCycles G

Generic graph-theoretic theorem: every connected component of a finite graph whose vertices all have degree at most two is represented by either a path or a cycle.

theorem IndexedLOrder.GiComponentStructure_holds {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) : GiComponentStructure c i

Final graph structure statement for G_i: its components are paths or cycles, and its endpoints are exactly the outside door of type i and the colorful rooms.