Tutte's path theorem for finite matroids, proved by corank induction.

Source: Baker–Jin–Lorscheid, arXiv:2601.02582v2, Theorem 1.8 (thm:path-theorem). Definitions appear in LeanPool.TuttePath.Definitions. Structural dependencies are proved in the imported project modules.

theorem TutteFormalization.path_theorem_of_indecomposable {α : Type u_1} (M : Matroid α) [M.Finite] (Γ : Set (Set α)) (hΓ : ModularCut M Γ) (F : Set α) (hF : Indecomposable M F) (X Y : Set α) (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 Γ

The stronger path theorem: connectedness of the contraction by F suffices. Properness of F follows from containment in the endpoint hyperplane.

theorem TutteFormalization.path_theorem {α : Type u_1} (M : Matroid α) [M.Finite] (_hM : Connected M) (Γ : Set (Set α)) (hΓ : ModularCut M Γ) (F : Set α) (hF : Indecomposable M F) (_hFproper : F ≠ M.E) (X Y : Set α) (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 Γ

thm:path-theorem, the two-endpoints-off-cut BJL formulation. A source-faithful specialization of path_theorem_of_indecomposable.