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.
Matchings, Covers, Menger and Network Flows — Examples
1 · Prerequisites
- Binary Operations, Monoids, Groups and Subgroups
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Countability and Uncountability
- Eulerian and Hamiltonian Graphs
- Finite Counting, Factorials and Binomial Coefficients
- Foundations of the Real Numbers for Analysis
- Graphs, Walks and Connectivity
- Matchings, Covers, Menger and Network Flows
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- Roots, Rational Powers, and Classical Inequalities
- The ZFC Axioms and the Basic Set Constructions
2 · Summary
3 · Logical flowchart
4 · Definitions, theorems and proofs
None yet.
5 · Examples, counterexamples and false statements
The middle edge of is a maximal matching but the two end edges form a larger matching
Counterexample
Let have consecutive vertices and let . Then is maximal but not maximum: is a matching of size two.
Facts & Assumptions
Given: The path and its middle-edge matching .
A matching is maximum exactly when it has no augmenting path (Berge's theorem: a matching is maximum if and only if it has no augmenting path).
Verification
Verification technique: direct.
The two remaining edges and each meet , so neither can be added to ; hence is maximal.
The path is -augmenting, and [L1] therefore also shows that is not maximum.
Independently, is a disjoint two-edge matching, so the maximal and maximum notions differ in this finite path.
Three left vertices with only two collective neighbours fail Hall's condition and cannot all be matched
Example
Take left part , right part , and all six possible edges between the two parts. This graph has no matching saturating .
Facts & Assumptions
Given: The displayed finite bipartite graph.
A finite bipartite graph has a matching saturating its left part exactly when Hall's condition holds (Hall's marriage theorem for a finite bipartite graph).
Verification
Verification technique: direct.
For , the neighbourhood is , so .
Thus Hall's condition fails, and [L1] proves that no matching can saturate all three left vertices.
The two available right vertices also show directly that any matching has at most two edges.
A three-set family with an explicit system of distinct representatives
Example
For , , and , the assignment , , is an SDR.
Facts & Assumptions
Given: The three finite sets .
A family with finite index set and finite union has an SDR exactly when every indexed subfamily has union at least as large as its index set (A finite family has an SDR if and only if every subfamily has a union at least as large as its index set).
Verification
Verification technique: constructive.
Each singleton union has size two, each two-set union is , and the three-set union is ; the Hall union inequalities all hold.
By [L1], the family has an SDR.
The displayed assignment chooses an element of each and has three distinct values, so it is the promised SDR.
has , so König's equality needs bipartiteness
Counterexample
In the triangle , every matching has at most one edge, while every vertex cover has at least two vertices. Hence .
Facts & Assumptions
Given: The complete graph on three vertices.
König's equality applies to finite bipartite graphs (König's theorem: for every finite bipartite graph).
Verification
Verification technique: direct.
Any two edges of share a vertex, so a matching has at most one edge; any one edge gives .
Deleting one vertex leaves an edge, so one vertex is not a cover; two vertices cover all edges, giving .
Thus , and [L1] shows precisely why this does not contradict König's theorem: is not bipartite.
This triangle is a finite witness that bipartiteness is a necessary hypothesis for the equality.
A four-vertex integral network with an exhibited maximum flow and minimum cut of value five
Example
Let the vertices be , with labelled arcs and capacities The flow with values in that order has value five and is maximum.
Facts & Assumptions
Given: The displayed finite integral network and flow .
Finite integral max-flow min-cut equates a maximum flow value and a minimum cut capacity (Ford-Fulkerson terminates for finite integer capacities and proves max-flow min-cut with an integral maximum flow).
Verification
Verification technique: direct.
At , incoming flow equals outgoing flow , and at , incoming flow equals outgoing flow ; every arc value is within its capacity.
The flow value is , while the cut has capacity .
By [L1], the exhibited feasible flow and cut of common value five are respectively maximum and minimum.
This network therefore has max-flow value and min-cut capacity both equal to five.
In , the two vertices in the two-part have three internally disjoint paths and a minimum separator of size three
Example
Let have two-part and three-part . The paths for are internally vertex-disjoint, and is a minimum - separator.
Facts & Assumptions
Given: The displayed complete bipartite graph .
For nonadjacent terminals, finite vertex Menger equates maximum internally disjoint paths and minimum vertex separators (Menger's theorem: the finite directed and undirected arc, edge and nonadjacent-vertex forms).
Verification
Verification technique: direct.
The three paths , , and have distinct internal vertices.
Deleting all three destroys every - path, while deleting fewer leaves some and its two-edge path.
The terminals are nonadjacent, so [L1] agrees with the direct calculation: both the packing and separator numbers equal three.
This is a concrete equality case for the local undirected vertex form.