← back to the atlas

d4-journals-geb-2020-0100 (d4-journals-geb-2020-0100)

Answer: —

The anchor (named result in the paper)

Theorem 5.1 — class: other

PDF text-layer excerpt — equations and symbol order may be approximateConsider a matching market with institutions E = (I, H, τ, D, Q, A, δ, P, ≻, π). 1. The µNDAI is individually rational, non-wasteful, respects distributional constraints and there is no justified envy; namely, the assignment µNDAI is fair. 2.

statement extracted from the paper’s text layer; consult the paper for the exact wording

The continuous mirror question, as graded

Given a finite set of household types \(T\) with rational masses \(\mu_t\), each type’s institution and complete ranking of apartment classes \(A\), per-capita class supplies \(s_a\), institutional quotas \(q_i\), apartment priorities over institutions, and responsive institutional rankings over class-type pairs, compute a rational allocation \(x_{t,a,i}\). Require \(x_{t,a,i}=0\) for unacceptable pairs or institutions outside type \(t\)’s attachment; \(\sum_{a,i}x_{t,a,i}\leq\mu_t\), \(\sum_{t,i}x_{t,a,i}\leq s_a\), and \(\sum_{t,a}x_{t,a,i}=q_i\). Under feasible quota filling and an over-demand promise that, for every \(i,a\), more than \(q_i\) mass of types attached to \(i\) accepts \(a\) and is acceptable to \(i\), find an individually rational allocation with no positive-mass waste or justified-envy block that is Pareto-undominated among such allocations. Compare allocations by first-order dominance for each type’s distribution over its ranked classes, with unmatched agents ranked last.

Packaged proof task (what the prover saw — nothing else)

Let \(A\) be \(m\) apartment classes and \(I\) be \(n\) institutions. A society is given by its support: the list of \(\tau\) types with positive mass, each with its mass as a binary rational; \(\tau\) is the support size, not the number of possible types. Normalize \(\sum_t\mu_t=1\), and let \(L\) be the total input bit length.
Each type \(t\) has exactly one attachment \(i(t)\) and a strict ranking of \(A\cup\{\varnothing\}\); classes above \(\varnothing\) are acceptable. Each institution supplies a strict ranking of its class-type pairs and \(\varnothing\), interpreted responsively. Each class has a strict priority order over all institutions, all acceptable to it.
Supplies \(s_a\) and quotas \(q_i\) are positive binary rationals satisfying \(\sum_a s_a=\sum_i q_i\leq1\). Promise feasible individually rational quota filling and, for every \(i,a\), \(\sum_{t:i(t)=i,\ a\succ_t\varnothing,\ (a,t)\succ_i\varnothing}\mu_t>q_i\).
An allocation has rational \(x_{t,a,i}\geq0\), zero unless \(i=i(t)\) and the pair is acceptable to both sides, with \(\sum_{a,i}x_{t,a,i}\leq\mu_t\), \(\sum_{t,i}x_{t,a,i}\leq s_a\), and \(\sum_{t,a}x_{t,a,i}=q_i\). Put \(x_{t,\varnothing}=\mu_t-\sum_{a,i}x_{t,a,i}\).
Type \(t\) demands \(a\) if positive mass of it receives a strictly worse class or is unmatched. Institution \(i(t)\) is willing to admit \((a,t)\) if positive assigned mass at that institution has a strictly lower-ranked class-type pair; this is the responsive quota test for replacing an equal positive amount of incumbent contracts.
A waste block exists when a demanded, mutually acceptable class has unused supply and the attached institution is willing. An envy block exists when \(t\) demands \(a\), \(x_{u,a,j}>0\), and either \(j\neq i(t)\), the attached institution is willing and has higher priority at \(a\) than \(j\), or \(j=i(t)\) and \((a,t)\succ_j(a,u)\). These are local acceptance tests; the displaced institution need not retain its quota.
Call an allocation fair if it is individually rational and has neither block. Compare allocations by first-order dominance of each type's class distribution, with unmatched mass last; domination requires weak dominance for every type and strict dominance for at least one. Seek a fair allocation undominated among fair allocations.

Does every promised instance admit such a rational allocation, and is finding one solvable in polynomial time in \(m,\tau,n,L\), or is this search problem NP-hard?

For finite households and apartments under over-demand and single institutional attachment, NDAI produces a quota-filling fair assignment undominated among fair assignments and is strategy-proof for households. [Bloch, Cantala and Gibaja](https://www.sciencedirect.com/science/article/abs/pii/S0899825620300117).
No result settling the specified mass-based problem was located.

Modeling choices made when packaging the task

Prover output (gpt-6.1-sol / high, Bolzano prover prompt)

Partial results for the mass-based problem

The general existence and complexity questions remain unresolved here. The following results advance them:

$$ \left(\prod_{i=1}^{n}(\tau_i+1)^m\right)\operatorname{poly}(m,\tau,n,L) $$
time, where $\tau_i$ is the number of supported types attached to institution $i$. In particular, for fixed $m,n$, fair feasibility and the requested search can be solved in polynomial time.

$$ \mu_t>q_{i(t)}\qquad\text{for every supported type }t $$
admits a rational undominated fair allocation, computable in polynomial time. This includes the case of exactly one supported type per institution.

I also prove the conditional input-grid and undominance results needed for these conclusions.

1. Feasibility and the exact blocking tests

Suppress the redundant institution index, writing $x_{t,a}=x_{t,a,i(t)}$. Let
$$ E=\{(t,a):a\succ_t\varnothing,\ (a,t)\succ_{i(t)}\varnothing\} $$
be the set of mutually acceptable pairs, and write $z_t=x_{t,\varnothing}$.

Temporarily allow real coordinates. Let $P$ be the polytope specified by
$$ \begin{aligned} &x_{t,a}\geq0,\quad z_t\geq0,\\ &\sum_{a:(t,a)\in E}x_{t,a}+z_t=\mu_t &&\text{for every }t,\\ &\sum_{t:(t,a)\in E}x_{t,a}\leq s_a &&\text{for every }a,\\ &\sum_{t:i(t)=i}\sum_{a:(t,a)\in E}x_{t,a}=q_i &&\text{for every }i. \end{aligned} $$
Variables outside $E$ are identically zero.

Every point of $P$ fills every class. Indeed,
$$ \sum_a\sum_t x_{t,a}=\sum_iq_i=\sum_as_a. $$
The nonnegative unused supplies therefore sum to zero, so each unused supply is zero. Thus waste blocks are impossible throughout $P$.

For $(t,a)\in E$, define
$$ D_{t,a}(x)=z_t+ \sum_{\substack{b:(t,b)\in E\\a\succ_t b}}x_{t,b}. $$
The type demands $a$ exactly when $D_{t,a}(x)>0$.

For each institution $i$, assign distinct integer ranks $\rho_i(a,t)$ to its mutually acceptable pairs, with smaller rank meaning higher institutional preference. Define
$$ W_{t,a}(x)= \sum_{\substack{(v,b)\in E\\i(v)=i(t)\\ \rho_{i(t)}(b,v)>\rho_{i(t)}(a,t)}}x_{v,b}. $$
The institution is willing under the specified local test exactly when $W_{t,a}(x)>0$.

Consequently, fairness on $P$ is exactly the absence of these two kinds of envy:

$$ \rho_{i(t)}(a,t)<\rho_{i(t)}(a,u). $$

All candidate pairs in these conditions belong to $E$.

2. An exact description by rank cutoffs

Let
$$ E_{i,a}=\{t:i(t)=i,\ (t,a)\in E\}. $$

A cutoff profile chooses, for every institution–class pair,
$$ c_{i,a}\in\{0\}\cup\{\rho_i(a,t):t\in E_{i,a}\}. $$
The value zero represents an empty cell. A positive value permits only contracts at least as highly ranked as that value.

Put
$$ R_i(c)=\max_a c_{i,a}. $$

For a mutually acceptable candidate $(t,a)$, with $i=i(t)$, call the candidate restricted by $c$ if either

$$ \rho_i(a,t)<c_{i,a}, $$

or

$$ \rho_i(a,t)<R_i(c) $$

and there is an institution $j\neq i$ such that $c_{j,a}>0$ and $i$ has higher priority at $a$ than $j$.

Define $P_c$ by adding the following constraints to $P$:

$$ x_{t,a}=0 \quad\text{whenever }\rho_{i(t)}(a,t)>c_{i(t),a}, $$

and

$$ D_{t,a}(x)=0 \quad\text{for every candidate restricted by }c. $$

Because $D_{t,a}$ is a sum of nonnegative coordinates, its vanishing merely forces those coordinates to zero. Thus $P_c$ is a face of $P$, possibly empty.

Theorem 1: cutoff characterization

If $F$ denotes the set of fair real allocations, then
$$ F=\bigcup_c P_c. $$

Proof: every point of $P_c$ is fair

Take $x\in P_c$.

Suppose there were within-institution envy by $t$ of an incumbent $u$ at $a$. The positive incumbent coordinate satisfies
$$ \rho_i(a,u)\leq c_{i,a}. $$
Hence
$$ \rho_i(a,t)<\rho_i(a,u)\leq c_{i,a}. $$
The candidate is restricted, so $D_{t,a}(x)=0$, contradicting demand.

Now suppose there were cross-institution envy by a type attached to $i$, displacing positive mass attached to $j$ at $a$. Positivity of $W_{t,a}(x)$ gives some positive incumbent $x_{v,b}$ at $i$ with
$$ \rho_i(a,t)<\rho_i(b,v)\leq c_{i,b}\leq R_i(c). $$
The displaced positive coordinate implies $c_{j,a}>0$. The priority condition therefore makes $(t,a)$ restricted. Again $D_{t,a}(x)=0$, a contradiction.

There are no waste blocks by Section 1. Thus $x$ is fair.

Proof: every fair allocation belongs to some $P_c$

Take a fair allocation $x$. Set
$$ c_{i,a}= \begin{cases} 0,&\text{if }\sum_{t\in E_{i,a}}x_{t,a}=0,\\ \max\{\rho_i(a,t):x_{t,a}>0,\ t\in E_{i,a}\}, &\text{otherwise}. \end{cases} $$
Every positive coordinate satisfies its cutoff restriction.

Consider a candidate restricted by the first condition. A positive incumbent realizes the rank $c_{i,a}$ and is strictly below the candidate. Fairness therefore forces $D_{t,a}(x)=0$.

For a candidate restricted by the second condition, a positive incumbent at $i$ realizes $R_i(c)$ and is strictly below the candidate. Thus $W_{t,a}(x)>0$. The relevant institution $j$ has positive mass at $a$ and lower priority there. Fairness again forces $D_{t,a}(x)=0$.

Hence $x\in P_c$, proving the characterization. This proof uses exactly the task’s local tests; it does not assume that a blocking displacement preserves another institution’s quota.

3. Rational undominated allocations and the cutoff algorithm

3.1. Integral vertices after scaling

Let $D$ be the least common multiple of the denominators of all masses, supplies, and quotas. Its bit length is polynomial in $L$, because it divides the product of those denominators.

Represent $P$ by the directed network
$$ o\longrightarrow i\longrightarrow t\longrightarrow a\longrightarrow r. $$
Use the following arc bounds:

The source supplies, and the sink receives, $\sum_iq_i$.

The correspondence is
$$ x_{t,a}=\operatorname{flow}(t\to a), \qquad z_t=\mu_t-\operatorname{flow}(i(t)\to t). $$
Flow conservation determines every remaining arc flow uniquely. Thus this is an affine bijection between feasible flows and $P$.

The additional restrictions defining $P_c$ remain arc bounds:

After multiplication by $D$, all bounds and balances are integral. A directed node–arc incidence matrix is totally unimodular: in any square submatrix, a column with at most one nonzero permits determinant expansion; if every column has two nonzeros, their opposite signs make the row sum zero. Induction gives determinants in $\{0,1,-1\}$. Adding coordinate bounds preserves total unimodularity.

The integral-flow theorem therefore gives integral vertices after scaling. The affine bijection preserves vertices.

It follows that every vertex of every nonempty $P_c$ has coordinates in
$$ D^{-1}\mathbb Z. $$

In particular, existence of a real fair allocation is equivalent to existence of a fair allocation on this input grid.

3.2. A dominance-increasing linear objective

For each type, list its mutually acceptable classes in its preference order:
$$ b_{t,1}\succ_t\cdots\succ_t b_{t,r_t}. $$
Define
$$ C_{t,k}(x)=\sum_{\ell=1}^{k}x_{t,b_{t,\ell}}, \qquad \Phi(x)=\sum_t\sum_{k=1}^{r_t}C_{t,k}(x). $$

Classes omitted from this list always receive zero mass. Since each type’s total mass is fixed and all assigned classes are above unmatched status, these cumulative quantities detect first-order dominance exactly.

If $y$ dominates $x$, every $C_{t,k}$ weakly increases, and at least one strictly increases. Therefore
$$ y\text{ dominates }x\quad\Longrightarrow\quad\Phi(y)>\Phi(x). $$

By Theorem 1, $F$ is a finite union of compact polytopes. If nonempty, it has a maximizer of $\Phi$, and every such maximizer is undominated among fair allocations.

Moreover, optimize $\Phi$ over each nonempty $P_c$ and choose an optimal vertex. Selecting the largest of these face optima gives an undominated fair allocation on the input grid.

Thus:

Conditional existence conclusion. If a fair real allocation exists, an undominated rational fair allocation exists with every coordinate in $D^{-1}\mathbb Z$.

There are at most $\tau(m+1)$ coordinates, all between zero and one. The resulting allocation has polynomial encoding length.

3.3. Running time

The number of cutoff profiles is
$$ N=\prod_{i,a}(|E_{i,a}|+1) \leq\prod_i(\tau_i+1)^m \leq(\tau+1)^{mn}. $$

For each profile:

Indeed,
$$ \Phi(x)= \sum_t\sum_{\ell=1}^{r_t}(r_t-\ell+1)x_{t,b_{t,\ell}}, $$
so assignment arcs receive the negatives of these coefficients as costs. Integer minimum-cost flow after scaling returns an integral optimum.

Each network has polynomial size and polynomial binary encoding length. Standard minimum-cost flow algorithms therefore give total running time
$$ N\operatorname{poly}(m,\tau,n,L). $$
No expansion into $D$ unit households is used.

The algorithm returns an undominated rational fair allocation whenever one exists, and otherwise reports nonexistence. For fixed $m,n$, its running time is polynomial in $\tau,L$. This computational result does not establish that the promises always make some $P_c$ nonempty.

4. A polynomial case with arbitrary numbers of institutions and classes

Additional hypothesis

Assume
$$ \mu_t>q_{i(t)}\qquad\text{for every supported type }t. $$

This hypothesis is stronger than the general promises.

Theorem 2

Under this additional hypothesis, every promised instance admits a rational fair allocation undominated among fair allocations, and one can find such an allocation in polynomial time in $m,\tau,n,L$.

4.1. Every type demands every mutually acceptable class

At a quota-filling allocation, a type attached to $i$ receives at most $q_i$ in total. Hence
$$ z_t\geq\mu_t-q_i>0. $$
Therefore
$$ D_{t,a}(x)>0\qquad\text{for every }(t,a)\in E. $$

For each institution–class pair, the overdemand promise implies $E_{i,a}\neq\varnothing$. Let $v_{i,a}$ be the unique type in $E_{i,a}$ maximizing institution $i$’s preference for $(a,t)$.

In any fair allocation, positive mass in cell $(i,a)$ must belong to $v_{i,a}$. Otherwise $v_{i,a}$ demands $a$ and has within-institution envy of the lower-ranked positive incumbent.

Thus every fair allocation is described by
$$ y_{i,a}=x_{v_{i,a},a}, $$
with all other assignment coordinates zero.

Conversely, type capacities impose no additional restriction on such a quota-filling matrix:
$$ \sum_{a:v_{i,a}=t}y_{i,a} \leq\sum_a y_{i,a} =q_i<\mu_t. $$

4.2. Reduction to bipartite stable allocation

Construct a complete bipartite graph between institutions and classes.

In this graph, an edge blocks when it is unsaturated and each endpoint can increase its flow using unused capacity or replacing positive flow on a less-preferred edge.

Every stable allocation fills both sides

Let $Q=\sum_iq_i=\sum_as_a$. If total flow were less than $Q$, some institution $i$ and some class $a$ would both have unused capacity.

Their edge exists, and
$$ y_{i,a}<q_i,\qquad y_{i,a}<s_a. $$
Thus it is unsaturated, and both endpoints can use unused capacity. It would block.

Therefore every stable allocation fills every institution and class.

Stability implies fairness

Lift a stable matrix $y$ by assigning each cell to $v_{i,a}$. The preceding capacity calculation makes this an individually rational, quota-filling allocation. There is no within-institution envy, because each occupied cell uses its top-ranked acceptable type.

Suppose a cross-institution envy block existed through candidate $(a,t)$ attached to $i$, displacing positive mass at a lower-priority institution $j$.

Since
$$ \rho_i(a,v_{i,a})\leq\rho_i(a,t), $$
willingness for $(a,t)$ implies willingness for $(a,v_{i,a})$. Hence institution $i$ has positive flow on a class it ranks below $a$. Class $a$ has positive flow at the lower-priority institution $j$.

These facts also imply
$$ y_{i,a}<q_i,\qquad y_{i,a}<s_a. $$
So $(i,a)$ is an unsaturated blocking edge, contradicting stability.

Fairness implies stability

A fair allocation must use the top type in each cell, as already proved. Its matrix fills both sides.

A stable-allocation block would therefore consist of an institution $i$ holding positive flow on a class below $a$, while $a$ holds positive flow at a lower-priority institution. The type $v_{i,a}$ demands $a$, and its institution is willing. This is precisely a cross-institution envy block.

Consequently, the reduction gives a bijection between fair allocations and stable allocations.

4.3. Computing an undominated allocation

The external theorem used here is that a finite bipartite stable-allocation instance with strict preferences, rational vertex and edge capacities, and rational edge costs admits polynomial-time minimum-cost optimization. Unused capacity is represented by last-ranked dummy vertices in the equality formulation. See [Dean–Munshi, Sections 2–4](https://people.computing.clemson.edu/~bcdean/stable_alloc.pdf).

For binary bit complexity, scale capacities by a common denominator. Their algorithm uses polynomially many augmentations and rotations, followed by minimum-weight closure. Augmentation amounts remain integral and bounded by total scaled capacity. Rotation costs consequently have polynomial encoding length, and closure is computable by polynomial-time maximum flow.

Give edge $(i,a)$ cost
$$ -\bigl(r_{v_{i,a}}-\ell_{v_{i,a}}(a)+1\bigr), $$
where $\ell_t(a)$ is the position of $a$ in type $t$’s mutually acceptable class list. The resulting cost is exactly $-\Phi$ for the lifted allocation.

All graph preferences are strict; capacities are binary rationals; costs are integers of magnitude at most $m$; and there are $mn$ edges. Thus the theorem applies and returns a rational fair allocation maximizing $\Phi$. By Section 3.2, it is undominated among fair allocations.

Finally, if there is exactly one supported type attached to each institution, the overdemand promise forces that type to accept every class mutually and to have mass greater than its institution’s quota. Thus this case satisfies the additional hypothesis.

5. A promised instance whose fair set is not convex

Let the classes be $a,b,c$, and let the institutions be $1,2$. Types $p,r,d$ attach to institution $1$, while $h,k$ attach to institution $2$.

Set
$$ \mu_p=\mu_r=\mu_h=\mu_k=\frac18, \qquad \mu_d=\frac12. $$
These masses sum to one. Set
$$ s_a=s_b=s_c=\frac18, \qquad q_1=\frac14,\quad q_2=\frac18. $$

Every class is acceptable to every type, and every class–type pair is acceptable to its attached institution. Type preferences are:

| Type | Class ranking |
|---|---|
| $p$ | $c\succ a\succ b\succ\varnothing$ |
| $r$ | $a\succ b\succ c\succ\varnothing$ |
| $d$ | $a\succ b\succ c\succ\varnothing$ |
| $h$ | $c\succ a\succ b\succ\varnothing$ |
| $k$ | $b\succ a\succ c\succ\varnothing$ |

Institutional rankings, with $\varnothing$ below every listed pair, are
$$ \begin{aligned} 1:\;&(b,r)\succ(a,p)\succ(b,p)\succ(c,p)\succ(c,r)\\ &\succ(a,r)\succ(a,d)\succ(b,d)\succ(c,d),\\ 2:\;&(c,k)\succ(c,h)\succ(b,h)\succ(a,h)\succ(a,k)\succ(b,k). \end{aligned} $$
Class priorities are
$$ a:\ 2\succ1,\qquad b:\ 1\succ2,\qquad c:\ 1\succ2. $$

The overdemand masses at every class are $3/4$ for institution $1$ and $1/4$ for institution $2$, strictly exceeding their quotas.

Consider these allocations, with every displayed assignment having mass $1/8$ and all others zero:

| Allocation | At $a$ | At $b$ | At $c$ |
|---|---|---|---|
| $X$ | $r$ through $1$ | $h$ through $2$ | $p$ through $1$ |
| $Y$ | $p$ through $1$ | $r$ through $1$ | $k$ through $2$ |

Both fill all supplies and quotas.

5.1. Allocation $X$ is fair

Types $p,r$ receive their first choices.

For within-institution envy, the only other possible competitors are:

Thus there is no within-institution envy.

For cross-institution envy:

Hence $X$ is fair.

5.2. Allocation $Y$ is fair

Within institution $1$, the demanding competitors at $a$ are $r,d$, both ranked below incumbent $p$. At $b$, $d$ is ranked below incumbent $r$; $p$ does not demand $b$.

Within institution $2$, unmatched $h$ is ranked below incumbent $k$ at $c$.

For cross-institution envy:

Thus $Y$ is fair.

5.3. Their midpoint is unfair

Let
$$ Z=\frac12X+\frac12Y. $$
At $Z$, type $p$ receives mass $1/16$ at $a$, which it ranks below $c$. Therefore
$$ D_{p,c}(Z)=\frac1{16}>0. $$

Institution $1$ holds mass $1/16$ of $(a,r)$, which it ranks below $(c,p)$. Hence
$$ W_{p,c}(Z)>0. $$

Class $c$ holds mass $1/16$ of type $k$ through institution $2$, and institution $1$ has higher priority there. These three positive masses establish a cross-institution envy block.

Therefore $X,Y\in F$ but $Z\notin F$: the fair set is nonconvex even on promised instances with dyadic data.

6. Remaining open questions

The cutoff characterization and the special-case reduction do not establish general fair feasibility. No counterexample to general existence is proved here.

They also do not settle polynomial-time solvability or NP-hardness when the numbers of classes and institutions vary and individual type capacities can bind. The nonconvexity example identifies an obstruction to directly optimizing over one convex feasible region, but supplies neither a hardness reduction nor an impossibility result.

⟨structured verdict parsed — rendered above⟩

Adversarial review (gpt-6.1-sol / medium, Bolzano verifier prompt)

Verification report

Overall assessment: partial, with substantial valid progress. The output does not settle general existence or general polynomial-time solvability versus $\mathrm{NP}$-hardness. It explicitly acknowledges both omissions. Its cutoff characterization, conditional rationality and undominance results, special-case algorithm, and nonconvexity example are sound in substance. I found one minor convention that should be made explicit, and no false central step.

1. Feasibility and blocking tests

Verified.

Suppressing the institution index is legitimate because each type has exactly one attachment. The polytope $P$ correctly encodes mutual acceptability, type capacities, class supplies, unmatched mass, and institution quota equalities.

The conclusion that every class fills follows from
$$ \sum_{t,a}x_{t,a}=\sum_iq_i=\sum_as_a $$
together with the individual class upper bounds. Therefore waste blocks are impossible throughout $P$. This uses the task’s equality of total supply and total quota; it does not require an additional existence assumption.

The quantities $D_{t,a}$ and $W_{t,a}$ correctly encode the specified demand and willingness tests. Their sums have nonnegative terms, so positivity is equivalent to the existence of positive mass satisfying the relevant comparison.

The two envy conditions reproduce the task correctly. In particular, the within-institution condition does not improperly add an institutional willingness requirement.

2. Cutoff characterization

Verified, subject to an explicit positive-rank convention.

Minor issue: ranks must be positive

Section 1 assigns “distinct integer ranks,” without expressly requiring positivity. Section 2 reserves $0$ for an empty cell and uses $c_{j,a}>0$ to indicate a potentially occupied cell. These arguments require
$$ \rho_i(a,t)\in\mathbb Z_{>0}. $$

The intended convention is apparent from the discussion of positive cutoffs. This is an expositional issue, rather than a substantive obstruction.

Minimum clarification: Specify that institutional ranks are distinct positive integers.

Forward inclusion

The proof that $P_c\subseteq F$ correctly checks both envy cases.

For within-institution envy, a positive incumbent obeys its assignment cutoff, giving
$$ \rho_i(a,t)<\rho_i(a,u)\leq c_{i,a}. $$
Thus the candidate is restricted and cannot have positive demand.

For cross-institution envy, positive willingness supplies a positive incumbent whose rank exceeds the candidate’s rank. The cutoff bounds that incumbent’s rank by $R_i(c)$. A positive displaced coordinate supplies the required positive cutoff at the lower-priority institution. The candidate is again restricted.

The proof does not assume that arbitrary cutoffs are attained by positive coordinates; that assumption would be unjustified in this direction, and the output correctly avoids it.

Reverse inclusion

For a fair allocation, the constructed positive cutoffs are attained by incumbents. Consequently:

Fairness therefore forces all the required demand quantities to vanish.

Empty cells cause no problem under the positive-rank convention. The characterization
$$ F=\bigcup_cP_c $$
is established.

Face assertion

Each equation $D_{t,a}=0$ forces its constituent nonnegative coordinates to vanish. The added restrictions therefore set nonnegative coordinates to zero, so each nonempty $P_c$ is indeed a face of $P$.

3. Input-grid rationality and undominance

Verified.

Network representation and integrality

The network correctly represents $P$:

Flow conservation uniquely determines the other flows from the assignment coordinates, and unmatched mass is recovered by the stated affine formula. Thus the claimed affine bijection is valid.

The restrictions defining $P_c$ become assignment-arc zero bounds and, when unmatched mass is excluded, fixed institution-to-type flows. After scaling by $D$, all bounds and balances are integral.

The total-unimodularity argument is valid. In a square incidence submatrix whose columns all retain two entries, those entries have opposite signs, making the rows linearly dependent. Otherwise determinant expansion and induction apply. Coordinate bounds preserve total unimodularity.

The integral-vertex conclusion applies to these bounded network-flow polytopes. The affine correspondence preserves vertices and recovers unmatched coordinates on the same grid. Hence every nonempty $P_c$ has a vertex in
$$ D^{-1}\mathbb Z. $$

This establishes existence of a grid-valued fair allocation whenever a real fair allocation exists. It does not assert that every fair allocation lies on that grid.

Dominance objective

The cumulative quantities $C_{t,k}$ correctly detect dominance on the feasible allocations. Omitted classes receive zero mass, and total type mass is fixed. Thus deleting those zero coordinates does not lose a possible strict dominance comparison.

Every domination strictly increases $\Phi$. Consequently, a global maximizer of $\Phi$ over $F$ is undominated.

The converse is neither proved nor needed: an undominated allocation need not maximize this particular objective.

Since $F$ is a finite union of compact polytopes, a maximizer exists whenever $F$ is nonempty. Optimizing over the individual faces and selecting a best integral vertex establishes the conditional rational undominance claim.

Encoding length

The denominator bound is valid because $D$ divides the product of the input denominators. Coordinates bounded by $1$ on this grid have polynomial bit length, and there are at most $\tau(m+1)$ coordinates. The output-size claim follows.

4. Cutoff enumeration algorithm

Verified as an algorithm that either finds an undominated fair allocation or reports fair infeasibility.

The profile count satisfies
$$ N=\prod_{i,a}(|E_{i,a}|+1) \leq\prod_i(\tau_i+1)^m \leq(\tau+1)^{mn}. $$

Each profile can be processed using a polynomial-size network. The expansion
$$ \Phi(x)=\sum_t\sum_{\ell=1}^{r_t}(r_t-\ell+1)x_{t,b_{t,\ell}} $$
is correct, so the stated assignment-arc costs implement maximization of $\Phi$.

Scaling does not require expanding the society into unit households. Polynomial-time minimum-cost flow with binary-encoded integral capacities gives the claimed bound.

For fixed $m,n$, the enumeration bound is polynomial in $\tau,L$. However, this computational statement remains compatible with reporting nonexistence: it does not prove that every promised instance admits a fair allocation.

5. Additional-hypothesis polynomial case

Verified.

Universal demand and cell representatives

Under
$$ \mu_t>q_{i(t)}, $$
the bound
$$ z_t\geq\mu_t-q_{i(t)}>0 $$
holds because all mass assigned to that type contributes to its institution’s quota. Every mutually acceptable class is therefore demanded.

The overdemand promise makes every $E_{i,a}$ nonempty. Strict institutional preferences give a unique top type $v_{i,a}$.

If a cell assigned positive mass to any other type, $v_{i,a}$ would have within-institution envy. Thus the restriction to cell representatives is necessary for fairness.

The capacity calculation correctly shows that quota-filling matrices lifted through these representatives satisfy every type capacity, even when a type represents multiple cells.

Stable-allocation correspondence

The complete bipartite graph and edge capacities are correctly specified.

If total flow were below the common total capacity, some institution and some class would both have residual capacity. Their common edge would have flow strictly below both endpoint capacities, hence below its edge capacity, and would block. Thus stable allocations fill both sides.

For stability implying fairness, the representative pair is at least as institutionally preferred as the proposed pair. Therefore willingness for the proposed pair implies willingness for the representative pair. The positive inferior institutional flow and positive lower-priority class flow also establish edge unsaturation. The alleged envy block consequently gives a stable-allocation block.

For fairness implying stability, both sides already fill. A blocking edge therefore requires inferior positive flow at both endpoints. Universal demand of the representative type turns this directly into cross-institution envy.

The claimed bijection is established.

Cited optimization theorem

The cited source supports the required theorem. Its model has strict preferences, vertex capacities, edge capacities, and dummy elements for unused capacity; it establishes stable existence and polynomial-time optimization of linear edge costs through rotations and minimum-cost closure. The reduction satisfies these hypotheses. [Dean–Munshi, Sections 2–4](https://people.computing.clemson.edu/~bcdean/stable_alloc.pdf)

The output’s scaling argument adequately addresses binary rational data: integral augmentation amounts remain bounded by scaled total capacity, and the polynomial number of rotations produces polynomial-length closure weights. The specified edge costs equal $-\Phi$ for lifted allocations.

Theorem 2 therefore stands. The one-supported-type-per-institution corollary also follows from the overdemand promise.

6. Nonconvexity example

Verified by recomputing all candidate envy tests.

The masses sum to $1$, and total supply and total quota both equal $3/8$. Both displayed allocations respect type capacities and fill supplies and quotas, establishing the feasibility promise.

Every pair is mutually acceptable. The attached masses are $3/4$ and $1/4$, strictly exceeding the respective quotas at every class.

For $X$, the within-institution comparisons exclude all demanding challengers. Across institutions, the only higher-priority demanding candidates at occupied lower-priority cells fail the willingness test.

For $Y$, the listed within-institution comparisons are correct. Institution $2$ cannot replace its highest-ranked incumbent at $a$; the demanding institutional candidates at $c$ rank below both institution-$1$ incumbents.

The complete check gives no envy block for either allocation.

At the midpoint,
$$ D_{p,c}(Z)=\frac1{16}, \qquad W_{p,c}(Z)=\frac1{16}, \qquad x_{k,c,2}(Z)=\frac1{16}. $$
Institution $1$ has higher priority than institution $2$ at $c$. Hence the stated midpoint block exists, establishing nonconvexity.

This example establishes neither hardness nor failure of general existence, as the output correctly acknowledges.

7. Outstanding task requirements and feedback

Two major omissions relative to the assigned target remain. They are acknowledged limitations, rather than hidden errors in the partial results.

Required completion: Establish existence for every originally promised instance, or provide a promised counterexample.

Required completion: Establish a polynomial-time algorithm under the original promises or a hardness result for the specified search problem, including its undominance requirement.

These are substantive missing results, not matters that additional wording alone can resolve. The existing direction is promising because its structural and restricted-case conclusions survive verification.

⟨structured verdict parsed — rendered above⟩

Tier: machine-proved, adversarially reviewed by an independent model. No human has checked this proof. Generated from pipeline artifacts by tools/atlas_build.py.