Exercise 6.5 — Hall's criterion with prescribed left degrees

Proved

YogeshwaranDM.capacitated_hall_iff

by wamlart · Sep 6, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

graph-theoryhall-theoremmatchings

Exercise 6.5 — Hall's criterion with prescribed left degrees. Let $G$ be a finite simple bipartite graph with vertex partition $L\sqcup R$ . For every $x\in L$ , prescribe a demand $d_x\in\mathbb N$ , allowing zero. Then

\begin{split} &\exists H\subseteq G:\ \bigl(\forall x\in L,\ \deg_H(x)=d_x\bigr) \quad\land\quad \bigl(\forall y\in R,\ \deg_H(y)\le1\bigr)\\ &\hspace{20mm}\Longleftrightarrow\quad \forall S\subseteq L,\ \sum_{x\in S}d_x\le |N_G(S)|. \end{split}

Formalization note. The witness is an actual native subgraph, not a fractional allocation or an assumed matching. A vertex's degree is the cardinality of its neighbor set in that subgraph, with degree zero outside the subgraph's vertex set. All finite cardinalities and all demands are natural numbers.

Preamble

import Mathlib.Combinatorics.Hall.Finite
import Mathlib.Combinatorics.SimpleGraph.Hall
import Mathlib.Tactic

set_option autoImplicit false
open scoped BigOperators

Formal statement

namespace YogeshwaranDM

theorem capacitated_hall_iff {V : Type*} [Fintype V] [DecidableEq V] (G : SimpleGraph V)
    [G.LocallyFinite] (L R : Set V) (hG : G.IsBipartiteWith L R)
    (hcover : L ∪ R = Set.univ) (d : L → ℕ) :
    (∃ H : G.Subgraph, (∀ x : L, (H.neighborSet x).ncard = d x) ∧
      ∀ y ∈ R, (H.neighborSet y).ncard ≤ 1) ↔
      ∀ S : Finset L, ∑ x ∈ S, d x ≤ (S.biUnion (fun x => G.neighborFinset x)).card := by sorry

end YogeshwaranDM

Source

D. Yogeshwaran, Discrete Mathematics—Lecture Notes, Indian Statistical Institute Bangalore, HTML edition generated May 9, 2025, Exercise(A) 6.5, https://www.isibang.ac.in/~d.yogesh/Course_Notes/DM1/Ch6.S1.html

Read-back

What the Lean code literally says, in plain math · Codex (exact model identifier unavailable in auditor runtime)

For every finite type $V$ equipped with a finite enumeration and decidable equality, every simple undirected loopless graph $G$ on $V$ equipped with finite enumerations of all its neighbor sets, every pair of sets $L,R \subseteq V$ , and every function $d:L\to\mathbb N$ , assume that $L$ and $R$ are disjoint, every edge of $G$ has one endpoint in each part, and $L \cup R=V$ . Then the following assertions are equivalent: there exists a subgraph $H$ of $G$ such that, for every vertex $x \in L$ , the set of neighbors of $x$ in $H$ has cardinality exactly $d(x)$ , and, for every vertex $y \in R$ , the set of neighbors of $y$ in $H$ has cardinality at most one; and, for every finite set $S$ of elements of $L$ , $\sum_{x\in S}d(x) \leq |N_G(S)|$ , where $N_G(S)$ is the finite union of the sets of neighbors in $G$ of the vertices of $S$ . A subgraph consists of a chosen vertex set and some edges of $G$ , with both endpoints of each chosen edge in the chosen vertex set. The neighbor sets in the first assertion are defined for every vertex of $V$ , including a vertex omitted from $H$ , which then has no neighbors in $H$ . Consequently a vertex $x\in L$ with positive $d(x)$ must belong to $H$ , but a vertex with zero demand and a vertex of $R$ with no chosen incident edge may be omitted or included as an isolated vertex. The assertion does not require $H$ to be spanning, does not require every vertex of $H$ to have exactly one neighbor, and does not require a unique witness. There is no positivity hypothesis on $d$ . The sum counts each element of $S$ once, the union counts each distinct neighbor once, and the assumptions place that union in $R$ . All cardinalities are ordinary finite counts: the natural-number cardinalities used for the neighbor sets cannot take their general infinite-set value of zero because $V$ is finite. The sum over the empty set and its neighbor-union cardinality are both zero. Empty $V$ and empty parts are included; if $L$ is empty, both assertions hold using the empty subgraph, and if $R$ is empty, both assertions hold exactly when every demand is zero. More generally, when $d$ is identically zero, the empty subgraph witnesses the first assertion and every inequality in the second holds. Infinite vertex types are not included.

Human review

Endorsed by Shuze Chen · Sep 6, 2026
Endorsed by wamlart · Sep 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph