← back to the atlas

d4-conf-ijcai-2021-0340 (d4-conf-ijcai-2021-0340)

Answer: —

The anchor (named result in the paper)

Theorem 1 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateThe GDA-FD algorithm runs in polynomial- time and returns a feasible outcome that is non-wasteful, even if each student has multiple types. Next, we propose a stability concept for the setting of School Choice with Flexible Diversity Goals and Specialized Seats by taking the dynamic precedence of schools into ac- count. The following Definition 1 captures a natural idea called dynamic priority proposed in a influential work on school choice with diversity goals [Ehlers et al., 2014]. While our new definition is applicable to any market with flexible di- versity goals.

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

The continuous mirror question, as graded

Given a rational distribution \(\mu\) over \(\tau\) complete applicant types, rational per-capita supplies of school-seat classes, type preferences over contracts, school priority classes, and rational diversity-level intervals expressed as population proportions, compute the terminal assignment of a mass version of GDA-FD. In each round, proposed type-mass follows its next preferred contract; schools select mass by current dynamic precedence and static priority, advancing to the next rational threshold, exhaustion, or capacity event before updating precedence. A type’s mass may split across contracts, while each individual receives one whole contract. Is this terminal feasible, non-wasteful assignment computable in time polynomial in the number of schools and seat classes, \(\tau\), the number of categories and interval endpoints, and input bit length?

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

A society is given by its support: \(\tau\) complete applicant types with positive binary-rational masses \(\mu_a\), summing to \(1\); \(\tau\) is the support size, not the number of possible types. There are \(m\) schools, \(s\) seat classes, and \(k\) diversity categories. Each seat class \(h\) belongs to one school and has nonnegative binary-rational supply \(q_h\); school capacity is the sum of its seat supplies.
Each applicant type specifies a nonempty category set \(T(a)\), mutually acceptable contracts \((h,b)\), preferences over these contracts, and its static priority class at every school. Refine preference ties by supplied fixed orders; refine school priority ties by support index, independently of the contract. Unmatched is below every acceptable contract.
For every school and category, explicitly listed rational intervals partition \([0,1]\), with a positive integer precedence label on each interval; smaller labels have higher precedence. Intervals are left-closed and right-open, except the last includes \(1\). These are soft diversity goals, measured against total population mass, not school enrollment; let \(e\) count listed endpoints.
Represent type \(a\) by a nonatomic interval \([0,\mu_a)\); within a type, every school breaks ties by increasing interval coordinate. Rejections attach permanently to the particular individuals and contracts concerned. Each individual receives at most one whole contract; an aggregate type may split across contracts.
Mass GDA-FD starts with no rejections. Each round, every individual proposes its favorite acceptable contract not previously rejected, or remains unmatched if none remains. Every school recomputes its selection from zero using only that round's proposals, including proposals from previously retained individuals.
In a school's selection, category counts are selected masses, and selecting type \(a\) increases the counts of every category in \(T(a)\). Among categories represented by remaining proposals to seat classes with residual supply, find those with highest current precedence; among proposals whose type contains one of these categories, choose by static school priority and the fixed tie orders.
Select that proposal's mass in coordinate order until its available fragment is exhausted, a seat or school capacity is reached, or any affected category reaches its next interval endpoint. Update all affected precedence labels at the event and repeat until no selectable proposal remains. Reject every unselected proposed individual-contract pair permanently; stop when a round rejects zero mass.
The output is the exact terminal mass \(x_{a,h}\) on each contract. Feasibility means \(x_{a,h}\geq 0\), \(\sum_h x_{a,h}\leq\mu_a\), and \(\sum_a x_{a,h}\leq q_h\), using acceptable contracts only. Non-wastefulness means no positive mass already assigned to a contract can move to a strictly preferred acceptable contract while preserving feasibility.

Is exact computation of the terminal assignment of this mass GDA-FD in \(\mathrm{P}\), with running time polynomial in \(m,s,\tau,k,e,L\), where \(L\) is total input bit length, or is it \(\mathrm{NP}\)-hard?

For finite applicants and individual seats, GDA-FD runs in polynomial time and returns a feasible, non-wasteful assignment even with overlapping categories ([Aziz and Sun](https://www.ijcai.org/proceedings/2021/0003.pdf)). No result settling this exact mass algorithm was identified in the literature search.

Modeling choices made when packaging the task

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

Partial progress on exact mass GDA-FD

1. Status and new results

The full complexity classification remains unresolved. I prove two polynomial-time subcases:

I also re-establish the polynomial-space upper bound for the unrestricted problem and give a counterexample showing why the fixed-priority reduction does not extend directly to overlapping, count-dependent categories.

A contract is identified with its seat class $h$, since its owning school is uniquely determined by $h$.

2. Compact states and exact simulation

2.1. Proposal intervals remain ordered

For type $a$, write its refined acceptable-contract list as
$$ h_{a,1}\succ_a h_{a,2}\succ_a\cdots\succ_a h_{a,d_a}, $$
where $d_a\leq s$. Rank $d_a+1$ means that all acceptable contracts have been rejected. Set
$$ M=\sum_a d_a\leq \tau s. $$

Lemma 1. At the beginning of every round, an individual’s current rank is nondecreasing in its coordinate within its type. In particular, each type-contract proposal set is an interval.

Proof. Initially all individuals of a type with acceptable contracts have rank $1$.

Suppose the assertion holds in a particular round. Represent type $a$’s rank-$j$ proposal interval by
$$ [u_{a,j-1},u_{a,j}), \qquad 0=u_{a,0}\leq u_{a,1}\leq\cdots\leq u_{a,d_a}\leq\mu_a. $$
Its exhausted individuals occupy $[u_{a,d_a},\mu_a)$.

Within a type-contract proposal interval, selection always takes the earliest remaining coordinates. Its selected individuals therefore form a prefix
$$ [u_{a,j-1},v_{a,j}), \qquad u_{a,j-1}\leq v_{a,j}\leq u_{a,j}. $$
Pausing and later resuming selection does not change this prefix property.

Rejection advances an individual by exactly one rank. Thus the rejected suffix of old rank $j-1$ and the retained prefix of old rank $j$ combine into
$$ [v_{a,j-1},u_{a,j-1}) \;\cup\; [u_{a,j-1},v_{a,j}) = [v_{a,j-1},v_{a,j}), $$
where $v_{a,0}=0$. These new boundaries are ordered because
$$ v_{a,j-1}\leq u_{a,j-1}\leq v_{a,j}. $$
The rejected suffix of the last acceptable rank joins the exhausted suffix. This proves the induction. $\square$

Consequently, the current rejection history is represented by $M$ boundaries, with update
$$ u_{a,j}^{\mathrm{next}}=v_{a,j}. $$
Every boundary is nonincreasing across rounds.

Types with no acceptable contracts remain unmatched and require no boundaries.

2.2. Arithmetic and termination

Let $D$ be the product of the denominators of all input masses, supplies, and category endpoints. Then
$$ \log_2 D=O(L). $$

Lemma 2. Every boundary and every selected mass produced by the algorithm is an integer multiple of $1/D$.

Proof. Initial boundaries, supplies, and endpoints lie on this lattice. At a selection event, the stopping distances are fragment lengths, residual capacities, and differences between category endpoints and current counts. All are differences of lattice quantities. Their minimum is also a lattice quantity. Addition and subtraction preserve the lattice throughout selection and boundary updates. $\square$

Define
$$ \Psi=\sum_a\sum_{j=1}^{d_a}u_{a,j}. $$
Initially $u_{a,j}=\mu_a$ for every acceptable rank, so
$$ \Psi_{\mathrm{initial}}=\sum_a\mu_a d_a\leq s. $$
In one round, the rejected mass from rank $j$ of type $a$ is precisely
$$ u_{a,j}-v_{a,j}. $$
Therefore $\Psi$ decreases by exactly the total rejected mass. Every nonterminal round decreases it by at least $1/D$, while $\Psi\geq0$. Hence there are at most
$$ D\sum_a\mu_a d_a $$
nonterminal rounds.

This proves finite termination. It also proves that every terminal mass has polynomial bit length: its denominator divides $D$, and it lies in $[0,1]$.

2.3. One round takes polynomial time

During selection, every positive event exhausts a proposal fragment, fills a seat class, reaches school capacity, or reaches a listed category endpoint.

A fragment can be exhausted only once during that selection; a seat class can fill only once; and category counts only increase. Thus the number of positive events in a round is at most
$$ M+s+m+e. $$
At an endpoint, the label for the interval containing the new count is used, and the next stopping endpoint is strictly larger.

Each event can be implemented by scanning the explicit proposals, category sets, priorities, and interval lists. All arithmetic quantities have polynomial bit length by Lemma 2: coordinates and category counts are bounded by $1$, while residual supplies and capacities are bounded by sums of input supplies.

It follows that one round is polynomial-time computable in $m,s,\tau,k,e,L$. Storing only the current boundaries and selection workspace gives a polynomial-space exact algorithm for the unrestricted problem. In particular, the terminal-entry threshold decision problem belongs to $\mathrm{PSPACE}$.

The denominator-dependent round bound does not establish polynomial time.

2.4. Seat occupancy depends only on proposed mass

The following fact will also be used below.

Lemma 3. If the proposed mass at seat class $h$ in a round is $P_h$, its selected mass is
$$ S_h=\min\{P_h,q_h\}. $$

Proof. Selection cannot exceed either quantity. Suppose selection ends with $S_h<P_h$ and $S_h<q_h$. Then positive proposed mass remains at $h$, and $h$ has positive residual supply.

The school cannot have reached its capacity: that capacity is the sum of its seat supplies, and at least one seat still has positive residual supply. A remaining proposal has a nonempty category set, so some represented category has highest current precedence and provides a selectable proposal. This contradicts termination of selection. $\square$

Thus the rejected mass at $h$ is
$$ R_h=\max\{P_h-q_h,0\}. $$
Diversity goals determine which individuals are rejected, but not the total rejected mass at that seat class.

3. Polynomial-time computation for fixed-priority choices

3.1. Two sufficient conditions

Call a school choice fixed-priority if, for every proposal collection, its selection at each seat class consists of the first $\min\{P_h,q_h\}$ mass in a fixed order on applicants. Within each type, this order uses increasing coordinate.

Lemma 4. School choices are fixed-priority under either of these conditions:

Proof.

For the first condition, let $\ell_{b,t}$ be school $b$’s constant label for category $t$, and define
$$ \alpha_b(a)=\min_{t\in T(a)}\ell_{b,t}. $$
Among eligible proposals, the highest represented precedence is the smallest represented value of $\alpha_b(a)$. The algorithm therefore orders applicants by:

This order is independent of selected counts and of the proposed contract. Selection visits eligible proposals in this order. A seat class with residual supply cannot be prevented from selecting its next proposal by school capacity, because school capacity equals the sum of seat supplies. Hence each seat class selects its own highest-priority proposal mass.

For the second condition, every eligible proposal contains the same represented categories. Whichever category has highest current precedence, every eligible proposal satisfies it. Selection therefore uses only refined static school priority and coordinate order. The same seat-by-seat conclusion follows. $\square$

In particular, when $k=1$, nonempty category sets force every type to have the same category set. Thus arbitrary precedence intervals are allowed in this subcase.

3.2. The associated stable-allocation problem

Assume school choices are fixed-priority. Let $\succ_h$ denote seat class $h$’s resulting strict order on types; coordinate order refines priorities within a type.

Construct a bipartite allocation problem:

For a feasible allocation $y$, define
$$ A_a(h)= \mu_a-\sum_{g:\,g\succeq_a h}y_{a,g}, $$
and
$$ B_h(a)= q_h-\sum_b y_{b,h} + \sum_{b:\,a\succ_h b}y_{b,h}. $$
Here $A_a(h)$ is the mass of type $a$ that is unmatched or assigned below $h$. The quantity $B_h(a)$ measures vacancy at $h$ plus mass assigned to strictly lower-priority types.

An acceptable pair $(a,h)$ blocks $y$ exactly when
$$ A_a(h)>0 \quad\text{and}\quad B_h(a)>0. $$
An allocation with no blocking pair is called stable.

We use the following established result.

Stable-allocation theorem. A bipartite allocation problem with strict vertex preferences and rational vertex quotas and edge capacities has a unique job-optimal stable allocation. For every job, its allocation vector, listed in preference order, is lexicographically maximal among stable allocations. This allocation can be computed by a strongly polynomial algorithm. See [Dean and Munshi, Sections 2–3](https://people.computing.clemson.edu/~bcdean/stable_alloc.pdf).

The hypotheses hold here. There are at most $\tau+s$ vertices and $M$ edges, and all preferences are strict. Set the redundant edge capacity to
$$ u_{a,h}=\min\{\mu_a,q_h\}. $$
Our blocking definition agrees with the edge-capacitated definition: if both $A_a(h)$ and $B_h(a)$ are positive, then
$$ y_{a,h}<\mu_a \quad\text{and}\quad y_{a,h}<q_h, $$
so the edge is not saturated.

For completeness, inequalities and unmatched mass can be converted to the balanced formulation used in the theorem. Put
$$ Q_{\mathrm{seat}}=\sum_h q_h. $$
Add a dummy type of quota $Q_{\mathrm{seat}}$ and a dummy seat of quota $1$. Connect each real type to the dummy seat, each real seat to the dummy type, and the two dummies to each other. Dummies are ranked last by real vertices.

Any feasible real allocation $y$ has the balanced extension
$$ y_{a,0}=\mu_a-\sum_h y_{a,h}, \qquad y_{0,h}=q_h-\sum_a y_{a,h}, \qquad y_{0,0}=\sum_{a,h}y_{a,h}. $$
These values satisfy all row and column quotas. Edge capacities $\mu_a$, $q_h$, and $\min\{1,Q_{\mathrm{seat}}\}$ suffice for the three respective kinds of dummy edges.

No dummy edge can block: at least one endpoint ranks that edge last. Blocking on real edges is precisely the condition above. Thus the theorem applies to our formulation, with only polynomially many added vertices and edges.

Let $y^*$ denote its job-optimal real allocation.

3.3. Why the computed allocation equals the specified mass algorithm

Computing some stable allocation would not suffice: the task asks for the output of a particular algorithm with individual rejection histories. We now prove equality.

Let $z$ be the terminal assignment of mass GDA-FD. By Section 2, $z$ is rational. The stable-allocation algorithm also returns rational $y^*$. Choose an integer $Q$ divisible by $D$ and by every denominator appearing in $y^*$.

Conceptually partition each type interval into cells
$$ \left[\frac{i}{Q},\frac{i+1}{Q}\right), \qquad 0\leq i<Q\mu_a. $$
Treat each cell as one finite applicant, and give seat class $h$ integer capacity $Qq_h$.

Every proposal boundary of the mass algorithm lies on this grid. Under fixed-priority choices, selecting mass at $h$ means selecting the highest-priority $Q\min\{P_h,q_h\}$ cells. Consequently, round by round, the mass algorithm is exactly finite applicant-proposing deferred acceptance on these cells and integer seat capacities.

This expansion is used only for the proof.

Lemma 5. Finite applicant-proposing deferred acceptance with strict applicant preferences and fixed strict seat priorities returns a stable assignment that every applicant weakly prefers to every stable assignment.

Proof. First, a seat’s retained set cannot worsen in priority: its next proposal collection includes all previously retained applicants, and it again keeps its highest-priority applicants up to capacity.

Therefore an applicant rejected from a seat cannot block with that seat at termination. Any applicant who prefers a seat to its terminal assignment must previously have proposed there and been rejected. This proves stability.

Now suppose some applicant-seat pair belonging to a stable assignment is rejected. Choose the earliest round in which this happens, and let $(i,h)$ be such a pair in stable assignment $N$.

At that round, $h$ retains its full capacity of applicants, all ranked above $i$. Since $N$ assigns $i$ to $h$, at least one retained applicant $j$ is not assigned to $h$ in $N$.

Applicant $j$ proposes to $h$. If $N(j)$ were preferred to $h$, then $j$ must have been rejected from $N(j)$ in an earlier round. That contradicts the choice of the earliest round. Hence $j$ strictly prefers $h$ to $N(j)$, and $h$ prefers $j$ to its assigned applicant $i$. This blocks $N$, a contradiction.

Thus no pair belonging to any stable assignment is ever rejected. Every applicant’s terminal choice is consequently weakly preferred to its assignment in any stable assignment. $\square$

Next realize $y^*$ as a finite assignment $N^*$ on the $Q$-grid: within each type, assign consecutive cells to contracts in preference order, using exactly $Qy^*_{a,h}$ cells at $h$, and leave the final suffix unmatched.

Lemma 6. The finite assignment $N^*$ is stable.

Proof. Suppose a cell of type $a$ strictly prefers $h$ to its assignment. Then $A_a(h)>0$. Stability of $y^*$ implies $B_h(a)=0$. Hence $h$ is full and has no assigned type strictly below $a$ in its priority order.

Any type-$a$ cells assigned to $h$ occur earlier in the canonical coordinate order than a type-$a$ cell assigned to a worse contract or left unmatched. They therefore also outrank the proposed blocking cell.

Thus every applicant assigned to $h$ outranks that cell. There is no vacancy or lower-priority assignee with which it can block. $\square$

By Lemma 5, every cell weakly prefers its assignment under $z$ to its assignment under $N^*$. Hence, for every type and every rank $j$,
$$ \sum_{r=1}^{j}z_{a,h_{a,r}} \geq \sum_{r=1}^{j}y^*_{a,h_{a,r}}. $$

Also, $z$ is a stable aggregate allocation. Otherwise a pair with $A_a(h)>0$ and $B_h(a)>0$ would give a finite blocking pair: choose a type-$a$ cell assigned below $h$ or unmatched, and a vacant place or an assignee of a strictly lower-priority type at $h$.

The cumulative inequalities imply that each row of $z$ is lexicographically at least its row in $y^*$. Indeed, at the first differing entry, preceding entries agree, so the cumulative inequality gives the direction of that difference.

But $y^*$ is job-optimal among stable allocations, and $z$ is stable. Therefore no row of $z$ can be lexicographically larger. Every row agrees, proving
$$ z=y^*. $$

3.4. Running time

The actual algorithm constructs the bipartite instance and computes $y^*$ directly; it never constructs the $Q$-grid.

The stable-allocation algorithms use polynomially many graph and arithmetic operations. Their numerical updates use additions, subtractions, comparisons, and minima of residual allocations and capacities. Starting from rational input, these operations preserve the common-denominator lattice. Allocation values and residual quantities are bounded by polynomially many sums of input quotas, so their bit lengths remain polynomial.

Consequently, this is a polynomial-time exact algorithm.

Theorem 1. Exact terminal mass GDA-FD computation is polynomial-time solvable whenever its school choices are fixed-priority. In particular, it is polynomial-time solvable for constant precedence labels and for $k=1$.

This theorem permits cyclic preference transitions; it does not rely on a polynomial bound for direct simulation.

4. Polynomial termination for acyclic preference transitions

This result allows the full diversity selection rule.

Construct a directed graph $G$ whose vertices are seat classes. For every type $a$ and every $j<d_a$, add the edge
$$ h_{a,j}\longrightarrow h_{a,j+1}. $$
It records where rejected individuals can propose in the next round.

Theorem 2. If $G$ is acyclic and its longest directed path contains $\rho$ vertices, then mass GDA-FD terminates within $\rho+1$ rounds. In particular, it terminates within $s+1$ rounds and is polynomial-time computable.

Proof. Consider round $r>1$. Every proposal at $h$ comes from either:

Retained individuals repropose to $h$, since their current contract has not been rejected. Let $I_h^r$ be the mass of new arrivals. Then
$$ P_h^r=S_h^{r-1}+I_h^r, \qquad S_h^{r-1}\leq q_h. $$

If positive mass is rejected at $h$ in round $r$, Lemma 3 gives
$$ P_h^r>q_h. $$
It follows that $I_h^r>0$. Since there are finitely many types, some positive arrival mass came from rejection at a preceding contract $h'$ in round $r-1$, with
$$ h'\longrightarrow h $$
an edge of $G$.

Repeatedly applying this implication shows that a positive rejection in round $r$ produces a directed walk with $r$ vertices, tracing positive rejections back to round $1$.

In an acyclic directed graph, such a walk cannot repeat a vertex and is a directed path. Therefore
$$ r\leq\rho. $$
There are no positive rejections after round $\rho$, so the algorithm stops by round $\rho+1$.

The graph has at most $M$ listed transitions, and acyclicity can be checked in polynomial time. Section 2 gives polynomial computation of each of the at most $s+1$ rounds. $\square$

The argument applies even when multiple seat classes belong to the same school. Its essential ingredient is Lemma 3: changes in category precedence cannot cause rejection at a seat class whose proposal mass does not exceed its supply.

If $s=0$, the first round already rejects zero mass.

5. Why the fixed-priority reduction does not cover the full domain

Here is a concrete failure of substitutability, even when precedence labels only worsen as category counts increase.

There is one school and one seat class $h$ with
$$ q_h=\frac12. $$
There are four types, each of mass $1/4$, all acceptable at $h$:

| Type | Category set |
|---|---|
| $U$ | $\{\alpha,\gamma\}$ |
| $R$ | $\{\alpha\}$ |
| $S$ | $\{\gamma\}$ |
| $V$ | $\{\beta\}$ |

Static priority is
$$ U\succ R\succ S\succ V. $$
For both $\alpha$ and $\gamma$, precedence is
$$ 1\quad\text{on }[0,\tfrac14), \qquad 3\quad\text{on }[\tfrac14,1]. $$
Category $\beta$ has constant label $2$.

Let $P$ consist of the proposals from $R,S,V$, and let $P'$ additionally contain the proposals from $U$.

Under $P$, the school first selects all $1/4$ of $R$: category $\alpha$ has label $1$, and $R$ precedes $S$. Category $\alpha$ then changes to label $3$. Category $\gamma$ still has label $1$, so the school selects all $1/4$ of $S$ and fills the seat. It rejects all of $V$.

Under $P'$, the school first selects all $1/4$ of $U$. This simultaneously brings both $\alpha$ and $\gamma$ to count $1/4$, changing both labels to $3$. Category $\beta$ now has highest precedence, so the school selects all $1/4$ of $V$.

Thus adding proposals causes a previously rejected proposal to become selected.

Formally, if $C$ denotes the school choice function, substitutability would require
$$ C(P')\cap P\subseteq C(P) \qquad\text{whenever }P\subseteq P'. $$
The type-$V$ proposals violate this inclusion.

This also rules out representing this choice function by a fixed applicant order: such an order cannot reject all of $V$ from $P$ but select all of $V$ after merely adding $U$.

This is an obstruction to the reduction in Section 3, not a hardness proof. The example concerns local school choices; it makes no claim about computational difficulty of its terminal assignment.

6. Remaining question

The unrestricted algorithm has a polynomial-size state, polynomial-time rounds, finite termination, and a polynomial-space exact simulation. The new results establish polynomial-time computation in two substantial domains: fixed-priority choices and acyclic preference transitions.

Neither argument settles instances combining cyclic preference transitions with count-dependent diversity choices that change the ordering of eligible types. A polynomial acceleration for that domain, or a valid hardness reduction, is still needed.

⟨structured verdict parsed — rendered above⟩

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

The output establishes substantial partial progress, but it does not resolve the unrestricted problem in USER_TASK. The compact simulation, polynomial-space upper bound, acyclic-transition result, and non-substitutability example are sound. The fixed-priority result is sound in substance for the two explicit sufficient conditions, with minor formulation gaps.

No verified argument establishes either polynomial-time computation or $\mathrm{NP}$-hardness for the full domain.

1. Scope and contract representation

Identifying a contract with its seat class $h$ is valid because every seat class belongs to exactly one school. The refined acceptable-contract lists are strict, and $d_a\leq s$ is justified.

Allowing types with no acceptable contracts is consistent with the task: the nonempty-set requirement concerns $T(a)$, not the acceptable-contract list. Such types remain unmatched.

Scope limitation — major relative to the requested resolution. Both polynomial-time results impose additional restrictions. Neither covers arbitrary cyclic preference transitions together with count-dependent diversity choices. The prover explicitly acknowledges this limitation; it is an incomplete resolution, not a false claim of completeness.

Minimum needed: a polynomial-time algorithm for the unrestricted specified process, or a valid hardness reduction for that process.

2. Lemma 1: ordered proposal intervals

The induction is correct.

$$ v_{a,j-1}\leq u_{a,j-1}\leq v_{a,j} $$
verifies that the new boundaries remain ordered.

Thus the boundary update and its coordinatewise monotonicity are justified. Empty intervals cause no difficulty.

3. Lemma 2: arithmetic lattice and termination

The lattice argument is correct. The product $D$ of input denominators has bit length $O(L)$, even though its numerical value can be exponential in $L$.

All relevant stopping distances are differences or sums of lattice quantities. Taking their minimum introduces no new denominator.

The potential calculation is also correct:

$$ \Psi_{\mathrm{initial}}=\sum_a\mu_a d_a\leq s, $$

and

$$ \Psi-\Psi^{\mathrm{next}} = \sum_a\sum_{j=1}^{d_a}(u_{a,j}-v_{a,j}) $$

equals the total rejected mass in that round. Every round with positive rejection therefore decreases $\Psi$ by at least $1/D$.

This proves finite termination and the stated denominator-dependent bound. It does not prove a polynomial number of rounds, as the prover correctly notes.

Terminal entries have polynomial bit length because they are lattice quantities in $[0,1]$.

4. Polynomial-time rounds and polynomial space

The event count is justified:

Simultaneous events only reduce the number of events. Left-closed interval conventions justify using the new interval’s label upon reaching an internal endpoint.

Scanning explicitly represented proposals, categories, priorities, and intervals is polynomial work per event. Supplies larger than population mass do not invalidate the arithmetic bound: their binary representations and sums still have polynomial bit length.

The boundary state and selection workspace require polynomial space. Combined with finite termination, this establishes an exact polynomial-space simulation. The terminal-entry threshold decision claim follows for a binary-rational threshold.

5. Lemma 3: occupancy at each seat class

The conclusion

$$ S_h=\min\{P_h,q_h\} $$

is correct.

If a seat class has both remaining proposals and residual supply, its school cannot be full: total school capacity equals the sum of seat supplies, and selection respects each supply. Nonempty category sets ensure that some eligible proposal can be selected.

The selected proposal need not belong to the particular seat class considered in the contradiction. It suffices that selection cannot terminate while that seat class has eligible remaining proposals.

The formula for total rejected mass at a seat class follows. This does not determine the identities of rejected individuals, and the output correctly preserves that distinction.

6. Lemma 4: the explicit fixed-priority subcases

Both sufficient conditions are valid.

For constant labels, the value

$$ \alpha_b(a)=\min_{t\in T(a)}\ell_{b,t} $$

correctly determines the best represented precedence associated with type $a$. Comparing this value, then refined static priority, then coordinate yields an order independent of selected counts.

When all eligible types at a school have the same category set, every eligible proposal satisfies whichever represented category has highest precedence. Selection consequently follows static priority and coordinate.

School capacity introduces no additional competition beyond seat supplies. Therefore each seat class takes its own prefix under the resulting order.

The $k=1$ specialization follows from nonempty category sets.

Minor issue — definition of “fixed-priority.” The definition permits a fixed order on individual applicants and only specifies coordinate order within each type. Section 3.2 subsequently assumes a strict order $\succ_h$ on whole types. Those are not identical formulations without an additional qualification.

Minimum clarification: state whether “fixed-priority” requires a fixed type order followed by coordinate order. Both explicit sufficient conditions already provide that structure. Otherwise, justify the passage from the broader individual-order definition to a type order.

7. Stable-allocation theorem and its application

The cited source supports the required substantive facts: a unique job-optimal stable allocation, jobwise lexicographic optimality, and a strongly polynomial algorithm computing that allocation. Its formulation uses strict preferences, edge capacities, balanced quotas, and specially ordered dummy vertices. These facts are stated in Sections 2–3 of [Dean and Munshi](https://people.computing.clemson.edu/~bcdean/stable_alloc.pdf).

The quantities $A_a(h)$ and $B_h(a)$ correctly describe willingness to increase an acceptable real edge. The redundant edge-capacity argument is valid:

$$ A_a(h)>0\implies y_{a,h}<\mu_a, $$

and

$$ B_h(a)>0\implies y_{a,h}<q_h. $$

Thus an aggregate blocking pair cannot be excluded by saturation of the proposed redundant capacity.

The balanced-extension formulas satisfy every quota. The stated dummy-edge capacities suffice, including for the dummy-to-dummy edge.

Minor issue — dummy preference lists are incomplete. “Dummies are ranked last by real vertices” does not specify how the dummy vertices rank each other. Consequently, the assertion that every dummy edge has an endpoint ranking it last is not established for the dummy-to-dummy edge.

A concrete failure under an unspecified completion is possible: take one real type and one real seat, both of quota $1$, with no acceptable real edge. The stated extension assigns

$$ y_{a,0}=y_{0,h}=1,\qquad y_{0,0}=0. $$

If both dummy vertices rank each other above their real neighbor, their connecting edge blocks. This completion satisfies the explicitly stated requirement concerning real vertices.

Minimum clarification: give complete strict dummy preference lists, including the placement of the other dummy. The cited theorem specifies that placement explicitly. This is a routine missing construction detail, not a substantive obstruction.

8. Equality with the specified mass process

Subject to the preceding formulation clarifications, the equality argument is correct.

The conceptual denominator $Q$ makes masses, supplies, proposal boundaries, and entries of $y^*$ integral after scaling. Its potentially enormous size is harmless because the expansion is used only in the proof.

Fixed-priority school selection then agrees round by round with finite applicant-proposing deferred acceptance.

Lemma 5. The retained-priority monotonicity argument establishes stability. The earliest-rejection argument correctly establishes applicant optimality:

Strict preferences supply the required strict comparison.

Lemma 6. The canonical realization is stable. An applicant assigned below $h$ implies $A_a(h)>0$. Aggregate stability gives $B_h(a)=0$, excluding vacancy and lower-priority types. Same-type applicants assigned to $h$ precede the proposed blocking applicant in coordinate order.

The cumulative inequalities follow from individual applicant optimality. Aggregate stability of $z$ follows from finite stability, because positive aggregate blocking quantities yield actual cells witnessing a finite blocking pair.

Finally, cumulative dominance implies lexicographic dominance at the first differing entry. Job-optimality of $y^*$ excludes strict dominance by the stable allocation $z$, establishing $z=y^*$.

9. Running time of the fixed-priority reduction

The proof-only grid is correctly excluded from the implementation.

The cited algorithm’s numerical operations are compatible with the stated rational bit-complexity argument. The common-denominator lattice is preserved, and quotas, capacities, and allocation values have polynomial bit length.

Thus the explicit constant-label and single-category subcases admit exact polynomial-time computation, subject only to the minor construction clarifications above.

10. Acyclic preference transitions

Theorem 2 is correct.

For $r>1$, proposals at $h$ consist of retained individuals and arrivals from the immediately preceding acceptable contract. Hence

$$ P_h^r=S_h^{r-1}+I_h^r. $$

By Lemma 3, positive rejection requires $P_h^r>q_h$, forcing $I_h^r>0$. Finitely many types ensure that some predecessor contributes positive arrival mass.

Tracing predecessors produces a directed walk with $r$ vertices. Acyclicity makes this a path, so positive rejection requires $r\leq\rho$. The additional zero-rejection stopping round explains the bound $\rho+1$.

Shared school ownership does not invalidate the argument. The separately stated $s=0$ case is correct.

11. Non-substitutability example

The computations are correct.

Under $P$, selecting $R$ raises only $\alpha$ to its threshold, after which $S$ remains favored through $\gamma$. The capacity is filled by $R$ and $S$.

Under $P'$, selecting $U$ raises both $\alpha$ and $\gamma$ to their thresholds. Their labels become $3$, making $\beta$, with label $2$, highest precedence. The remaining capacity goes to $V$.

Thus the positive mass of $V$ violates the stated substitutability inclusion. It also rules out a fixed applicant order representing this local choice function.

The example establishes neither hardness nor a lower bound on terminal computation. The prover expressly avoids claiming either.

12. Overall adjudication

The output contains genuine results and accurately identifies its remaining limitation. The unrestricted complexity classification remains unresolved. Further work is warranted, but another round must address the unrestricted domain to settle USER_TASK.

⟨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.