Prove2Me

Section 1, p. 193 — Q₆ is not Mengerian

Proved
SeymourMFMC.Binary.Q6_not_mengerian

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

clutterscombinatoricsmax-flow-min-cutp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1

The clutter

Q6={{1,3,5},{1,4,6},{2,3,6},{2,4,5}}Q_6 = \{\{1,3,5\}, \{1,4,6\}, \{2,3,6\}, \{2,4,5\}\}

is not Mengerian: there is a weight map w:E(Q6)→Z+w : E(Q_6) \to \mathbb Z^+ for which no integral packing q:Q6→Z+q : Q_6 \to \mathbb Z^+ satisfying the capacity constraints ∑A∋xq(A)≤w(x)\sum_{A \ni x} q(A) \le w(x) reaches the minimum weight of a member of b(Q6)b(Q_6).

The paper states this together with the fact that Q6Q_6 has the weak max-flow min-cut property. Only the "not Mengerian" half is formalized, as the weak property is not needed. With minor-closedness (2.3), it gives the "only if" direction of the main theorem.

Preamble
import Mathlib
import Definitions.Def_SeymourMFMC_Binary_Q6
import Definitions.Def_SeymourMFMC_Binary_IsMengerian
Formal statement
namespace SeymourMFMC.Binary

/-- Seymour 1977, Section 1, p. 193: the clutter `Q₆` is not Mengerian. -/
theorem Q6_not_mengerian : ¬ IsMengerian Q6 := by sorry

end SeymourMFMC.Binary
Source
Seymour, The Matroids with the Max-Flow Min-Cut Property, J. Combin. Theory Ser. B 23 (1977), p. 193, Section 1
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