← back to the atlas

d4-journals-geb-2022-0074 (d4-journals-geb-2022-0074)

Answer: Exact computation is polynomial-time solvable in \(m,\tau,L\). The specified rational mass IDAM always terminates at the unique student-optimal stable allocation. It has at most \(mD\) proposal rounds, where \(D\) is the common denominator of masses and capacities; its worst-case round count and round-by-round bit complexity are \(2^{\Theta(L)}\), already for \(m=\tau=2\).

The anchor (named result in the paper)

Proposition 1 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateAssume that, for every college c ∈C, fc satisfies IRC and contracts are substitutes.

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

The continuous mirror question, as graded

Given rational masses \(\mu_t\) over finitely many student types, each with a strict program ranking, score vector, and eligibility, and programs with rational per-capita capacities, compute a stable mass allocation \(x_{t,c}\) that is student-optimal among stable allocations. In a type-level IDAM, each type proposes to its best currently available program and a program may split mass at a score cutoff: does the process terminate and return such an allocation, and what is its complexity in the number of programs, support size, and input bit length?

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 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.
There are \(m\ge1\) programs with positive rational per-capita capacities \(q_c\) and rational minimum scores \(b_c\). Type \(t\) has rational scores \(z_{tc}\) and a strict ranking \(\succ_t\) over programs and the unmatched option \(\varnothing\); eligibility means \(z_{tc}\ge b_c\). Scores at each program are distinct across different support types; mass within a type is divisible and indistinguishable.
An allocation satisfies \(x_{td}\ge0\), \(\sum_{d\in C\cup\{\varnothing\}}x_{td}=\mu_t\), and \(\sum_t x_{tc}\le q_c\), with \(x_{tc}=0\) unless \(t\) is eligible and \(c\succ_t\varnothing\).
It is stable if there are no eligible \((t,c)\) and \(d\) with \(x_{td}>0\) and \(c\succ_t d\) such that either \(\sum_u x_{uc}<q_c\), or \(x_{uc}>0\) for some \(u\) with \(z_{tc}>z_{uc}\).
Student-optimal means that, for every stable allocation \(y\), every type \(t\), and every ranking prefix \(B\), \(\sum_{d\in B}x_{td}\ge\sum_{d\in B}y_{td}\).
Define synchronous mass IDAM using cumulative offered amounts \(a_{tc}\), initially zero. Programs hold \(h_{tc}=\min\{a_{tc},\max\{0,q_c-\sum_{u:z_{uc}>z_{tc}}a_{uc}\}\}\), splitting the cutoff type when necessary.
In each round, each type's active unheld mass proposes to its best acceptable eligible program satisfying \(a_{tc}<\max\{0,q_c-\sum_{u:z_{uc}>z_{tc}}a_{uc}\}\); add these proposals to \(a\) simultaneously and recompute \(h\). Held mass stays committed until rejected; active mass with no such program becomes permanently unmatched. Stop when no proposal is made.

Is exact computation of a student-optimal stable mass allocation polynomial-time in \(m,\tau,L\), or NP-hard?
Does the specified mass IDAM always terminate at such an allocation, and what are its worst-case round count and bit complexity in \(m,\tau,L\)?

For finite students with score priorities, unbounded IDAM under straightforward choices terminates at the student-optimal stable matching; standard deferred acceptance computes that matching in polynomial time ([Bó–Hakimov](https://doi.org/10.1016/j.geb.2022.07.001)).
For real-valued stable allocation, strongly polynomial algorithms and side-optimal stable allocations are known; a related greedy procedure can require arbitrarily many steps even with two agents on each side ([Baïou–Balinski, corrected version](https://pubsonline.informs.org/doi/pdf/10.1287/moor.27.4.662.302)).

Modeling choices made when packaging the task

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

Result

Exact computation of a student-optimal stable mass allocation is polynomial-time solvable in \(m,\tau,L\).

The specified synchronous mass IDAM always terminates at that allocation for rational input. However, its round-by-round execution has exponential worst-case round count and bit complexity: \(2^{\Theta(L)}\), already with \(m=\tau=2\).

More precisely, let \(D\) be the least common multiple of the denominators of the normalized masses and capacities. Counting only rounds that make a positive proposal, IDAM takes at most \(mD\) rounds. A dyadic family below takes exactly \(D-1\) rounds.

1. Notation and basic properties of IDAM

Let \(E\) consist of the acceptable eligible pairs:

\[ E=\{(t,c):z_{tc}\ge b_c,\ c\succ_t\varnothing\}. \]

Only pairs in \(E\) can receive proposals or allocation. Write \(u>_c t\) when \(z_{uc}>z_{tc}\), and define

\[ R_{tc}(a)=\max\left\{0,q_c-\sum_{u>_c t}a_{uc}\right\}. \]

Thus \(h_{tc}=\min\{a_{tc},R_{tc}(a)\}\). Call an edge available when \(a_{tc}<R_{tc}(a)\), and closed otherwise.

Cumulative offers never decrease. Consequently, residuals never increase, and an edge that closes remains closed.

Let \(M_t\) denote the mass of type \(t\) already declared permanently unmatched. Its active mass is

\[ r_t=\mu_t-M_t-\sum_c h_{tc}. \]

We first establish that the procedure remains feasible and that

\[ 0\le a_{tc}\le\mu_t. \]

Initially these assertions hold. Suppose type \(t\) proposes its active mass \(r_t\) to an available edge \((t,c)\). Availability implies \(h_{tc}=a_{tc}\), so

\[ a_{tc}+r_t =a_{tc}+\mu_t-M_t-\sum_jh_{tj} \le\mu_t. \]

After simultaneous proposals, a holding on an edge that received no proposal cannot increase, because its offer stays fixed and its residual cannot increase. The holding on the proposed edge increases by at most \(r_t\). Therefore the new total holding of type \(t\) is at most \(\mu_t-M_t\).

Declaring active mass permanently unmatched also preserves this inequality. Program feasibility follows directly from the holding formula: scanning types in decreasing score order accepts their offers until capacity is exhausted.

These observations prove the assertions inductively.

A further consequence will be used repeatedly:

Preference progression. If \((t,c)\) is currently available, type \(t\) has never proposed to a program worse than \(c\), and has never been declared permanently unmatched.

Indeed, a proposal to a worse program would mean that \(c\) was already closed. Permanent unmatched status would likewise mean that every acceptable eligible edge was closed. Both contradict current availability.

2. A rejection invariant valid against every stable allocation

Fix any stable allocation \(y\), allowing its entries to be arbitrary real numbers. At every IDAM state, the following inequalities hold for every \((t,c)\in E\):

\[ y_{tc}\le R_{tc}(a), \tag{1} \]

\[ \sum_{j\succ_t c}y_{tj}\le\mu_t-a_{tc}. \tag{2} \]

The sum in (2) runs over programs; unacceptable or ineligible programs have zero allocation.

Initially \(a=0\). Inequality (1) follows from program feasibility, and (2) from type feasibility.

Assume both inequalities hold before a round, and write \(a'\) for its new cumulative offers.

Updating the demand inequality

Consider a type \(t\) proposing to \(c\). Every acceptable eligible program preferred to \(c\) is closed. Hence, for each such program \(j\),

\[ h_{tj}=R_{tj}(a). \]

By preference progression, \(M_t=0\), and type \(t\) holds no mass at programs worse than \(c\). Also, \(h_{tc}=a_{tc}\), because \((t,c)\) is available. Thus its proposal gives

\[ a'_{tc}=a_{tc}+r_t =\mu_t-\sum_{j\succ_t c}h_{tj}. \]

Using the old inequality (1),

\[ \sum_{j\succ_t c}y_{tj} \le\sum_{j\succ_t c}R_{tj}(a) =\sum_{j\succ_t c}h_{tj} =\mu_t-a'_{tc}. \]

Thus (2) holds for the updated offer. It remains unchanged on edges receiving no proposal. This establishes (2) for all edges simultaneously.

Updating the rejection bound

Suppose, towards a contradiction, that

\[ y_{tc}>R_{tc}(a') \]

for some \((t,c)\in E\). Put \(H=\sum_{u>_c t}a'_{uc}\). The preceding strict inequality implies

\[ H+y_{tc}>q_c. \]

Program feasibility of \(y\) gives

\[ \sum_{u>_c t}y_{uc}\le q_c-y_{tc}<H. \]

Therefore some higher-priority type \(u>_c t\) satisfies \(y_{uc}<a'_{uc}\). Its offer is positive, so \((u,c)\in E\). Applying the already established new inequality (2),

\[ \sum_{j\succ_u c}y_{uj}+y_{uc} \le\mu_u-a'_{uc}+y_{uc} <\mu_u. \]

Thus type \(u\) has positive mass at an option worse than \(c\). Meanwhile, \(y_{tc}>0\), and \(t\) has lower priority than \(u\) at \(c\). This is precisely a blocking pair, contradicting stability of \(y\).

Consequently (1) also holds after the round. Induction proves both invariants.

This argument compares IDAM with all real-valued stable allocations; it does not restrict comparison allocations to a rational grid.

3. Termination, stability, and student optimality

Finite termination

All offers, holdings, active masses, and unmatched masses remain integer multiples of \(1/D\). This follows because the updates use only addition, subtraction, minima, and maxima.

Every proposal round therefore increases \(\sum_{t,c}a_{tc}\) by at least \(1/D\). On the other hand,

\[ \sum_{t,c}a_{tc}\le\sum_t m\mu_t=m. \]

Hence the number \(N\) of proposal rounds satisfies

\[ N\le mD. \]

There is at most one additional final round that makes no proposal and declares any remaining active mass unmatched.

Stability of the terminal allocation

Set \(x_{tc}=h_{tc}\) at termination, and assign the remaining type mass to \(\varnothing\).

Suppose type \(t\) has positive mass at an option worse than an acceptable eligible program \(c\). Then \((t,c)\) is closed at termination:

For a closed edge, \(a_{tc}\ge R_{tc}(a)\). We claim that the program is filled entirely by types with priority at least that of \(t\):

\[ \sum_{u>_c t}h_{uc}+h_{tc}=q_c. \]

To see this, let \(H=\sum_{u>_c t}a_{uc}\).

If \(H\ge q_c\), higher-priority offers alone fill the program. If \(H<q_c\), all higher-priority offers are held, and

\[ h_{tc}=R_{tc}(a)=q_c-H. \]

In either case, \(c\) has neither slack capacity nor a positive holding of a lower-priority type. Hence \((t,c)\) cannot block. This proves stability.

Student optimality

Let \(y\) be any stable allocation and \(B\) any ranking prefix for type \(t\).

If \(x_t(B)=\mu_t\), then \(x_t(B)\ge y_t(B)\) follows from feasibility.

Otherwise, some positive mass of \(t\) lies outside \(B\). Every acceptable eligible program \(c\in B\) is preferred to that mass, and therefore is closed. The rejection invariant gives

\[ y_{tc}\le R_{tc}(a)=h_{tc}=x_{tc}. \]

Summing over the programs in \(B\) proves \(y_t(B)\le x_t(B)\). A prefix containing \(\varnothing\) already contains every option that can receive positive allocation, so that case was covered by \(x_t(B)=\mu_t\).

Thus IDAM satisfies exactly the stated student-optimality definition.

The student-optimal allocation is unique: mutual prefix dominance between two such allocations makes every prefix sum equal; differences of consecutive prefix sums determine every entry.

4. Polynomial-time computation of the outcome

The preceding proof establishes correctness of IDAM, but its termination bound is not polynomial in the input bit length. A different algorithm computes its outcome efficiently.

Exact reduction to stable allocation

Construct a bipartite stable-allocation instance with:

All vertex quotas are positive. Preferences are strict: this is given for types, and follows from distinct support-type scores for programs. The instance has at most \(\tau m\) edges.

Unallocated row quota represents unmatched mass.

To verify the stability correspondence, define

\[ P_{tc}(x)=\sum_{j\succeq_t c}x_{tj}, \qquad Q_{tc}(x)=\sum_{u:\,z_{uc}\ge z_{tc}}x_{uc}. \]

The task’s blocking condition is equivalent to

\[ P_{tc}(x)<\mu_t \quad\text{and}\quad Q_{tc}(x)<q_c. \]

The first inequality means positive mass lies below \(c\). The second means that \(c\) has slack or positive mass below \(t\) in its priority order.

The standard stable-allocation condition on an edge with \(x_{tc}<\pi_{tc}\) excludes exactly these simultaneous inequalities. If \(x_{tc}=\pi_{tc}=\mu_t\), then \(P_{tc}(x)=\mu_t\) automatically. Thus the stable allocations in the two models correspond exactly.

The algorithmic theorem and the preference comparison

For finite stable-allocation instances with strict preferences and nonnegative edge bounds, Baïou–Balinski’s corrected paper supplies a strongly polynomial arithmetic algorithm for a stable allocation, followed by a polynomial arithmetic algorithm for the row-optimal allocation. Stable allocations have identical row sums. Their row-optimality relation implies that, whenever \(x_{tc}<y_{tc}\), \(x_{tj}=0\) for every \(j\) worse than \(c\). See Theorem 2, Lemma 8, Theorem 10, and Corollary 4 in the [corrected paper](https://pubsonline.informs.org/doi/pdf/10.1287/moor.27.4.662.302).

This comparison implies the required prefix dominance. Indeed, if \(y_t(B)>x_t(B)\), some \(c\in B\) has \(y_{tc}>x_{tc}\). Equality of row sums forces \(x_{tj}>y_{tj}\) for some program \(j\notin B\). Since \(j\) is worse than \(c\), this contradicts the quoted row-optimality relation. Prefixes containing \(\varnothing\) again have total mass \(\mu_t\).

Therefore the computed row-optimal allocation is student-optimal in the task’s sense, and hence equals IDAM’s unique outcome.

Exact arithmetic

The cited constructions use additions, subtractions, comparisons, and minima of quotas, allocations, and residual quantities. Starting with the common denominator \(D\), these operations preserve that denominator. Feasibility bounds allocation entries, while capacities and auxiliary residuals have polynomial bit length.

Moreover,

\[ \log D\le L, \]

because an least common multiple is at most the product of the input denominators. Thus scaling by \(D\) permits exact integer arithmetic with polynomial-length integers throughout. Together with the polynomial arithmetic-operation count and polynomial preprocessing, this yields polynomial bit complexity in \(m,\tau,L\).

5. An exponential family for the specified synchronous rule

Let \(k\ge2\), \(D=2^k\), \(\varepsilon=1/D\), and \(n=D/2-1\).

There are two types and two programs, \(A,B\). Specify

\[ \mu_1=(n+2)\varepsilon,\qquad \mu_2=n\varepsilon, \]

\[ q_A=(n+1)\varepsilon,\qquad q_B=n\varepsilon. \]

The masses sum to one. Both programs are acceptable and eligible for both types. Preferences are

\[ A\succ_1 B\succ_1\varnothing, \qquad B\succ_2 A\succ_2\varnothing. \]

Program priorities are reversed:

\[ 2>_A1,\qquad 1>_B2. \]

For example, use scores \(z_{2A}=z_{1B}=2\), \(z_{1A}=z_{2B}=1\), with minimum scores zero.

Round recurrence

In round one, type \(1\) offers \((n+2)\varepsilon\) to \(A\), and type \(2\) offers \(n\varepsilon\) to \(B\). Their holdings are respectively \((n+1)\varepsilon\) and \(n\varepsilon\). Type \(1\) has active mass \(\varepsilon\).

Both initial edges are closed permanently: type \(1\)’s offer exceeds \(A\)’s capacity, and type \(2\)’s offer equals \(B\)’s capacity.

For each \(j=1,\ldots,n\), the next two rounds proceed as follows.

In round \(2j\), type \(1\) offers \(\varepsilon\) to \(B\). Its cumulative offer there becomes \(j\varepsilon\). This displaces \(\varepsilon\) of type \(2\), producing holdings

\[ h_{1B}=j\varepsilon,\qquad h_{2B}=(n-j)\varepsilon, \]

\[ h_{2A}=(j-1)\varepsilon,\qquad h_{1A}=(n+2-j)\varepsilon. \]

Type \(2\) now has active mass \(\varepsilon\).

In round \(2j+1\), type \(2\) offers that mass to \(A\), producing

\[ h_{2A}=j\varepsilon,\qquad h_{1A}=(n+1-j)\varepsilon, \]

while the holdings at \(B\) stay unchanged. Type \(1\) again has active mass \(\varepsilon\).

These proposals satisfy the availability test:

This verifies the recurrence inductively.

After round \(2n+1\), type \(1\)’s offer to \(B\) equals \(q_B\). Both its edges are now closed, so its remaining active mass \(\varepsilon\) becomes unmatched. Type \(2\) has no active mass. The terminal allocation is

\[ x_{1A}=\varepsilon,\qquad x_{1B}=n\varepsilon,\qquad x_{1\varnothing}=\varepsilon, \]

\[ x_{2A}=n\varepsilon,\qquad x_{2B}=x_{2\varnothing}=0. \]

The number of proposal rounds is exactly

\[ 2n+1=D-1=2^k-1. \]

All numerical inputs are dyadic, and their total encoding length is \(\Theta(k)\). Consequently the round count is \(2^{\Omega(L)}\), even with \(m=\tau=2\).

6. Round count and bit complexity

After sorting program priorities, one round can be implemented with \(O(m\tau)\) arithmetic operations: priority scans compute residuals and holdings, and preference scans select proposals.

Scaling masses and capacities by \(D\) makes these integer operations. All integers have \(O(L)\) bits, so elementary addition and comparison give \(O(m\tau L)\) bit operations per round.

For round-by-round simulation, therefore,

\[ T_{\mathrm{bit}} \le \operatorname{poly}(m,\tau,L)+O(m\tau L N) \le \operatorname{poly}(m,\tau,L)+O(m^2\tau LD). \]

Since \(D\le2^L\), this is \(2^{O(L)}\). The explicit family forces \(2^{\Omega(L)}\) rounds, and therefore at least that many operations in any execution that processes every round. Thus both worst-case round count and round-by-round bit complexity are \(2^{\Theta(L)}\).

This exponential simulation cost does not apply to computing the terminal allocation directly, which is polynomial-time solvable by Section 4.

For the elementary boundary cases, \(m=1\) permits at most one proposal round; \(\tau=1\) permits at most \(m\), because every round either completes the allocation or closes the proposed program.

⟨structured verdict parsed — rendered above⟩

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

The output resolves the intended task in substance. The IDAM correctness proof, exponential example, and polynomial-time reduction withstand verification. There is one minor domain-of-notation issue: several statements must explicitly restrict edges and sums to acceptable eligible pairs.

The appropriate classification is proved_with_minor_gaps.

Cumulative offers only increase, so each residual \(R_{tc}(a)\) only decreases. Consequently, a closed edge remains closed.

On a proposed edge, availability implies \(h_{tc}=a_{tc}\). The displayed bound
\[ a_{tc}+r_t\le\mu_t \]
follows directly from the definition of active mass and nonnegativity of other holdings and permanently unmatched mass.

Simultaneous proposals do not invalidate the argument: holdings on unproposed edges cannot increase, while the holding on the one proposed edge increases by at most that type’s active mass. Program feasibility follows from the priority scan implicit in the holding formula. These steps are correct.

For an edge in \(E\), current availability means it was available throughout the preceding execution. A type therefore could not previously have proposed to a worse program or exhausted all its acceptable eligible programs. The claimed preference progression follows.

Minor issue: the statement “If \((t,c)\) is currently available” does not explicitly require \((t,c)\in E\). Without that restriction, it is false.

A concrete failure occurs with one type and two acceptable programs \(A\succ_t B\), each of capacity one, where the type is ineligible for \(A\) and eligible for \(B\). The type proposes to \(B\), while \(a_{tA}=0<R_{tA}(a)=1\). Thus the numerically available pair \((t,A)\) does not satisfy the claimed progression.

Minimum clarification: define availability and closure only for pairs in \(E\), or explicitly restrict the preference-progression statement to \(E\). All substantive uses of the statement concern such pairs.

Both initial inequalities follow from feasibility.

For the demand update, preference progression correctly establishes that the proposing type has no permanently unmatched mass and no holdings below its proposed program. The identity
\[ a'_{tc}=\mu_t-\sum_{j\succ_t c}h_{tj} \]
is therefore correct.

Minor issue, part of the same domain problem: the subsequent equality
\[ \sum_{j\succ_t c}R_{tj}(a)=\sum_{j\succ_t c}h_{tj} \]
is valid only when the sum is restricted to eligible acceptable programs. An ineligible program preferred to \(c\) can have \(a_{tj}=h_{tj}=0\) but \(R_{tj}(a)>0\). The observation that its allocation in \(y\) is zero does not make its residual zero.

Minimum clarification: restrict this comparison chain to programs \(j\) satisfying \((t,j)\in E\). The other terms in the allocation and holding sums are zero, so this is an expositional correction.

The rejection-bound update is otherwise correct. From the alleged violation and program feasibility, the proof obtains a higher-priority type \(u\) with \(y_{uc}<a'_{uc}\). Positive cumulative offer ensures \((u,c)\in E\). The updated demand inequality then implies positive allocation below \(c\), while \(y_{tc}>0\) supplies a lower-priority occupant at \(c\). This contradicts stability exactly as defined.

The invariant genuinely applies to arbitrary real-valued comparison allocations; it does not assume their entries lie on the rational grid.

The grid argument is valid. All numerical updates preserve multiples of \(1/D\), and every positive-proposal round increases total cumulative offers by at least \(1/D\).

The bound \(a_{tc}\le\mu_t\) gives
\[ \sum_{t,c}a_{tc}\le m, \]
hence at most \(mD\) positive-proposal rounds. One additional round suffices to declare any remaining active mass unmatched and detect that no proposal is made.

Permanently unmatched mass does not compromise this argument because closed eligible edges never reopen.

Positive mass below an acceptable eligible program implies that its edge is closed at termination. Both cases—allocation to a worse program and allocation to the unmatched option—are correctly covered.

The closed-edge calculation is correct in both cases \(H\ge q_c\) and \(H<q_c\). It establishes that capacity is filled by types with priority at least that of \(t\), excluding both possible blocking conditions.

Eligible programs ranked below the unmatched option cannot create omitted blocking pairs: every positively allocated option is ranked at least as high as the unmatched option.

The prefix-dominance proof is sound. If a prefix does not contain all the type’s allocated mass, every eligible acceptable program in that prefix is closed, and the rejection invariant bounds its allocation in every stable \(y\) by its terminal holding. Prefixes containing the unmatched option contain every option permitted to receive positive allocation.

Mutual prefix dominance also correctly proves uniqueness of the student-optimal allocation.

The reduction preserves feasibility and stability. In particular, the two strict inequalities involving \(P_{tc}(x)\) and \(Q_{tc}(x)\) express exactly the two sides of a blocking pair. The edge upper bound \(\pi_{tc}=\mu_t\) creates no discrepancy: when attained, the type cannot have mass below that edge.

I checked the cited results in the [corrected Baïou–Balinski paper](https://pubsonline.informs.org/doi/pdf/10.1287/moor.27.4.662.302). Theorem 2 bounds the inductive algorithm’s generated allocations by \(3|E|+m\); Lemma 8 gives equal row totals across stable allocations; Theorem 10 and Corollary 4 provide row-optimal existence and the polynomial bound on its algorithm. The preference relation used by the prover is the paper’s stated relation. The hypotheses—positive vertex quotas, nonnegative edge bounds, finite sets, and strict preferences—are satisfied, without any nondegeneracy assumption.

The conversion from that relation to prefix dominance is correct: equal row totals force a compensating excess outside a deficient prefix, contradicting the stated restriction on allocations below the deficient edge.

The exact-arithmetic justification also stands. The cited updates preserve the common denominator, and the allocation, residual, and adjustment quantities have polynomial bit length. The inequality \(\log_2 D\le L\) follows from bounding the least common multiple by the product of encoded denominators.

The masses are positive for \(k\ge2\), sum to one, and satisfy every eligibility, acceptability, and distinct-score requirement.

The round recurrence checks out, including the endpoints \(j=1\) and \(j=n\). Each even round transfers active mass \(\varepsilon\) to \(B\), and each following odd round transfers the resulting active mass to \(A\). Every proposed edge passes the availability test.

After round \(2n+1\), the stated holdings and unmatched mass are correct. There are exactly
\[ 2n+1=D-1 \]
positive-proposal rounds. The least common denominator is indeed \(D\), since \(q_A=1/2-\varepsilon\) has reduced denominator \(D\). The family has total encoding length proportional to \(k\), establishing the claimed exponential lower bound.

Priority and preference scans give the stated arithmetic cost per round. Scaling by \(D\) yields integers of \(O(L)\) bits, including capacities, so the bit-cost upper bound is valid.

Combined with the explicit exponential number of rounds, this establishes exponential worst-case complexity for execution that processes each round. The output correctly distinguishes this from directly computing the terminal allocation.

The boundary claims for one program and one support type are also correct.

No major issue or false central step was found. The minimum repair is to make the \(E\)-restriction explicit wherever availability, preference progression, or equality between residual and holding sums is used.

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