← back to the atlas

d4-conf-atal-2014-0345 (d4-conf-atal-2014-0345)

Answer: Polynomial-time solvable: \(\mathrm P\).

The anchor (named result in the paper)

Theorem 1 — class: hardness

PDF text-layer excerpt — equations and symbol order may be approximateFinding an allo- cation that maximizes the utilitarian welfare is NP-hard, even when given a fixed size ℓsuch that the all the pieces given by the allocation must be of size exactly ℓ. This holds in the discrete setting as well (in which each piece is compsed of the same number of items). The mechanism we provide here finds an allocation that is guaranteed to have at least 1/2 of the optimal welfare. Both this mechanism and the one for the more general case (in which intervals of different sizes may be allocated) use a matching technique.

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

The continuous mirror question, as graded

Given a finite set of complete valuation types \(T\), rational masses \(\mu_t\) summing to \(1\), a fixed rational plot length \(\ell\), piecewise-constant rational valuation densities \(f_t\), and a piecewise-constant rational per-capita capacity profile \(b\) on \([0,1]\), determine the exact complexity of maximizing welfare over mass allocations to length-\(\ell\) intervals. Each unit of allocated mass must receive one whole interval; the mass of type \(t\) assigned to intervals is at most \(\mu_t\), and total mass assigned to intervals containing location \(z\) is at most \(b(z)\) almost everywhere. The objective is \(\sum_{t\in T}\int_{\mathcal I_\ell}(\int_I f_t(z)\,dz)\,dx_t(I)\), where \(\mathcal I_\ell=\{[a,a+\ell]:0\le a\le1-\ell\}\) and \(x_t\) is the allocation measure for type \(t\).

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

A society is given by its support: a finite list \(T\) of \(\tau\) complete valuation types with positive binary-rational masses \(\mu_t\), where \(\sum_{t\in T}\mu_t=1\). Here \(\tau\) is the support size, not the number of possible types.
The input also contains a common plot length \(\ell\in\mathbb Q\), \(0<\ell\le1\), and nonnegative piecewise-constant valuation densities \(f_t\) and per-capita capacity profile \(b\) on \([0,1]\). All breakpoints and heights are binary rationals; valuations need not be normalized. Let \(m\) be the number of cells in their common breakpoint partition and \(L\) the total input bit length. The length \(\ell\) is part of the input.
Let \(\mathcal I_\ell=\{[a,a+\ell]:0\le a\le1-\ell\}\). An allocation consists of nonnegative finite Borel measures \(x_t\) on \(\mathcal I_\ell\), identified with its start-point interval, satisfying \(x_t(\mathcal I_\ell)\le\mu_t\) and \(\sum_{t\in T}\int_{\mathcal I_\ell}\mathbf1_{\{z\in I\}}\,dx_t(I)\le b(z)\) for Lebesgue-almost every \(z\in[0,1]\).
Each allocated unit of mass receives one whole interval; a type's mass may be divided among different intervals. Unallocated mass and unused capacity are allowed. Endpoints have no effect on welfare or feasibility.
Define \(\mathrm{OPT}=\sup_x\sum_{t\in T}\int_{\mathcal I_\ell}\left(\int_I f_t(z)\,dz\right)dx_t(I)\). A binary-rational threshold \(K\) is included in the input.

Is deciding whether \(\mathrm{OPT}\ge K\) in \(\mathrm P\), with running time polynomial in \(m,\tau,L\), or is it \(\mathrm{NP}\)-hard?

For finitely many individual agents, welfare maximization with at most one plot per agent is \(\mathrm{NP}\)-hard even when all allocated plots have equal length; the same hardness is stated for consecutive blocks of indivisible items of a common size. [Source](https://www.ifaamas.org/Proceedings/aamas2014/aamas/p1045.pdf)
No result settling this exact mass-allocation problem was located in the literature search.

Modeling choices made when packaging the task

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

1. Result and notation

The decision problem is in \(\mathrm P\). There is an exact rational linear program of size polynomial in \(m,\tau,L\), even when \(1/\ell\) is exponentially large. Moreover, the supremum defining \(\mathrm{OPT}\) is attained.

Write the common partition as
\(0=p_0<p_1<\cdots<p_m=1\).
On cell \((p_{i-1},p_i)\), let the capacity be \(b_i\) and type \(t\)'s density be \(f_{t,i}\). Define
\(V_t(a)=\int_a^{a+\ell}f_t(z)\,dz\).

The proof has two parts. First, allocations can be rounded exactly onto a finite grid, which may be exponentially large. Second, that grid's linear program can be compressed to polynomial size.

2. Exact rounding to a finite grid

Define
\(G=\{p_i+k\ell:0\le i\le m,\ k\in\mathbb Z\}\cap[0,1]\)
and the allowed grid starts
\(S=G\cap[0,1-\ell]\).

These sets are finite. Also, \(0,1-\ell\in S\), and every start in \(S\) has its endpoint in \(G\).

Rounding lemma. Every feasible allocation can be replaced by an allocation supported on \(S\), preserving each type's allocated mass and its welfare.

Proof. A start already in \(S\) remains fixed. Otherwise, let \(u<v\) be its neighboring points in \(S\), and replace mass at start \(a\in(u,v)\) by masses at \(u\) and \(v\), with respective proportions
\(\lambda=(v-a)/(v-u)\) and \(1-\lambda=(a-u)/(v-u)\).

We verify that this preserves the integrated coverage of every cell of the finer partition \(G\).

The points \(u,v\) are consecutive in \(G\), and so are \(u+\ell,v+\ell\). Indeed, a grid point strictly between the latter two would translate back to a grid point strictly between \(u,v\). Furthermore, \(v-u\le\ell\): the grid contains all multiples of \(\ell\) lying in \([0,1]\).

Consequently, only the two finer cells \((u,v)\) and \((u+\ell,v+\ell)\) have coverage that changes as the start varies from \(u\) to \(v\). Their covered lengths for start \(a\) are respectively \(v-a\) and \(a-u\), exactly the stated convex combinations of the covered lengths for starts \(u,v\). Every other finer cell is either fully covered for all these starts or uncovered for all of them.

Thus, for every finer cell \(D\),
\(\int_D\mathbf1_{\{z\in[a,a+\ell]\}}\,dz =\lambda\int_D\mathbf1_{\{z\in[u,u+\ell]\}}\,dz +(1-\lambda)\int_D\mathbf1_{\{z\in[v,v+\ell]\}}\,dz\).

Apply this finite, measurable rounding kernel to each measure \(x_t\). Tonelli's theorem shows that each type's integrated coverage on each finer cell is preserved.

The rounded total coverage is constant on each open finer cell, since all interval endpoints belong to \(G\). Its value is therefore the average of the original coverage there, which is at most that cell's capacity. This proves feasibility. Since every \(f_t\) is constant on each finer cell, preserving integrated coverage also preserves welfare. The rounding proportions sum to one, so allocated type masses are preserved. ∎

The resulting finite-grid optimization has nonnegative variables \(X_{t,a}\), for \(t\in T,a\in S\), with the original capacity and mass constraints. Its feasible set is nonempty, closed, and bounded by the type-mass constraints. Hence it is compact and attains its maximum.

The lemma proves that this maximum equals \(\mathrm{OPT}\). In particular, \(\mathrm{OPT}\) is attained. We use this potentially large grid only to prove correctness; the algorithm will not enumerate it.

3. A flow formulation of the grid problem

Construct a directed graph with vertices \(G\), containing:

All arcs point to the right. For a grid vertex \(h\), define
\(d(h)=b_{\mathrm{right}}(h)-b_{\mathrm{left}}(h)\),
where the capacity outside \([0,1]\) is defined to be zero.

Thus \(d(h)=0\) unless \(h\) is an original partition breakpoint.

Flow lemma. Grid plot masses satisfy the capacity constraints if and only if they can be supplemented with nonnegative idle flows satisfying
\(\sum_{A:\operatorname{tail}(A)=h}F_A-\sum_{A:\operatorname{head}(A)=h}F_A=d(h)\)
at every grid vertex.

Proof. Given feasible plot masses, set the idle flow on each finer cell equal to its capacity minus its plot coverage. These flows are nonnegative.

At a grid vertex, plot coverage changes by the total plot flow starting there minus the total ending there. Therefore the change in idle flow, added to the plot-flow imbalance, equals the change in capacity. This is precisely the required balance equation, including at the boundary vertices.

Conversely, sum the balance equations over the vertices to the left of any finer cell. Since every arc points right, cancellation leaves the sum of flows crossing that cell. The right-hand side telescopes to its capacity. The crossing flows consist of its plot coverage and its nonnegative idle flow. Hence plot coverage is at most capacity. ∎

The absence of separate upper bounds on idle or plot arcs is useful: capacities are enforced by the balance equations.

4. Polynomially many boundary plots and terminals

Call a grid plot crossing if its interior contains an original internal breakpoint. Its possible starts form
\(C=\{a\in S:\text{some }p_j\text{ satisfies }a<p_j<a+\ell,\ 1\le j<m\}\).

There are only polynomially many such starts. For a fixed generating breakpoint \(p_i\) and an internal breakpoint \(p_j\), a start \(a=p_i+k\ell\) crossing \(p_j\) must satisfy
\((p_j-p_i)/\ell-1<k<(p_j-p_i)/\ell\).
This open interval has length one, so it contains at most one integer.

Therefore \(|C|\le(m+1)(m-1)\).

Crucially, \(C\) can be constructed without enumerating \(G\): for each pair \(i,j\), compute the candidate integer
\(k=\lceil(p_j-p_i)/\ell\rceil-1\)
and check the strict inequalities and the allowed start range. Remove duplicates.

Define the retained terminal set
\(Q=\{p_0,\ldots,p_m\}\cup C\cup\{a+\ell:a\in C\}\).
Then \(|Q|=O(m^2)\).

Every plot not in \(C\) lies wholly within one closed original cell. Within such a cell, its welfare for type \(t\) is simply \(\ell f_{t,i}\), independent of its start.

For each cell, put
\(Q_i=Q\cap[p_{i-1},p_i]\).
For terminals \(u<v\) in \(Q_i\), define
\(n_{i,u,v}=\lfloor(v-u)/\ell\rfloor\).

This is the maximum number of plot arcs that a rightward path from \(u\) to \(v\) can contain. The upper bound follows from their lengths. It is attained by plots starting at
\(u,u+\ell,\ldots,u+(n_{i,u,v}-1)\ell\),
followed by idle movement to \(v\). All these endpoints belong to \(G\).

5. The compressed linear program

Retain each crossing plot arc \(a\to a+\ell\), with variable \(X_{t,a}\) for every type.

For every cell \(i\) and terminal pair \(u<v\) in \(Q_i\), introduce:

All variables are nonnegative.

Impose the slot constraint
\(\sum_{t\in T}Z_{t,i,u,v}\le n_{i,u,v}Y_{i,u,v}\)
for every compressed arc.

Impose the type-mass constraints
\(\sum_{a\in C}X_{t,a}+\sum_i\sum_{u<v,\ u,v\in Q_i}Z_{t,i,u,v}\le\mu_t\)
for every type \(t\).

Finally, impose flow balance at every terminal \(h\in Q\):
\(\sum_{A:\operatorname{tail}(A)=h}F_A-\sum_{A:\operatorname{head}(A)=h}F_A=d(h)\).

Here the flow-bearing arcs are the crossing plot arcs, with flows \(X_{t,a}\), and the compressed arcs, with flows \(Y_{i,u,v}\). The variables \(Z_{t,i,u,v}\) do not independently enter flow balance.

Maximize
\(\sum_{t\in T}\sum_{a\in C}V_t(a)X_{t,a} +\sum_i\sum_{u<v,\ u,v\in Q_i}\sum_{t\in T}\ell f_{t,i}Z_{t,i,u,v}\).

We next prove exact equivalence.

6. Proof that compression preserves the optimum

From a grid allocation to the compressed program

Supplement a feasible grid allocation with idle flows using the flow lemma. Retain the crossing plot arcs and consider the remaining graph separately inside each original cell.

Every nonterminal vertex in a cell has zero flow imbalance: the capacity is constant there, and all endpoints of crossing plot arcs belong to \(Q\).

The internal flows can therefore be decomposed into directed paths between terminals. To justify this explicitly, trace any positive-flow internal edge backward and forward through nonterminal vertices. Conservation permits continuation, and acyclicity ensures that the tracing reaches terminals. Subtract the minimum flow on the resulting path. At least one edge becomes zero. Repeating gives a finite decomposition.

Consider a path from \(u\) to \(v\) with flow amount \(w\), containing \(k_t\) plot arcs of type \(t\). Its total number of plots satisfies
\(\sum_t k_t\le\lfloor(v-u)/\ell\rfloor=n_{i,u,v}\).

Add \(w\) to \(Y_{i,u,v}\), and add \(wk_t\) to each \(Z_{t,i,u,v}\).

The slot constraint follows from the displayed inequality. Replacing a path by its compressed arc preserves its endpoint imbalances, so flow balance holds. Each plot's mass is counted once, so type-mass constraints hold.

All plots on the path lie within cell \(i\), and therefore have type-\(t\) value \(\ell f_{t,i}\). The compressed objective consequently equals the original welfare.

From the compressed program to a grid allocation

Take any feasible compressed solution. Retain its crossing plot arcs.

Fix a compressed arc \(u\to v\) in cell \(i\), and abbreviate its variables by \(Y,Z_t\), with \(n=n_{i,u,v}\).

If \(n=0\), the slot constraint forces every \(Z_t=0\); route \(Y\) entirely through idle arcs.

Otherwise, form the \(n\) consecutive slots
\([u+(j-1)\ell,u+j\ell]\), for \(1\le j\le n\).

The inequality \(\sum_tZ_t\le nY\) permits distributing the masses \(Z_t\) among these slots, with total mass at most \(Y\) in each slot. One explicit construction is to place consecutive type blocks of lengths \(Z_t\) inside \([0,nY]\), divide that interval into \(n\) bins of length \(Y\), and assign each block-bin intersection to the corresponding type and slot.

Let \(c_{t,j}\) denote the resulting masses. Then
\(\sum_{j=1}^n c_{t,j}=Z_t\)
and
\(\sum_t c_{t,j}\le Y\).

On slot \(j\), send flow \(c_{t,j}\) through the type-\(t\) plot arc, and send the remaining flow \(Y-\sum_t c_{t,j}\) through idle arcs across that slot. After the last slot, route \(Y\) through idle arcs to \(v\).

This expands the compressed arc into grid flows with exactly its endpoint imbalances and zero imbalance elsewhere. It contributes exactly \(Z_t\) allocated mass and exactly \(\ell f_{t,i}Z_t\) welfare for type \(t\).

Expand every compressed arc this way and add all contributions. The resulting full-grid flow satisfies the balance equations. By the flow lemma, its plot masses satisfy the capacity constraints. The compressed type constraints give the required bounds \(\mu_t\), and welfare is preserved.

Thus the compressed linear program has optimum exactly \(\mathrm{OPT}\). The expansion is a proof of realizability; the algorithm need not materialize its potentially enormous number of slots.

7. Size and exact decision complexity

The terminal set has size \(O(m^2)\). Each terminal belongs to at most two original cells, so
\(\sum_i|Q_i|\le2|Q|=O(m^2)\).

Consequently, the number of compressed arcs is
\(\sum_i\binom{|Q_i|}{2}=O(m^4)\).
The program has \(O(\tau m^4)\) variables and polynomially many constraints.

All coefficients have polynomial bit length:

\(V_t(a)=\sum_{i=1}^m f_{t,i}\max\{0,\min(a+\ell,p_i)-\max(a,p_{i-1})\}\).

Thus the compressed program is constructible in time polynomial in \(m,\tau,L\). Rational linear-program feasibility is decidable in polynomial time in the dimension and binary encoding length; this standard theorem is recalled in [Adler and Beling's introduction](https://adler.ieor.berkeley.edu/ilans_pubs/lp_algebraic_stoc_1992.pdf).

Add the single inequality requiring its objective to be at least \(K\), and test feasibility. Because \(\mathrm{OPT}\) is attained and the formulation is exact, this is equivalent to deciding \(\mathrm{OPT}\ge K\).

8. Relation to the individual-agent hardness

The cited [Theorem 1](https://www.ifaamas.org/Proceedings/aamas2014/aamas/p1045.pdf) concerns individual agents receiving at most one interval. Here, type mass can be split freely among starts.

That distinction is used explicitly in the reverse construction: any totals \(Z_t\) satisfying the slot constraint can be divided among the available slots. Hence the individual-agent hardness does not transfer to this mass-allocation problem.

⟨structured verdict parsed — rendered above⟩

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

Verification report

Verdict: proved. The output establishes an exact polynomial-size rational linear programming formulation for the stated mass-allocation problem. The rounding lemma, flow formulation, and both directions of compression are valid. The bit-complexity argument supports polynomial-time exact threshold decision, including when \(1/\ell\) is exponentially large.

No major or minor mathematical issues were found.

1. Scope and definitions

The argument addresses the problem in USER_TASK: allocations are nonnegative measures, type mass may be divided among starts, and both unallocated mass and unused capacity are allowed.

The finite-grid variables represent allocated mass rather than indivisible agents. The constraints retain the separate bounds \(\mu_t\), and the objective uses the given, potentially unnormalized densities. No normalization assumption is introduced.

The use of open partition cells is consistent with almost-everywhere capacity constraints and the task’s convention that endpoints have no effect.

2. Finite grid and exact rounding

The grid \(G\) is finite because \(\ell>0\): for each fixed breakpoint \(p_i\), only finitely many integers \(k\) satisfy \(0\le p_i+k\ell\le1\).

The endpoint claims are correct:

For a nongrid start \(a\), neighboring starts \(u<v\) therefore exist. They are also consecutive in \(G\), since any intervening grid point would lie in the allowed start range.

The translation argument establishing that \(u+\ell\) and \(v+\ell\) are consecutive in \(G\) is valid. Any intervening grid point would translate back to a grid point between \(u\) and \(v\).

The bound \(v-u\le\ell\) follows from the presence of the multiples of \(\ell\) in the grid. Consequently, the two varying finer cells do not overlap in their interiors. Their covered lengths are correctly computed as \(v-a\) and \(a-u\). The stated rounding weights reproduce both lengths exactly. Coverage on every other finer cell is constant as the start varies.

The passage from pointwise rounding to rounding Borel measures is justified. The kernel has finitely many pieces with measurable weights. The coverage indicators are measurable and nonnegative, so Tonelli’s theorem applies.

After rounding, coverage is constant on every open finer cell. Its value equals the original coverage averaged over that cell. Since capacity is constant there and the original constraint holds almost everywhere, that average is at most capacity. Thus feasibility is preserved.

Typewise integrated coverage preservation implies welfare preservation because each density is constant on every finer cell. The weights sum to one, so allocated type masses are also preserved.

Assessment: the rounding lemma is correct, including for arbitrary feasible finite Borel measures.

3. Attainment of the optimum

The finite-grid feasible set is nonempty: the zero allocation is feasible.

It is closed because it is defined by finitely many non-strict linear constraints. It is bounded because nonnegativity and the type-mass constraints bound every variable by its corresponding \(\mu_t\). The linear objective therefore attains a maximum.

Every grid allocation is an admissible continuous allocation, and every admissible continuous allocation has a grid replacement with identical welfare. These two inclusions establish equality of optimal values and attainment of the continuous supremum.

Assessment: the attainment claim is justified.

4. Flow formulation

The sign convention for \(d(h)=b_{\mathrm{right}}(h)-b_{\mathrm{left}}(h)\) agrees with the stated outgoing-minus-incoming balance equations.

In the forward direction, idle flow equals capacity minus plot coverage on each finer cell and is nonnegative. The change in plot coverage at a vertex is the starting plot flow minus the ending plot flow. Adding the idle-flow change gives exactly the capacity change.

Defining exterior capacity as zero handles both boundary vertices consistently.

In the reverse direction, summing balance equations over a prefix of vertices cancels internal arcs. Since all arcs point right, the remaining sum consists precisely of flows crossing the selected finer cell. The right-hand side telescopes to that cell’s capacity. Nonnegative idle flow then gives the required capacity inequality.

Parallel plot and idle arcs cause no problem: their contributions are included separately in the balances.

Assessment: the flow lemma proves the claimed equivalence.

5. Crossing plots and retained terminals

For fixed generating breakpoint \(p_i\) and internal breakpoint \(p_j\), the crossing condition gives the stated open interval of length one for \(k\). Such an interval contains at most one integer. The bound \(|C|\le(m+1)(m-1)\) is therefore valid; duplicate representations only reduce the count.

The candidate \(k=\lceil(p_j-p_i)/\ell\rceil-1\), followed by the strict-inequality and start-range checks, correctly handles both integral and nonintegral quotients.

The terminal set contains all original breakpoints and all endpoints of crossing plot arcs. Every remaining plot is contained in one closed original cell, where its typewise value is \(\ell f_{t,i}\).

For terminals \(u<v\) within a cell, a rightward path containing \(k\) plot arcs must satisfy \(k\ell\le v-u\). The proposed consecutive-slot path attains the resulting bound \(\lfloor(v-u)/\ell\rfloor\). Its endpoints belong to \(G\), and any remaining distance can be traversed by idle arcs.

Assessment: the counting, enumeration, and slot-count claims are correct.

6. Compression equivalence

Grid allocation to compressed solution

After crossing arcs are retained separately, every nonterminal vertex in each cell has zero imbalance. Capacity changes occur only at original breakpoints, and crossing-arc endpoints are terminals.

The supplied path-decomposition argument is valid for this finite acyclic graph. Tracing continues through nonterminals by conservation and reaches terminals by acyclicity. Each subtraction eliminates at least one positive-flow edge, ensuring finite termination.

For each decomposed path, the assigned quantities \(Y_{i,u,v}\) and \(Z_{t,i,u,v}\) correctly record path flow and typewise plot mass. The path-length bound gives the slot constraint. Replacing paths by compressed arcs preserves terminal imbalances.

Each original plot mass is counted once, and its value inside the cell is exactly the coefficient used in the compressed objective.

Compressed solution to grid allocation

The slot constraint is sufficient for the stated distribution of type masses among slots. Divisibility of type mass is explicitly permitted by the task.

For each slot, plot flows and residual idle flow sum to \(Y\). Thus each slot routes the same total flow from its left endpoint to its right endpoint. Consecutive slots cancel their intermediate imbalances, and the final idle segment completes the route to \(v\).

The expansion preserves allocated type mass and welfare exactly. Superposition preserves nonnegativity and the balance equations, so the flow lemma establishes capacity feasibility.

The case \(n=0\) is handled explicitly. If \(Y=0\), the slot constraint forces all \(Z_t=0\), so the construction contributes zero flow and zero allocated mass.

Assessment: both directions preserve feasibility and objective value. The compression introduces no relaxation gap.

7. Size, encoding, and exact decision

Each terminal belongs to at most two original closed cells. Hence the stated bound on \(\sum_i|Q_i|\), and consequently the \(O(m^4)\) bound on compressed arcs, is valid. Introducing typewise variables gives \(O(\tau m^4)\) variables and polynomially many constraints.

All coefficient constructions use rational arithmetic on numbers of polynomial binary encoding length. In particular, numerically large slot counts do not require enumerating slots: they enter the program as binary-encoded integers.

The formula for \(V_t(a)\) correctly computes the length of intersection with each original cell and multiplies it by the appropriate density. Summing polynomially many such rational terms preserves polynomial encoding length.

The invoked rational linear-programming theorem applies to the constructed finite system with rational coefficients, including equality constraints and nonnegative variables. The cited introduction confirms polynomial-time solvability in the number of coefficients and their total binary encoding length. [Adler and Beling](https://adler.ieor.berkeley.edu/ilans_pubs/lp_algebraic_stoc_1992.pdf)

Because the optimum is attained and the formulations are exact, adding the objective inequality with threshold \(K\) correctly decides \(\mathrm{OPT}\ge K\). This also handles zero or negative thresholds.

8. Boundary cases and hardness comparison

The construction accommodates \(m=1\), \(\ell=1\), zero capacities, zero densities, plots ending at breakpoints, and cells shorter than \(\ell\). Strict interior crossing conditions and zero slot counts treat these cases consistently.

The cited individual-agent theorem concerns allocations with at most one interval per agent and states hardness under a common prescribed plot size. [AAMAS 2014, Theorem 1](https://www.ifaamas.org/Proceedings/aamas2014/aamas/p1045.pdf)

The output correctly identifies the relevant distinction: its reverse compression construction divides type mass among slots. That operation is authorized here and does not assert an admissible construction for indivisible individual agents.

Required prover feedback: none. No additional lemma, correction, or clarification is needed to verify the claimed result.

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