Equal-capacity bipartite matching
Random choice.
Better matching.
When every bin has the same capacity and each job gets an independent, uniformly chosen feasible set, fresh random choices match at least as many jobs in distribution as a shared priority ranking.
Pr(MRV ≥ K) ≥ Pr(MRANKING ≥ K)
Every finite size. Every positive integer capacity.
Every matching-size threshold K.
This is a comparison of probability distributions over random graphs and choices. It does not say that RANDOM-VERTEX wins on every individual run.
How the proof fits together
Two branches. One comparison.
Choose a result to read its statement and see what its proof uses. An arrow points from an ingredient to a result that uses it.
Selected resultUsed directly
Six supporting results, the coupling argument, and the main conclusion. Numbers match the manuscript; Theorem 8 states the formal source-model version of the conclusion. The arrows show the main mathematical dependencies.
01 / 07
The theorem
Compare the whole distribution.
RANDOM-VERTEX chooses uniformly from the current job’s available neighbors. RANKING uses one common bin order for every job. Both reject a job only when none of its neighbors has room.
The claim is stronger than an average advantage: for any target K, the probability of accepting at least K jobs is no smaller with RANDOM-VERTEX.
Explore a small instance. Every feasible neighborhood and response is included in finite probability sums; this is not a sampled simulation. Values on screen are rounded.
What the proof must explainWhy can concentrating choices on a shared priority make future acceptance harder?
Open the formal theorem ↗RANDOM-VERTEXRANKING
Each point is Pr(M ≥ K). The job order is fixed in this example; the theorem also allows averaging over an independent random arrival order.
Lemma · normalized coefficients
One calculation gives two inequalities.
Look at choices involving two bins. Every row prefers the first bin: uj ≥ vj ≥ 0. Expand the product ∏(ujX + vjY), then divide its kth coefficient by binom(t,k).
gk = [XkYt−k] ∏(ujX + vjY) / binom(t,k)
The resulting sequence is increasing and convex: its first and second differences are nonnegative.
Why are the differences nonnegative?
Write gk as the average over permutations of k factors u and t−k factors v. A first difference replaces one v with u−v. A second difference replaces two. Every factor is nonnegative, and symmetry makes the two middle terms agree.
Used twiceConvexity controls concentration after balancing. Monotonicity orders the chance that each bin reaches its cap.
Coefficient lemma in Lean ↗Four different choice rows share the same order. At zero preference the sequence is flat. Increasing preference makes the positive differences visible.
Association + concentration theorem
Condition on staying below the cap.
Distribute r choices among b bins, then condition on every load being at most q. Uniform choices give the reference mass μ(x) proportional to 1/∏xi!.
For commonly ordered choice rows, symmetrize bin labels and write the conditioned mass as μ(x)L(x). The two-bin convexity lemma shows that moving a unit from a fuller bin to a less full bin cannot increase L.
The association theorem says that two symmetric quantities increasing with concentration have nonnegative covariance under μ. Apply it to L and an observable F:
EorderedF − EμF = Covμ(F,L) ≥ 0.
Where does association come from?
The written proof applies Cohen–Sackrowitz’s conditional association theorem to the truncated factorial carrier. The Lean proof establishes the required rational specialization directly, by induction on the common cap. The small display illustrates the inequality; the general statement comes from the proof.
What we gainAny symmetric concentration-increasing statistic has at least its uniform-reference expectation.
Concentration theorem in Lean ↗b = 3 bins · r = 4 choices · F(x) = Σ x²
Each column groups all permutations of a load vector. From left to right, loads become more balanced. L is the density of the conditioned, symmetrized law relative to μ; here EμL = 1.
Corollary · saturation hazard
How likely is the next choice to fill a bin?
Take capacity C = q+1. A bin with current load q becomes full after one more choice. Its boundary probability is pi = Pr(Ni = q | all loads ≤ q).
The coefficient lemma orders these boundary probabilities in the same direction as the preference rows. An ordered next choice therefore hits the boundary at least as often as a uniform next choice.
Then apply the concentration theorem to B(x), the number of bins at the cap:
ordered next hazard ≥ EorderedB / b ≥ EμB / b = h.
What we gainThe uniform reference gives a lower bound on the probability of creating another full bin. This is the mark comparison used in the coupling.
Saturation comparison in Lean ↗The old rows and cap come from the previous step. Zero next-choice preference makes the first inequality an equality. Zero old preference makes both inequalities equalities.
Lemma · the refined history law
The cap is the entire remaining constraint.
At an accepted count K, record which bins are full, the jobs assigned to them, and all accept/reject indicators. Leave destinations in the nonfull bins unspecified.
Every residual assignment below the cap produces the same recorded full-bin history. Its weight factors into choice-row weights times a constant. Thus the residual law is a product law conditioned on the cap.
Those conditioned choices need not stay independent. The next destination is independent of them inside each fixed refinement, which is all the hazard argument needs.
What we gainThe abstract capped-load inequality now applies to the actual matching process. Averaging over refinements gives the bound conditional on the accepted-count state.
History-fiber bijection in Lean ↗Capacity C = 3 · six accepted jobs · A fills at job 6
Fixed: jobs 2, 4, 6 → A. Free: jobs 1, 3, 5 → B or C.
Six of the eight assignments leave B and C nonfull. The all-B and all-C assignments are excluded precisely by the residual cap q = 2. Rejections and assignments to full bins are fixed data in the general argument.
Coupling · induction on accepted jobs
Use the same random number to preserve order.
The state after K acceptances records the arrival index σK and the number a of full bins. A degree-d job is rejected with probability binom(a,d) / binom(m,d), regardless of partial loads.
Starting earlier and having fewer full bins makes the next acceptance no later in stochastic order. A shared quantile couples the two waiting times. If old full-bin counts agree, the hazard lemma orders their zero-or-one increments. If they differ, increments of at most one cannot reverse their order.
Why is no Markov assumption needed?
At each level we couple the actual conditional next-state distributions given the current state. Summing against the current coupling recovers both next marginal laws by total probability. We construct couplings of one-time state laws; we do not claim to reproduce the original complete path laws.
What we gainAt every acceptance level, RV reaches the level no later and has no more full bins. A never-reached level is an absorbing state above all finite ones.
Actual transition coupling in Lean ↗m = 4 · C = 3 · K = 6 · start at arrival 6 for RV, 8 for RK.
Future degrees, arrivals 7–12: 1, 2, 1, 2, 1, 2.
The waiting laws use the exact binomial formula. For equal old counts, the mark display uses h and an illustrative admissible p = h + 0.2(1−h). It demonstrates the coupling for p ≥ h; p is not a computed RANKING conditional probability.
The final implication
Reaching K is the same as matching at least K.
{M ≥ K} = {σK ≤ n}
The coupled hitting-time order gives every matching-size tail inequality. Relabeling bins preserves uniform neighborhoods and the number accepted. Finally, average over the independent uniform arrival and priority permutations.
This proves Arnosti’s full RANDOM-VERTEX versus RANKING conjecture in the stated random-neighborhood model. Equal capacities are part of the original conjecture. The final Lean statement has no unproved comparison, association, coupling or Markov premise.
Where it can helpFor jobs or requests with uniformly random feasible sets and identical resource capacities, the theorem justifies fresh random tie-breaking over a persistent global priority. Correlated feasibility, unequal capacities, and fixed adversarial graphs require separate analysis.
Inspect the complete source-model theorem ↗The two branches meet
The two-bin identity supplies convexity for the concentration comparison and monotonicity for the next-choice comparison. Together they give the saturation bound.
The history lemma transfers that bound to the algorithms. Coupling then turns the local transition comparison into an inequality for every matching-size tail.
Revisit the proof dependency map ↑Select any result on the map to see its direct prerequisites and how each one is used. The linked manuscript and Lean sources contain the general arguments.
Check the result
A proof you can inspect.
The full source-model theorem was checked with Lean 4.34.0 in Azure. The record covers 91 modules, 714 named theorems and 929 audited declarations. Its axiom dependencies are propext, Classical.choice and Quot.sound.
No admitted goals, custom axioms, unsafe declarations or native_decide occur in the positive proof. A deliberately false control was rejected. The package includes source hashes, compiler logs and a metadata checker.
VibeMathed lists the result as Candidate, Lean-checked. A full independent proof and formal statement audit remains open. The kernel checks the formal statement; the manuscript and review guide explain its correspondence with the source conjecture.
The two source papers.
- Nick Arnosti. Greedy Matching in Bipartite Random Graphs. Stochastic Systems 12(2), 133–150, June 2022. First published online 2 November 2021.
Algorithms: p. 135, §1.1. Random graph: p. 136, Definition 2. Equal-capacity conjecture: p. 136, following Theorem 2.
- Arthur Cohen and Harold B. Sackrowitz. Unbiasedness of Tests for Homogeneity. The Annals of Statistics 15(2), 805–816, 1987.
Conditional association: Lemma 4.1, pp. 811–812. The integer-valued extension is stated on p. 809 and developed in §5. Lean proves the required specialization directly.