Alphabeta Math
CorollaryStatement: 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.

The maximum matching from XX has size ∣X∣−max⁡S⊆X(∣S∣−∣N(S)∣)|X|-\max_{S\subseteq X}(|S|-|N(S)|)

Statement

Let (X,Y)(X,Y) be a finite bipartite graph and put d:=max⁡S⊆X(∣S∣−∣N(S)∣).d:=\max_{S\subseteq X}\bigl(|S|-|N(S)|\bigr). Then the greatest number of vertices of XX saturable by a matching is ∣X∣−d|X|-d.

Facts & Assumptions

Given: A finite bipartite graph with parts (X,Y)(X,Y) and the displayed dd.

[L1]

Hall's theorem supplies a matching saturating a finite left part exactly under Hall's inequalities (Hall's marriage theorem for a finite bipartite graph).

Proof

technique · direct
1.1

Any matching saturating rr vertices of XX leaves at least ∣S∣−∣N(S)∣|S|-|N(S)| vertices of every S⊆XS\subseteq X unmatched, so r≤∣X∣−dr\le|X|-d.

given
1.2

Adjoin dd new right vertices, adjacent to every x∈Xx\in X; then every S⊆XS\subseteq X has at least ∣N(S)∣+d≥∣S∣|N(S)|+d\ge|S| neighbours, so [L1] gives a matching saturating XX in the enlarged graph.

L1
2.1

At most dd of its matching edges use new vertices, so deleting those edges leaves a matching of the original graph saturating at least ∣X∣−d|X|-d vertices of XX.

step 1.2
3.1

The upper bound in step 1.1 and lower bound in step 2.1 establish the formula.

step 1.1step 2.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 21 results over 13 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