Lax Lean Archive

Consecutive Ones Implies Total Unimodularity

Lax496464.ConsecutiveOnes · concepts/Lax496464/ConsecutiveOnes.lean · lax-496464

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    A matrix of zeros and ones has the consecutive ones property when the ones in each row occupy a consecutive block of columns. Such a matrix is totally unimodular: every square submatrix has determinant 00, 11 or −1-1.

    This is the theorem of Fulkerson and Gross, and it is what makes the integer program of Section 6.2 solvable as a linear program.

    Concept map
    1 concept; 1 descendant hidden
    100%
    Proven claimThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    In the paper

    • page 6 of this submission's paper

    Lean source view on GitHub

    1import Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
    2
    3/-!
    4---
    5title: Consecutive Ones Implies Total Unimodularity
    6type: theorem
    7---
    8A matrix of zeros and ones has the *consecutive ones property* when the ones in each row
    9occupy a consecutive block of columns. Such a matrix is *totally unimodular*: every
    10square submatrix has determinant 00, 11 or −1-1.
    11
    12This is the theorem of Fulkerson and Gross, and it is what makes the integer program of
    13Section 6.2 solvable as a linear program.
    14
    15# Formalization Notes
    16
    17The property is stated as a closure condition — if a row has a one at two columns then it
    18has a one at every column between them — rather than through an ordering of the columns
    19supplied from outside. The two agree once the columns are ordered, and the closure form
    20is what a matrix built from intervals satisfies by construction and what a proof uses.
    21
    22The columns are only required to carry an order, not to be finite or linearly ordered:
    23nothing below needs more. Total unimodularity is mathlib's, so the conclusion is the
    24standard one and is available to whatever consumes it.
    25
    26The paper cites this result. It is proved here rather than assumed, since neither it nor
    27anything equivalent is in the background library, and a hardness or tractability claim
    28resting on it should not rest on an axiom that could as well be false.
    29-/
    30
    31namespace Lax496464.ConsecutiveOnes
    32
    33/-- The ones of each row occupy a consecutive block of columns. -/
    34def HasConsecutiveOnes {m n : Type*} [LE n] (A : Matrix m n ℤ) : Prop :=
    35 (∀ r c, A r c = 0 ∨ A r c = 1) ∧
    36 ∀ r c₁ c c₂, c₁ ≤ c → c ≤ c₂ → A r c₁ = 1 → A r c₂ = 1 → A r c = 1
    37
    38/-- **Fulkerson–Gross.** A matrix with the consecutive ones property is totally
    39unimodular. -/
    40axiom isTotallyUnimodular {m n : Type*} [LinearOrder n] {A : Matrix m n ℤ}
    41 (h : HasConsecutiveOnes A) : A.IsTotallyUnimodular
    42
    43end Lax496464.ConsecutiveOnes
    44
    Show Proof
    Formalization Notes

    The property is stated as a closure condition — if a row has a one at two columns then it has a one at every column between them — rather than through an ordering of the columns supplied from outside. The two agree once the columns are ordered, and the closure form is what a matrix built from intervals satisfies by construction and what a proof uses.

    The columns are only required to carry an order, not to be finite or linearly ordered: nothing below needs more. Total unimodularity is mathlib's, so the conclusion is the standard one and is available to whatever consumes it.

    The paper cites this result. It is proved here rather than assumed, since neither it nor anything equivalent is in the background library, and a hardness or tractability claim resting on it should not rest on an axiom that could as well be false.

    Builds on

    none

    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…