LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-02

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Switching along an augmenting path increases a matching by one edge

Statement

If $P$ is an $M$ -augmenting path in a finite graph, then $M^{'} : = M △ E (P)$ is a matching and $∣ M^{'} ∣ = ∣ M ∣ + 1$ .

Facts & Assumptions

Given: A matching $M$ and an $M$ -augmenting path $P$ .

[F1]

An augmenting path alternates between edges outside and inside $M$ , begins and ends outside $M$ , and has exposed endpoints (Alternating and augmenting paths relative to a matching).

Proof

technique · constructive

1.1

Along $P$ there is one more edge outside $M$ than inside $M$ , and every internal vertex of $P$ is incident with precisely one edge of $M \cap E (P)$ .

F1construct

1.2

Replacing the $M$ -edges of $P$ by its non- $M$ edges leaves every internal vertex incident with one new matching edge, and its exposed endpoints incident with one; all edges away from $P$ are unchanged, so $M^{'}$ is a matching.

2.1

The replacement deletes $∣ M \cap E (P) ∣$ edges and adds $∣ M \cap E (P) ∣ + 1$ edges, hence $∣ M^{'} ∣ = ∣ M ∣ + 1$ .

step 1.1discharge-construct∎

Remarks

The use of symmetric difference is literal: it deletes the old matching edges on $P$ and inserts the new ones, with no choice of any further edges.

Depends on

Used by

Berge's theorem: a matching is maximum if and only if it has no augmenting path Theorem

Dependency tree · two levels

5 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

M. Goemans, Lecture notes on bipartite matching (standard reference, not scraped)