Theorem 1 — a matching is maximum iff no alternating chain connects two neutral points

Let $G = (X, U)$ be a finite simple graph and $V \subseteq U$ a matching. Call the edges of $V$ strong and the other edges weak; a vertex met by no strong edge is neutral, and an alternating chain is a walk that does not use the same edge twice and in which, of any two consecutive edges, one is strong and the other weak. Then

Here "maximum" means that no matching of $G$ has more edges than $V$.

This is Berge's characterization of maximum matchings by augmenting chains. It turns the global optimality of a matching into a local, checkable condition, and it is the basis of the augmenting-path algorithms for maximum matching in general graphs, notably Edmonds' blossom algorithm.

Formalization Note The graph is a finite Mathlib SimpleGraph, the matching is a subgraph with IsMatching, and its size is the number of its edges. Alternating chains are trails (no repeated edge; vertices may repeat), and alternation is required of consecutive edges only. The endpoints are required to be distinct, as in the paper's proof ("a neutral point $a'$ different from $a$"); otherwise the one-vertex chain at any neutral point would count. No connectedness or nonemptiness hypothesis is assumed.