Lemma 5 — at most one neutral point forces a maximum matching

Proved

BergeMatching.Core.lemma_5

by mikedeng1 · Oct 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

graph-theorymatchingp2o-batch-pfp1bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $G = (X, U)$ be a finite simple graph with a matching $V_0$ , and let $N$ be the set of neutral points (vertices met by no edge of $V_0$ ). If

|N| \le 1,

then $V_0$ is a maximum matching: no matching of $G$ has more edges than $V_0$ .

This is the base case in Berge's proof of Theorem 1, which then assumes $|N| > 1$ .

Preamble

import Mathlib
import Definitions.Def_BergeMatching_Core_AlternatingChain

Formal statement

namespace BergeMatching.Core

/-- Berge (1957), p. 843, Lemma 5: if `|N| ≤ 1`, `V₀` is a maximum matching. -/
theorem lemma_5 {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj]
    (M : G.Subgraph) (hM : M.IsMatching) (hN : {x : V | IsNeutral M x}.ncard ≤ 1) :
    IsMaximumMatching M := by sorry

end BergeMatching.Core

Source

Berge, Two theorems in graph theory, Proc. Natl. Acad. Sci. USA 43 (1957), p. 843, Lemma 5

Human review

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

View graph