Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Blueprint for the Formalization of Seymour's Matroid Decomposition Theorem

Ivan Sergeev, Martin Dvorak, Cameron Rampell, Mark Sandey, Pietro Monticone

Abstract

This document is a blueprint for the formalization in Lean of the structural theory of regular matroids underlying Seymour's decomposition theorem. We present a modular account of regularity via totally unimodular representations, show that regularity is preserved under $1$-, $2$-, and $3$-sums, and establish regularity for several special classes of matroids, including graphic, cographic, and the matroid $R_{10}$. The blueprint records the logical structure of the proof, the precise dependencies between results, and their correspondence with Lean declarations. It is intended both as a guide for the ongoing formalization effort and as a human-readable reference for the organization of the proof.

A Blueprint for the Formalization of Seymour's Matroid Decomposition Theorem

Abstract

This document is a blueprint for the formalization in Lean of the structural theory of regular matroids underlying Seymour's decomposition theorem. We present a modular account of regularity via totally unimodular representations, show that regularity is preserved under -, -, and -sums, and establish regularity for several special classes of matroids, including graphic, cographic, and the matroid . The blueprint records the logical structure of the proof, the precise dependencies between results, and their correspondence with Lean declarations. It is intended both as a guide for the ongoing formalization effort and as a human-readable reference for the organization of the proof.
Paper Structure (16 sections, 50 theorems, 44 equations)

This paper contains 16 sections, 50 theorems, 44 equations.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Total Unimodularity
  4. Pivoting
  5. Vector Matroids
  6. Regular Matroids
  7. Regularity of 1-Sum
  8. Regularity of 2-Sum
  9. Regularity of 3-Sum
  10. Definition
  11. Canonical Signing
  12. Properties of Canonical Signing
  13. Proof of Regularity
  14. Special Matroids
  15. Regularity of Cographic Matroids
  16. ...and 1 more sections

Key Result

Lemma 4

Matrix.IsTotallyUnimodular Let $A$ be a TU matrix. Suppose rows of $A$ are multiplied by $\{0, \pm 1\}$ factors. Then the resulting matrix $A'$ is also TU.

Theorems & Definitions (127)

  • Definition 1
  • Definition 2
  • Definition 3
  • Lemma 4
  • Lemma 5
  • proof
  • Definition 6
  • Lemma 7
  • proof
  • Definition 8
  • ...and 117 more