LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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\mathbin{\triangle}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 · next 3 levels

Direct dependencies and their dependencies through the next three levels: 13 results over 10 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

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