← back to the atlas

d4-journals-geb-2023-0075 (d4-journals-geb-2023-0075)

Answer: —

The anchor (named result in the paper)

Proposition 2 — class: other

PDF text-layer excerpt — equations and symbol order may be approximateLet (Chd)d∈D be feasible and acceptant and have completions satisfying substitutability and LAD. Let (Chc)c∈C denote its rationalization satisfying substitutability and acceptance.

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

The continuous mirror question, as graded

Given a finite rational distribution μ over student types t, where each type specifies a home district and strict school ranking, per-capita school capacities, and finitely represented district and school admission rules acting on type-mass vectors, compute the school-based student-optimal stable mass assignment and the district-based COP mass assignment. Determine whether, for each type, the school-based assignment mass weakly stochastically dominates the district-based assignment mass according to that type’s ranking.

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

A society is given by its support: the list of the \(\tau\) types with positive mass, each mass \(\mu_t\) a binary rational, with \(\sum_t\mu_t=1\). Here \(\tau\) is the support size, not the number of possible types. Each type specifies a home district and a strict ranking of all \(m\) schools above being unmatched.
There are districts \(D\), school sets \(C_d\), and nonnegative binary-rational capacities \(q_c\). Write \(k_d=\sum_{t:d(t)=d}\mu_t\). Require \(|D|\ge2\), \(k_d>0\), \(q_c\le k_d\le\sum_{c\in C_d}q_c\), and \(|C_d|\ge2\) for some district.
An offer vector has coordinates \(0\le a_{tc}\le\mu_t\); cumulative offers may include the same type's mass at several schools. Admission maps are supplied as circuits using rational affine operations, minimum and maximum. Let \(L\) be the total binary input length, including these circuits. Each district map \(A_d\) chooses \(0\le A_d(a)\le a_d\), respects school capacities, and satisfies \(\sum_{c\in C_d}A_d(a)_{tc}\le\mu_t\).
Acceptance means that, whenever \(\sum_{c\in C_d}a_{tc}\le\mu_t\) for every type, rejection at \((t,c)\) implies either \(\sum_u A_d(a)_{uc}=q_c\) or \(\sum_{u,c\in C_d}A_d(a)_{uc}\ge k_d\). Each district has a supplied completion \(F_d\): it chooses from its offers, respects school capacities, and at every input either equals \(A_d\) or violates a type's mass bound. It satisfies mass substitutability, \(a-F_d(a)\le b-F_d(b)\) whenever \(a\le b\), and the law of aggregate demand, \(\sum F_d(a)\le\sum F_d(b)\).
School rules are the restrictions \(A_c(a_c)=A_d(a_c)_c\), with other school coordinates zero. They are promised to satisfy mass substitutability and acceptance \(\sum_t A_c(a_c)_t=\min\{q_c,\sum_t a_{tc}\}\).
Define simultaneous mass COP for either the district rules or the school rules as follows. Initially each type offers its entire mass to its first-ranked school. At round \(n\), let \(h^n\) be the aggregate chosen vector. Writing \(c_{t,r}\) for type \(t\)'s school of rank \(r\), keep first-rank offers equal to \(\mu_t\) and set \(a^{n+1}_{t,c_{t,r}}=\max\{a^n_{t,c_{t,r}},a^n_{t,c_{t,r-1}}-h^n_{t,c_{t,r-1}}\}\) for \(r\ge2\). The outcome is \(\lim_n h^n\).
An assignment \(z\) is feasible when \(z\ge0\), \(\sum_c z_{tc}\le\mu_t\), and \(\sum_tz_{tc}\le q_c\); its remaining mass is unmatched. School stability means \(A_c(z_c)=z_c\) and no type with positive mass at worse schools or unmatched can offer any positive amount of that mass to \(c\) and increase its chosen mass there. Student optimality means weak stochastic dominance, type by type, over every school-stable assignment.
Restrict to inputs for which both COP outcomes exist as rational feasible assignments and the school outcome is student-optimal. Denote the district outcome by \(X\) and the school outcome by \(Y\). Compute both exactly and determine whether \(\sum_{j=1}^rY_{t,c_{t,j}}\ge\sum_{j=1}^rX_{t,c_{t,j}}\) for every \(t\) and \(1\le r\le m\).
Can this computation and comparison be performed in time polynomial in \(m,\tau,|D|,L\), or is the task NP-hard?
For finite students, feasible acceptant district rules with substitutable, aggregate-demand-monotone completions induce school rules whose COP outcome is student-optimal and weakly preferred by every student to district COP. [Ehlers](https://www.sciencedirect.com/science/article/pii/S0899825623001355).
Discrete substitutable matching can require exponentially many preference-oracle queries when choice computation is not supplied explicitly. [Deng, Panigrahi and Waggoner](https://ojs.aaai.org/index.php/AAAI/article/view/10595). No exact complexity result for the mass problem specified here was located.

Modeling choices made when packaging the task

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

Partial result: dominance is settled; exact computation reduces to contraction

The requested comparison is always affirmative:
$$ \sum_{j=1}^{r}Y_{t,c_{t,j}} \ge \sum_{j=1}^{r}X_{t,c_{t,j}} \qquad\text{for every }t,r. $$

I do not settle whether exact computation is polynomial-time solvable for variable $m,\tau$. I establish a sharper complexity upper bound: under the explicit completion-circuit interpretation, exact computation reduces in polynomial time to finding the unique fixed point of a rational piecewise affine $\ell_1$ contraction. Consequently, it lies in $\mathsf{PromiseUEOPL}$, is polynomial-time solvable when $m,\tau$ are fixed, and cannot be $\mathsf{NP}$-hard under promise-preserving polynomial-time reductions unless $\mathsf{NP}=\mathsf{coNP}$.

1. Representation and scope

For the complexity results involving $X$, I assume that each supplied completion $F_d$ is represented by a rational affine/minimum/maximum circuit and that its encoding contributes to $L$. The task explicitly specifies this representation for admission maps, but is less explicit about completions; this assumption therefore remains a representation qualification.

The dominance proof below does not require completion circuits. In particular, continuity of completions follows from substitutability and aggregate demand alone.

The complexity results for $Y$ also require no additional representation assumption: its school circuits are obtained by restricting the supplied admission circuits.

2. Aggregate demand implies nonexpansiveness

Let $G$ be either the aggregate district completion $F$ or the aggregate school rule $H$, where
$$ F(a)_{tc}=F_d(a)_{tc}\quad(c\in C_d), \qquad H(a)_{tc}=A_c(a_c)_t. $$
Define its rejection map by
$$ R_G(a)=a-G(a). $$

Both maps choose from their offers, so
$$ 0\le R_G(a)\le a. $$
Their rejection maps are coordinatewise monotone. For $F$, this is the completion substitutability promise. For $H$, it follows from the school substitutability promises.

Both maps also satisfy aggregate demand. For $F$, sum the district aggregate-demand inequalities. For $H$, school acceptance gives
$$ \sum_{t,c}H(a)_{tc} = \sum_c\min\left\{q_c,\sum_ta_{tc}\right\}, $$
which is coordinatewise nondecreasing.

If $a\le b$, rejection monotonicity and aggregate demand imply
$$ \begin{aligned} \|R_G(b)-R_G(a)\|_1 &=\sum_i\bigl(R_G(b)_i-R_G(a)_i\bigr)\\ &=\sum_i(b_i-a_i)-\left(\sum_iG(b)_i-\sum_iG(a)_i\right)\\ &\le \|b-a\|_1. \end{aligned} $$
Here $i$ indexes type-school coordinates.

For arbitrary $a,b$, put $w=\min\{a,b\}$ coordinatewise. Monotonicity and the preceding inequality give
$$ \begin{aligned} \|R_G(a)-R_G(b)\|_1 &\le \|R_G(a)-R_G(w)\|_1+\|R_G(b)-R_G(w)\|_1\\ &\le \|a-w\|_1+\|b-w\|_1\\ &=\|a-b\|_1. \end{aligned} $$

Thus $R_G$ is nonexpansive in $\ell_1$. In particular, $R_G$ and $G=a-R_G$ are continuous. This proves continuity of the completions without any representation assumption.

3. COP follows the completion and reaches a least fixed point

Write coordinates in preference order:
$$ a_{t,r}=a_{t,c_{t,r}}. $$

3.1 Equality of admissions and completions along district COP

I prove by induction that every district COP round satisfies
$$ a^n_{t,r}\le R_F(a^n)_{t,r-1} \qquad(r\ge2). $$
This holds initially because every offer below first rank is zero.

Suppose it holds at round $n$. Since $a^n_{t,1}=\mu_t$,
$$ \begin{aligned} \sum_{r=1}^{m}F(a^n)_{t,r} &=\sum_{r=1}^{m}\bigl(a^n_{t,r}-R_F(a^n)_{t,r}\bigr)\\ &=\mu_t-R_F(a^n)_{t,m} +\sum_{r=2}^{m}\bigl(a^n_{t,r}-R_F(a^n)_{t,r-1}\bigr)\\ &\le\mu_t. \end{aligned} $$
Every district contribution to this sum is nonnegative. Hence each $F_d(a^n)$ respects every type's mass bound. The completion alternative therefore forces
$$ F_d(a^n)=A_d(a^n) \qquad\text{for every }d. $$

The COP update consequently reduces to
$$ a^{n+1}_{t,r}=R_F(a^n)_{t,r-1} \qquad(r\ge2). $$
The induction hypothesis implies $a^{n+1}\ge a^n$. Rejection monotonicity then gives
$$ R_F(a^{n+1})\ge R_F(a^n), $$
which proves the invariant at round $n+1$.

For school COP, the identical argument applies with $H$ in place of $F$. No completion alternative is needed there.

3.2 Least fixed points

Let
$$ \mathcal B= \left\{a:a_{t,1}=\mu_t,\quad 0\le a_{t,r}\le\mu_t\text{ for }r\ge2\right\}. $$
For $G\in\{F,H\}$ define
$$ T_G(a)_{t,1}=\mu_t, \qquad T_G(a)_{t,r}=R_G(a)_{t,r-1}\quad(r\ge2). $$

This is a monotone self-map of $\mathcal B$: rejection is monotone and lies between zero and the corresponding offer. COP offers are precisely its iterates from the bottom element of $\mathcal B$.

These iterates increase and are bounded, so they have a coordinatewise limit $a^G$. Continuity gives
$$ T_G(a^G)=a^G. $$
If $b$ is any other fixed point, the bottom element is at most $b$, and monotonicity gives $a^n\le b$ at every round. Therefore
$$ a^G\le b. $$
Thus $a^G$ is the least fixed point.

The choices converge to $G(a^G)$. The type-mass inequalities above pass to the limit, as do capacity constraints. Consequently, both limits are feasible. At the district limit, each completion is again mass-feasible and therefore equals its admission map. Hence
$$ X=F(a^F), \qquad Y=H(a^H). $$

At either fixed point, cancellation of adjacent offer and rejection coordinates gives
$$ \sum_{j=1}^{r}G(a^G)_{t,j} = \mu_t-R_G(a^G)_{t,r} \qquad(1\le r\le m). $$

Finally, identify $\mathcal B$ with the box of its free coordinates, those of ranks at least two. In these coordinates, $T_G$ is $\ell_1$ nonexpansive: inserting the fixed first-rank coordinates preserves distances, $R_G$ is nonexpansive, and retaining only preceding-rank rejection coordinates cannot increase the norm.

4. The school outcome dominates the district outcome

Fix $c\in C_d$. Let $a^{[c]}$ retain only offers to $c$, setting every other coordinate to zero.

Because each type offers at only one school in $a^{[c]}$, choosing from offers ensures that $F_d(a^{[c]})$ respects every type's mass bound. Therefore
$$ F_d(a^{[c]})=A_d(a^{[c]}), $$
and its choice at $c$ equals $A_c(a_c)$.

Apply completion substitutability to $a^{[c]}\le a$. The offer at coordinate $(t,c)$ is identical in the two inputs, so
$$ a_{tc}-A_c(a_c)_t \le a_{tc}-F_d(a)_{tc}. $$
Thus, throughout the offer box,
$$ F(a)\le H(a), \qquad R_H(a)\le R_F(a), \qquad T_H(a)\le T_F(a). $$

Iteration from the common bottom element yields
$$ a^H\le a^F. $$
Consequently,
$$ R_H(a^H)\le R_H(a^F)\le R_F(a^F). $$
Substituting into the cumulative-choice identity proves
$$ \sum_{j=1}^{r}Y_{t,c_{t,j}} \ge \sum_{j=1}^{r}X_{t,c_{t,j}} $$
for every $t,r$.

Neither student optimality nor rationality of the outcomes is needed for this conclusion.

5. Two rational-polytope lemmas

The remaining argument concerns a rational circuit map
$$ T:K\longrightarrow K, \qquad K=\prod_{i=1}^{n}[0,u_i]\subseteq[0,1]^n, $$
which is monotone and $\ell_1$ nonexpansive. Its least fixed point is denoted by $x^*$.

These hypotheses hold for the free-coordinate versions of $T_F,T_H$ under the representation assumption in Section 1.

5.1 Polynomial bit length of least or unique fixed points

Introduce a variable for every circuit gate. For each minimum or maximum gate, select an operand and impose both:

Together with affine gate equations, box constraints and fixed-point equations, each branch selection defines a rational polytope. Their union is exactly the fixed-point set with its gate evaluations.

Every such polytope is bounded: offers lie in a compact box, and gate values are uniquely determined by evaluating a finite continuous circuit.

The extended vector corresponding to $x^*$ uniquely minimizes
$$ \sum_{i=1}^{n}x_i $$
over the union. Indeed, every other fixed point is coordinatewise at least $x^*$, and equality of sums forces equality of all coordinates. Gate evaluations are unique as well.

In any branch polytope containing $x^*$, its extended vector is therefore a unique linear minimizer and hence a vertex. To justify the last inference, a nonvertex could be expressed as a nontrivial convex combination of feasible points; linearity would force both points to be minimizers.

Cramer's rule applied to a full-rank active subsystem now bounds all coordinate bit lengths polynomially in the circuit encoding. The same conclusion holds for a unique fixed point, without needing leastness: its extended vector is the sole point of every nonempty fixed-point branch polytope.

For later use, let $s$ be a polynomially bounded, computable upper bound on the dimensions and binary encodings of all branch systems, including the residual constraints used below. We may choose
$$ B=10(s+2)^4 $$
large enough that every reduced coordinate denominator of $x^*$ is at most
$$ Q=2^B. $$

5.2 A uniform bound for small residuals

Consider a bounded rational polytope
$$ P_\delta=\{z:Mz\le c+\delta d\}, $$
where $M,c,d$ do not depend on $\delta$. Suppose their dimensions and encoding lengths are bounded by $s$. With the preceding choice of $B$, the following holds:
$$ 0<\delta\le2^{-2B-1},\quad z\in P_\delta \quad\Longrightarrow\quad \exists z^0\in P_0: \|z-z^0\|_1\le\delta\,2^B. $$

Here is a direct proof, including the quantitative bounds.

Let there be $N$ variables, and suppose every rational coefficient has numerator and denominator bounded in absolute value by $2^b$, with $N,b\le s$. At a vertex, choose $N$ linearly independent active rows. Solving their equations gives
$$ z(\delta)=u+\delta v, $$
where $u,v$ are rational.

Clear the denominators in each active row, including its entries in $c,d$. The resulting integer entries have absolute value at most $2^{(N+2)b}$. The determinant bound
$$ |\det M'|\le N!\,2^{N(N+2)b} $$
and Cramer's rule show that each coordinate of $u,v$ has numerator and denominator bounded by $2^D$, where
$$ D=N(N+2)b+\left\lceil\log_2(N!)\right\rceil+2. $$

These bounds have three consequences, all covered by $B=10(s+2)^4$:

If $u$ violated a constraint of $P_0$, its positive violation would be at least $2^{-B}$. But moving to $u+\delta v$ could reduce that violation by at most
$$ \delta\,2^B\le2^{-B-1}, $$
contradicting feasibility in $P_\delta$. Thus $u\in P_0$, and the vertex is within $\delta2^B$ of $P_0$.

Every point of a nonempty bounded polytope is a convex combination of vertices. Taking the same convex combination of the corresponding vectors $u$ proves the claimed bound.

Apply this lemma to a circuit branch with its usual gate and box constraints, replacing fixed-point equations by
$$ -\delta\le x_i-T(x)_i\le\delta. $$
The branch polytope remains bounded. Therefore, whenever $\delta\le2^{-2B-1}$,
$$ \|x-T(x)\|_\infty\le\delta \quad\Longrightarrow\quad \exists y=T(y): \|x-y\|_1\le\delta\,2^B. $$
The same $B$ works for every branch; no branch enumeration is required to compute this bound.

6. Recovering the least fixed point from one contraction

Choose
$$ \gamma=2^{-4B-10}, \qquad \varepsilon=\frac{\gamma}{n+1}, \qquad \lambda=1-\varepsilon. $$
All these numbers have polynomial binary encoding length.

Define
$$ S_\lambda(x)=\lambda T(x). $$
Because $K$ has bottom element zero, $S_\lambda$ maps $K$ into itself. Moreover,
$$ \|S_\lambda(x)-S_\lambda(y)\|_1 \le\lambda\|x-y\|_1. $$
The box $K$ is complete, and $\lambda<1$, so the Banach contraction theorem gives a unique fixed point $x^\lambda$.

6.1 Its distance from the least fixed point

Since
$$ S_\lambda(x^*)=\lambda x^*\le x^*, $$
iteration of $S_\lambda$ from zero remains below $x^*$. Taking limits gives
$$ x^\lambda\le x^*. $$

Its residual for the original map satisfies
$$ \begin{aligned} \|x^\lambda-T(x^\lambda)\|_1 &=\varepsilon\|T(x^\lambda)\|_1\\ &\le\varepsilon n\\ &<\gamma. \end{aligned} $$
Section 5.2 therefore supplies a fixed point $y$ of $T$ with
$$ \|x^\lambda-y\|_1\le\gamma2^B. $$
Leastness gives $x^*\le y$. Hence
$$ 0\le x^*-x^\lambda\le y-x^\lambda, $$
and consequently
$$ \|x^*-x^\lambda\|_1 \le\gamma2^B = 2^{-3B-10}. $$

6.2 Exact rational recovery

Every coordinate of $x^*$ has reduced denominator at most $Q=2^B$. Distinct rationals with denominators at most $Q$ differ by at least $Q^{-2}$. The preceding error bound is smaller than $1/(4Q^2)$, so each coordinate of $x^*$ is uniquely identified by the corresponding coordinate of $x^\lambda$ and the denominator bound.

Recovery is polynomial-time by continued fractions. Explicitly, Legendre's approximation theorem states that if a reduced fraction $p/q$ satisfies
$$ \left|v-\frac pq\right|<\frac{1}{2q^2}, $$
then $p/q$ is a continued-fraction convergent of $v$. Here $q\le Q$ and
$$ |x_i^\lambda-x_i^*|<\frac{1}{4Q^2}<\frac{1}{2q^2}. $$
If the coordinates are equal, the target is simply the final convergent. Enumerating the convergents and retaining the unique rational with denominator at most $Q$ within the proved error bound recovers $x_i^*$.

The unique fixed point $x^\lambda$ has polynomial bit length by Section 5.1 applied to the circuit for $S_\lambda$. Thus this continued-fraction computation takes polynomial time.

We have proved the following reduction:

Given an exact fixed point of the polynomial-size contraction circuit $S_\lambda$, the least fixed point of $T$ can be recovered exactly in polynomial time.

7. Consequences for the matching task

7.1 One contraction instance computes both outcomes

Construct the free-coordinate maps $T_F,T_H$ and choose a common bound $B$ for their branch systems. Their circuit sizes are polynomial in $m,\tau,|D|,L$: school restrictions are obtained by copying district admission circuits and setting other coordinates to zero.

To put the contraction on a unit cube, define coordinatewise clipping into the free-offer box $K$:
$$ P(v)_i=\min\{u_i,\max\{0,v_i\}\}. $$
This is a rational circuit and is $\ell_1$ nonexpansive.

The combined map
$$ \widehat S(u,v)= \bigl(\lambda T_F(P(u)),\lambda T_H(P(v))\bigr) $$
maps $[0,1]^{2n}$ into itself and satisfies
$$ \|\widehat S(u,v)-\widehat S(u',v')\|_1 \le \lambda\|(u,v)-(u',v')\|_1. $$
Its fixed point lies in $K\times K$, so clipping is inactive there. It supplies the two perturbed fixed points required by Section 6.

Recover the least offer fixed points, restore first-rank coordinates, and evaluate the choice circuits. This computes $X,Y$ exactly.

7.2 A known contraction theorem applies

Fearnley, Gordon, Mehta and Savani prove that exact fixed-point computation for rational piecewise linear contraction circuits under an $\ell_p$ norm belongs to $\mathsf{PromiseUEOPL}$, and is polynomial-time solvable in fixed dimension. See Theorems 34 and 40 of [*Unique End of Potential Line*](https://arxiv.org/html/1811.03841).

All relevant hypotheses have been checked here: $\widehat S$ uses rational affine/minimum/maximum gates, maps a unit cube into itself, and has strict contraction factor $\lambda$ in $\ell_1$.

It follows that, under the completion-circuit interpretation:

The second conclusion also applies to school-outcome computation alone without any additional completion representation assumption.

7.3 Polynomial certificates for either answer to outcome questions

Let $\Pi$ be any polynomial-time Boolean predicate of the input and the exact outcomes—for example, whether a specified coordinate exceeds a supplied rational threshold.

A certificate consists of the unique rational fixed point $w$ of $\widehat S$. Its bit length is polynomial by Section 5.1. A verifier can:

Uniqueness ensures that every valid certificate yields the actual outcomes. The same certificate therefore certifies the correct answer whether $\Pi$ is true or false. Such decision questions belong to promise-$\mathsf{NP}\cap\mathsf{coNP}$.

In particular, a promise-preserving polynomial-time reduction deciding satisfiability from exact outcome computation would put satisfiability in $\mathsf{coNP}$, implying
$$ \mathsf{NP}=\mathsf{coNP}. $$
This also holds for polynomially many adaptive calls, provided every oracle call satisfies the matching promises: certificates for their contraction fixed points give a polynomial-size verifiable transcript for either final answer.

This is a conditional obstruction to $\mathsf{NP}$-hardness, not an unconditional exclusion of it.

8. What remains open

The dominance comparison is completely resolved and always returns yes.

For exact computation with variable $m,\tau$, the argument supplies a reduction to a unique contraction fixed-point problem, a fixed-dimension polynomial algorithm, and a certificate-based obstruction to ordinary promise-preserving $\mathsf{NP}$-hardness. It does not supply a polynomial-time algorithm in variable dimension or establish hardness.

The unresolved mathematical question is whether the additional matching structure permits polynomial-time computation beyond what follows from general piecewise affine contraction theory.

⟨structured verdict parsed — rendered above⟩

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

Verification report

The output establishes genuine partial progress. The dominance proof is correct, and the contraction reduction is sound under the explicitly stated completion-circuit assumption. No false central step was found. However, the output does not resolve whether exact computation in variable dimension is polynomial-time solvable or $\mathsf{NP}$-hard.

1. Scope and representation

Section 1 correctly distinguishes the supplied admission circuits from the additional assumption that completions also have rational affine/minimum/maximum circuits whose encodings contribute to $L$.

This qualification matters:

Because the qualification is explicit, it is not an unjustified hypothesis silently introduced into the proof. Nevertheless, these conditional computational results cannot be presented as unconditional results for the original input specification without clarifying completion representation.

2. Rejection nonexpansiveness

Section 2 is correct.

For comparable inputs $a\le b$, substitutability makes every coordinate of $R_G(b)-R_G(a)$ nonnegative. Consequently, its $\ell_1$ norm equals its coordinate sum. Aggregate demand then gives exactly the displayed bound.

For arbitrary inputs, the coordinatewise minimum $w$ remains in the offer domain. The triangle inequality and the comparable-input bounds apply, and
$$ \|a-w\|_1+\|b-w\|_1=\|a-b\|_1. $$

School acceptance supplies aggregate demand for $H$, while the district aggregate-demand promises supply it for $F$. Thus the continuity conclusion is justified, including for completions without circuit representations.

3. COP and least fixed points

3.1 Equality with completions along district COP

The induction in Section 3.1 is valid.

Initially, all lower-ranked offers vanish and rejections are nonnegative. Under the induction hypothesis, the telescoping calculation gives
$$ \sum_r F(a^n)_{t,r}\le\mu_t. $$

Because all district choices are nonnegative, each district’s contribution separately respects the type bound. The completion alternative therefore forces equality with its admission map.

The invariant also justifies removing the maximum from the update:
$$ \max\{a^n_{t,r},R_F(a^n)_{t,r-1}\} = R_F(a^n)_{t,r-1}. $$

Rejection monotonicity then propagates the invariant. The school version requires no completion alternative and follows by the same induction.

3.2 Existence, leastness, and identification of outcomes

Section 3.2 is correct.

The offer box is invariant under $T_G$, since each rejection lies between zero and its corresponding offer. Iteration from its bottom element increases coordinatewise and remains bounded. Continuity justifies passing to the limit in the fixed-point equation.

The comparison with any other fixed point establishes leastness, rather than merely existence.

The type bounds and capacity constraints pass to the limit. At the district limit, the completion alternative again identifies the completion with the admission map. Therefore the displayed identifications of $X$ and $Y$ follow.

The cumulative-choice identity is also correct. At a fixed point,
$$ a_{t,j}=R_G(a)_{t,j-1}\qquad(j\ge2), $$
so adjacent terms cancel, including when $r=m$.

Finally, inserting fixed first-rank coordinates preserves distances, and selecting a subset of rejection coordinates cannot increase the $\ell_1$ norm. The claimed nonexpansiveness of the free-coordinate map is justified.

4. Dominance

Section 4 correctly proves the requested comparison.

At the restricted input $a^{[c]}$, choosing from offers makes the completion type-feasible because each type offers at only one school. Hence the completion equals the admission map there.

Substitutability applies to $a^{[c]}\le a$. The equal offer coordinates at school $c$ yield
$$ A_c(a_c)_t\ge F_d(a)_{tc}. $$

This proves the stated ordering of choices, rejections, and offer-update maps. Iteration from the common bottom element then gives
$$ a^H\le a^F. $$

Both rejection inequalities used afterward have the correct directions. Substitution into the cumulative-choice identity proves dominance for every type and every rank.

The observation that this argument does not use student optimality or rationality is accurate. The district acceptance condition is also unnecessary for this particular argument.

5. Rational-polytope arguments

5.1 Polynomial bit length

Section 5.1 is sound under the circuit assumption.

Branch equations and selection inequalities describe the circuit graph exactly, including ties at minimum and maximum gates. Each branch polytope is bounded because its input coordinates lie in a compact box and its gate values are determined by circuit evaluation.

Leastness makes the extended least fixed point the unique minimizer of the coordinate-sum objective on every branch containing it. The argument that a unique linear minimizer must be a vertex is valid.

A full-rank active subsystem therefore permits Cramer’s-rule bounds. Keeping gate variables avoids expanding the circuit into potentially much larger affine expressions.

The corresponding argument for a unique fixed point is also valid.

5.2 Uniform residual bound

The quantitative argument in Section 5.2 checks out.

Clearing denominators row by row gives the stated integer-entry bound. The determinant and Cramer’s-rule estimates bound the coordinates of $u$ and $v$. The chosen
$$ B=10(s+2)^4 $$
is sufficiently large for the slope, nonzero-slack, and row-perturbation bounds stated in the proof.

For a feasible vertex of $P_\delta$, a positive violation at $u$ cannot be eliminated by a perturbation of size at most
$$ \delta2^B\le2^{-B-1}. $$

Thus its associated $u$ is feasible in $P_0$. Convex combinations preserve both feasibility and the distance bound.

The application to residual constraints is legitimate: circuit branch constraints remain exact, and only the fixed-point equalities are relaxed. The resulting nearby point satisfies the actual circuit fixed-point equations.

No branch enumeration is needed to obtain a common encoding-size bound.

6. Contraction and exact recovery

Section 6 is correct.

The scaled map preserves the box and has contraction factor $\lambda<1$, so the stated application of Banach’s theorem satisfies its hypotheses.

Monotone iteration from zero remains below $x^*$, giving
$$ x^\lambda\le x^*. $$

The residual estimate is valid because the box lies in $[0,1]^n$. The selected $\gamma$ satisfies the threshold required by Section 5.2.

The nearby fixed point $y$ satisfies $x^*\le y$ by leastness. Together with $x^\lambda\le x^*$, this justifies the distance bound to the least fixed point.

The rational-recovery argument is also valid:

The perturbed fixed point has polynomial bit length by the earlier unique-fixed-point argument, so exact continued-fraction recovery takes polynomial time.

7. Computational consequences

7.1 Combined contraction

The clipping map is $\ell_1$ nonexpansive. The product construction therefore has the stated contraction factor.

Every fixed point of the combined map lies in the free-offer boxes, making clipping inactive there. Recovering both least fixed points and evaluating their choice circuits consequently computes both outcomes exactly.

7.2 External theorem

The cited results support the claims made. Theorem 34 gives the promise-preserving containment for piecewise-linear contraction, and Theorem 40 gives exact fixed-point computation in polynomial time when dimension is fixed. The constructed rational affine/minimum/maximum circuit satisfies the relevant circuit, domain, and contraction hypotheses. See [Fearnley, Gordon, Mehta, and Savani, *Unique End of Potential Line*](https://arxiv.org/html/1811.03841).

Thus the conditional $\mathsf{PromiseUEOPL}$ upper bound and the fixed-$m,\tau$ polynomial-time conclusion are justified. The exponentially small contraction gap does not invalidate this application.

7.3 Certificates and the hardness qualification

The certificate argument is valid under the same representation assumption.

A polynomial-length rational fixed point can be checked by exact circuit evaluation. Uniqueness ensures that a valid certificate produces the actual outcomes, allowing either truth value of a polynomial-time outcome predicate to be certified.

The conditional consequence for promise-preserving reductions from satisfiability follows. The adaptive-call extension is also justified: verified unique answers determine the subsequent queries, and polynomially many polynomial-size certificates yield a polynomial-size transcript.

This establishes a conditional obstruction to $\mathsf{NP}$-hardness; it does not establish polynomial-time computation or unconditionally exclude hardness.

8. Blocking issue and actionable feedback

Major — the variable-dimension complexity question remains unresolved. Section 8 explicitly acknowledges this. A contraction reduction and fixed-dimension algorithm do not decide the complexity of exact computation when $m$ and $\tau$ vary.

To resolve USER_TASK, the prover must supply either a polynomial-time exact algorithm in the requested parameters or a hardness result with its reduction and promises verified. This requires additional mathematics, not an expositional repair.

The existing dominance proof and conditional upper bounds can stand as partial results. Any computational claim concerning $X$ must retain the completion-circuit qualification unless the input specification explicitly supplies that representation.

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