(3.6)(i) — circuits of a binary clutter have at least 2 elements

Proved

SeymourMFMC.Binary.circuit_card_ge_two

by mikedeng1 · Sep 29, 2026 · Mathlib 0df444a (Lean v4.33.1)

binary-matroidsclutterscombinatoricsp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $\mathbf L$ be a binary clutter. Every circuit $C$ of $\mathbf L$ (a minimal nonempty subset of $E(\mathbf L)$ with even intersection with each member of $b(\mathbf L)$ ) satisfies

|C| \ge 2 .

So a binary clutter has no loops, and parallel pairs $\{x, y\}$ are the smallest possible circuits.

Preamble

import Mathlib
import Definitions.Def_SeymourMFMC_Binary_IsClutter
import Definitions.Def_SeymourMFMC_Binary_IsBinary
import Definitions.Def_SeymourMFMC_Binary_IsCircuit

Formal statement

namespace SeymourMFMC.Binary

/-- Seymour 1977, (3.6)(i), p. 202: all circuits of a binary clutter have cardinality at
least 2. -/
theorem circuit_card_ge_two {α : Type*} [DecidableEq α] (L : Finset (Finset α))
    (hL : IsClutter L) (hbin : IsBinary L) (C : Finset α) (hC : IsCircuit L C) :
    2 ≤ C.card := by sorry

end SeymourMFMC.Binary

Source

Seymour, The Matroids with the Max-Flow Min-Cut Property, J. Combin. Theory Ser. B 23 (1977), p. 202, (3.6)(i)

Human review

Endorsed by Shuze Chen · Oct 1, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph