Source vocabulary for Baker–Jin–Lorscheid, arXiv:2601.02582, Sections 1 and 4. We reuse Mathlib flats, closure, contraction and eRk. In the finite-ground-set setting all ranks here are finite, so their equations are natural-rank equations. The pinned matroid API has no connectedness, hyperplane or modular-cut predicate.

def TutteFormalization.Connected {α : Type u_1} (M : Matroid α) : Prop

def:matroid-operations: no partition into two nonempty additive-rank parts. In particular, no nonemptiness of the ground set is required.

Equations

• TutteFormalization.Connected M = ¬∃ (A : Set α) (B : Set α), A.Nonempty ∧ B.Nonempty ∧ Disjoint A B ∧ A ∪ B = M.E ∧ M.eRk A + M.eRk B = M.eRk M.E

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

def:matroid: a maximal proper flat. Ground containment follows from IsFlat.

Equations

• TutteFormalization.IsHyperplane M H = (M.IsFlat H ∧ H ≠ M.E ∧ ∀ (G : Set α), M.IsFlat G → H ⊆ G → G = H ∨ G = M.E)

def TutteFormalization.Indecomposable {α : Type u_1} (M : Matroid α) (F : Set α) : Prop

def:indecomposable: flatness and source connectedness of the contraction.

Equations

• TutteFormalization.Indecomposable M F = (M.IsFlat F ∧ TutteFormalization.Connected (M.contract F))

def TutteFormalization.ModularPair {α : Type u_1} (M : Matroid α) (F G : Set α) : Prop

def:modular-cut: a pair of flats satisfying the modular rank equality. Their join is the Mathlib closure of their union.

Equations

• TutteFormalization.ModularPair M F G = (M.IsFlat F ∧ M.IsFlat G ∧ M.eRk F + M.eRk G = M.eRk (F ∩ G) + M.eRk (M.closure (F ∪ G)))

structure TutteFormalization.ModularCut {α : Type u_1} (M : Matroid α) (Γ : Set (Set α)) : Prop

def:modular-cut: a collection of flats, upward closed among flats and closed under intersections of modular pairs. The empty collection is allowed.

• isFlat (F : Set α) : F ∈ Γ → M.IsFlat F
• upward (F G : Set α) : F ∈ Γ → M.IsFlat G → F ⊆ G → G ∈ Γ
• inter_mem (F G : Set α) : F ∈ Γ → G ∈ Γ → ModularPair M F G → F ∩ G ∈ Γ

def TutteFormalization.CorankTwo {α : Type u_1} (M : Matroid α) (F : Set α) : Prop

A corank-two flat: for finite ground set, this rank equation says rk(M.E) - rk(F) = 2, without truncated subtraction or conversion from ℕ∞.

Equations

• TutteFormalization.CorankTwo M F = (M.IsFlat F ∧ M.eRk F + 2 = M.eRk M.E)

def TutteFormalization.TutteAdjacent {α : Type u_1} (M : Matroid α) (H K : Set α) : Prop

def:tutte-path: the condition on two consecutive vertices. Hyperplane conditions are imposed on every vertex by TuttePath.

Equations

• TutteFormalization.TutteAdjacent M H K = (H ≠ K ∧ TutteFormalization.Indecomposable M (H ∩ K) ∧ TutteFormalization.CorankTwo M (H ∩ K))

structure TutteFormalization.TuttePath {α : Type u_1} (M : Matroid α) : Type u_1

def:tutte-path: length counts edges, and there are length + 1 vertices. i.castSucc and i.succ index positions i and i+1. Length zero is allowed; there is no injectivity requirement or restriction on nonconsecutive repetitions.

• length : ℕ

  Number of edges.

• vertex : Fin (self.length + 1) → Set α

  The nonempty finite sequence of hyperplanes.

• isHyperplane (i : Fin (self.length + 1)) : IsHyperplane M (self.vertex i)
• adjacent (i : Fin self.length) : TutteAdjacent M (self.vertex i.castSucc) (self.vertex i.succ)

def TutteFormalization.TuttePath.origin {α : Type u_1} {M : Matroid α} (p : TuttePath M) : Set α

The first vertex.

Equations

• p.origin = p.vertex 0

def TutteFormalization.TuttePath.terminus {α : Type u_1} {M : Matroid α} (p : TuttePath M) : Set α

The last vertex.

Equations

• p.terminus = p.vertex (Fin.last p.length)

def TutteFormalization.TuttePath.On {α : Type u_1} {M : Matroid α} (p : TuttePath M) (F : Set α) : Prop

Every vertex contains F; this does not assert that F is the carrier.

Equations

• p.On F = ∀ (i : Fin (p.length + 1)), F ⊆ p.vertex i

def TutteFormalization.TuttePath.Off {α : Type u_1} {M : Matroid α} (p : TuttePath M) (Γ : Set (Set α)) : Prop

Every vertex lies outside the cut.

Equations

• p.Off Γ = ∀ (i : Fin (p.length + 1)), p.vertex i ∉ Γ

def TutteFormalization.TuttePath.carrier {α : Type u_1} {M : Matroid α} (p : TuttePath M) : Set α

The carrier from def:tutte-path. The index type is always nonempty.

Equations

• p.carrier = ⋂ (i : Fin (p.length + 1)), p.vertex i