The concrete path operations used by the source induction, PT-01/PT-02/PT-04/PT-09. The protected finite-sequence representation is unchanged. Appending one vertex is enough for the source proof; no injectivity of the sequence is imposed.

def TutteFormalization.TuttePath.singleton {α : Type u_1} {M : Matroid α} (H : Set α) (hH : IsHyperplane M H) : TuttePath M

PT-01: a one-vertex path has no edge conditions.

Equations

• TutteFormalization.TuttePath.singleton H hH = { length := 0, vertex := fun (x : Fin (0 + 1)) => H, isHyperplane := ⋯, adjacent := ⋯ }

@[simp]

theorem TutteFormalization.TuttePath.singleton_origin {α : Type u_1} {M : Matroid α} (H : Set α) (hH : IsHyperplane M H) : (singleton H hH).origin = H

@[simp]

theorem TutteFormalization.TuttePath.singleton_terminus {α : Type u_1} {M : Matroid α} (H : Set α) (hH : IsHyperplane M H) : (singleton H hH).terminus = H

theorem TutteFormalization.TuttePath.singleton_on {α : Type u_1} {M : Matroid α} {H F : Set α} (hH : IsHyperplane M H) (hF : F ⊆ H) : (singleton H hH).On F

theorem TutteFormalization.TuttePath.singleton_off {α : Type u_1} {M : Matroid α} {H : Set α} {Γ : Set (Set α)} (hH : IsHyperplane M H) (hΓ : H ∉ Γ) : (singleton H hH).Off Γ

theorem TutteFormalization.TuttePath.On.mono {α : Type u_1} {M : Matroid α} {p : TuttePath M} {F G : Set α} (h : p.On G) (hFG : F ⊆ G) : p.On F

PT-04: a path on a larger flat is also on any subset of that flat.

def TutteFormalization.TuttePath.snoc {α : Type u_1} {M : Matroid α} (p : TuttePath M) (H : Set α) (hH : IsHyperplane M H) (hEdge : TutteAdjacent M p.terminus H) : TuttePath M

PT-09: append a hyperplane joined to the old terminus by a Tutte edge.

Equations

• p.snoc H hH hEdge = { length := p.length + 1, vertex := Fin.snoc p.vertex H, isHyperplane := ⋯, adjacent := ⋯ }

@[simp]

theorem TutteFormalization.TuttePath.snoc_origin {α : Type u_1} {M : Matroid α} (p : TuttePath M) (H : Set α) (hH : IsHyperplane M H) (hEdge : TutteAdjacent M p.terminus H) : (p.snoc H hH hEdge).origin = p.origin

@[simp]

theorem TutteFormalization.TuttePath.snoc_terminus {α : Type u_1} {M : Matroid α} (p : TuttePath M) (H : Set α) (hH : IsHyperplane M H) (hEdge : TutteAdjacent M p.terminus H) : (p.snoc H hH hEdge).terminus = H

theorem TutteFormalization.TuttePath.On.snoc {α : Type u_1} {M : Matroid α} {p : TuttePath M} {F H : Set α} (h : p.On F) (hH : IsHyperplane M H) (hEdge : TutteAdjacent M p.terminus H) (hFH : F ⊆ H) : (p.snoc H hH hEdge).On F

theorem TutteFormalization.TuttePath.Off.snoc {α : Type u_1} {M : Matroid α} {p : TuttePath M} {Γ : Set (Set α)} {H : Set α} (h : p.Off Γ) (hH : IsHyperplane M H) (hEdge : TutteAdjacent M p.terminus H) (hHoff : H ∉ Γ) : (p.snoc H hH hEdge).Off Γ

theorem TutteFormalization.exists_singleton_path {α : Type u_1} {M : Matroid α} {F X : Set α} {Γ : Set (Set α)} (hX : IsHyperplane M X) (hFX : F ⊆ X) (hXoff : X ∉ Γ) : ∃ (p : TuttePath M), p.origin = X ∧ p.terminus = X ∧ p.On F ∧ p.Off Γ

PT-01: the singleton case with the full endpoint and On/Off conclusions.

theorem TutteFormalization.exists_edge_path {α : Type u_1} {M : Matroid α} {F X Y : Set α} {Γ : Set (Set α)} (hX : IsHyperplane M X) (hY : IsHyperplane M Y) (hXY : TutteAdjacent M X Y) (hFX : F ⊆ X) (hFY : F ⊆ Y) (hXoff : X ∉ Γ) (hYoff : Y ∉ Γ) : ∃ (p : TuttePath M), p.origin = X ∧ p.terminus = Y ∧ p.On F ∧ p.Off Γ

PT-02: a single edge, with all finite-sequence and vertex constraints.

theorem TutteFormalization.exists_path_of_corankTwo {α : Type u_1} {M : Matroid α} [M.Finite] {F X Y : Set α} {Γ : Set (Set α)} (hF : Indecomposable M F) (hc : CorankTwo M F) (hX : IsHyperplane M X) (hY : IsHyperplane M Y) (hFX : F ⊆ X) (hFY : F ⊆ Y) (hXoff : X ∉ Γ) (hYoff : Y ∉ Γ) : ∃ (p : TuttePath M), p.origin = X ∧ p.terminus = Y ∧ p.On F ∧ p.Off Γ

PT-02: complete corank-two base path, including equal endpoints.