Assigning distinct resources under compatibility constraints

A finite allocation problem begins with a list of permitted choices. Each recipient may use some resources but not others, and a resource may be assigned at most once. Knowing that every recipient has an available resource is insufficient: several recipients may all depend on the same small pool. A useful theorem must decide whether the compatibility pattern permits all requirements to be met simultaneously.

This mission develops the matching results in the chapter on systems of distinct representatives in D. Yogeshwaran's Discrete Mathematics—Lecture Notes, §6.1. Its endpoint allows different recipients to require different numbers of resources. The classical one-resource problem, the regular-graph case, and the case in which a bounded number of assignments may remain unfilled are retained as separate source-numbered results. The project concerns established theorems, not a new conjecture about the existence of matchings.

Graphs, matchings, and demands

A finite simple graph consists of a finite set of vertices and unordered pairs of distinct vertices called edges. A bipartition is a pair of disjoint sets $L,R$ whose union is the vertex set, such that every edge joins a vertex in $L$ to a vertex in $R$. The left vertices represent recipients and the right vertices represent resources. An edge records that the resource is permitted for that recipient. These graph conventions follow Definition 1.1 of the notes.

For a vertex $x$, the neighbor set $N_G(x)$ contains the vertices joined to $x$. For a set $S$ of vertices, write $N_G(S)=\bigcup_{x\in S}N_G(x)$. A matching is an edge set in which no vertex is used twice. It is complete on $L$ if every left vertex is used, and perfect if every vertex is used. A subgraph may retain selected edges of the original graph. Its degree $\deg_H(x)$ counts the retained neighbors of $x$.

A demand is a natural number $d_x$ attached to each $x\in L$. Unlike a complete ordinary matching, the capstone may assign more than one resource to a recipient. Resources still have capacity one, and a demand may be zero.

Formalization targets

The ordinary matching criterion is Theorem 6.2:

$$\exists\text{ a complete matching on }L \quad\Longleftrightarrow\quad \forall S\subseteq L,\quad |S|\le |N_G(S)|.$$

The development also includes Exercise 6.3, asserting that a $k$-regular bipartite graph has a perfect matching when $k>0$. Proposition 6.4 states the quantitative deficit version:

$$\bigl(\forall S\subseteq L,\ |S|-d\le |N_G(S)|\bigr) \quad\Longrightarrow\quad \exists M\text{ matching},\quad |L|-d\le |E(M)|, \qquad d\ge1.$$

The capstone is the prescribed-degree equivalence of Exercise 6.5:

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

This statement retains the entire demand function and does not fix a uniform demand, restrict demands to positive values, or replace integral selections by real weights.

The set-theoretic interface is Corollary 6.9. A finite family of arbitrary sets $(A_i)_{i\in I}$ has a system of distinct representatives, meaning an injective choice $f(i)\in A_i$, exactly when

$$\forall J\subseteq I,\qquad |J|\le \left|\bigcup_{i\in J}A_i\right|.$$

Only the index family is finite; the sets themselves may be infinite.

What the development provides

The demand criterion characterizes feasibility entirely in terms of the original compatibility graph and the requested multiplicities. Its necessity identifies an obstruction to any assignment, while its sufficiency asserts that no other obstruction exists. The deficit theorem gives a quantitative statement when complete coverage is unavailable. The regular case gives a distinct consequence for graphs described through their degrees, rather than through a separately supplied collection of neighborhood inequalities. These are the respective contents of Exercises 6.3 and 6.5 and Proposition 6.4.

Mathlib already provides finite-family and graph versions of Hall's theorem in its Hall development and graph interface. The source-aligned development therefore reuses established infrastructure. Its additional work consists of connecting exact graph degrees and edge counts to the source statements, retaining the deficit and zero-demand cases, and supplying an arbitrary-set representatives interface. Local proofs of the five theorem statements have been checked in Lean 4.29.0-rc3 with Mathlib 777aaa6.

Where exact formalization is delicate

Independent local choices do not guarantee a matching: different choices can collide at one resource. Replacing distinct selections by nonnegative real allocations would change the conclusion. Counting total demand alone also misses obstructions carried by proper subsets of recipients.

Several representation issues matter even after the mathematics is known. A left-saturating matching need not be perfect. A subgraph's vertex set may omit isolated ambient vertices. Cardinality conventions for infinite sets can turn a superficially plausible formula into a different assertion. Finally, a theorem that assumes all neighborhood inequalities has not established those inequalities merely because a graph is regular. The individual interfaces must distinguish these obligations rather than hide them inside a definition.

Formalization scope

The graph results use finite vertex types and native SimpleGraph and Subgraph objects. Both disjointness and coverage of the bipartition are explicit. Local-finiteness instances supply finite neighbor enumerations; they impose no further restriction on finite graphs. The complete-matching predicate combines the native matching condition with inclusion of the prescribed vertex set.

Degrees in the capstone are cardinalities of finite subgraph neighbor sets. The deficit conclusion counts unordered subgraph edges. Natural subtraction is truncated at zero, an equivalent convention for these nonnegative cardinality lower bounds. Empty graphs, empty index families, and zero demands remain admissible. In the representatives theorem, arbitrary sets are measured by extended cardinality; infinity is never replaced by zero.

The reusable outputs are the source-aligned graph statements, the complete-matching interface, the prescribed-degree equivalence, and the arbitrary-set representatives criterion. Equivalent proofs and clearer reusable interfaces are within scope. Placeholder conclusions, extra assumptions that exclude the difficult cases, and fractional substitutes for the integral capstone are not.

Selected references

• D. Yogeshwaran, Discrete Mathematics—Lecture Notes, Indian Statistical Institute Bangalore, HTML edition generated 2025. Chapter 6.1; graph conventions.
• The mathlib community, Mathlib 4, revision 777aaa6, 2026. Finite-family Hall theorem; native graph Hall theorem.