Answer: No everywhere-terminating exact Robertson–Webb protocol exists, so worst-case query complexity has no finite bound. Explicit rational piecewise-constant densities admit polynomial-time feasibility testing and an output-polynomial allocation construction using zero Robertson–Webb queries.
Theorem 4 — class: algorithmic
Given a distinguished root with a valuation oracle, a finite support \(\Theta\) of branch types with rational masses \(\mu_\theta\), and a specified cake-capacity measure \(\sigma\) that accounts for per-capita branch supply and the root’s bundle, compute a locally envy-free allocation. A type records its manager’s valuation and whether it has a leaf, including that leaf’s valuation. The output is a root bundle and, for each type, a finite-support distribution over deterministic manager–leaf bundle assignments; every realized assignment must satisfy the paper’s local envy inequalities, and total mass-weighted cake use plus the root’s use must respect \(\sigma\). What is the Robertson–Webb query complexity in \(\tau=|\Theta|\), the input bit length \(L\), and output size \(S\)?
The cake is \([0,1]\). A society is given by its support: \(\tau\geq1\) branch types with positive binary-rational masses \(\mu_\theta\) summing to \(1\); \(\tau\) counts listed types, not possible types. There is also one distinguished root of mass \(1\).
Type \(\theta\) specifies a manager valuation \(v_\theta\), a flag \(b_\theta\in\{0,1\}\), and, when \(b_\theta=1\), a leaf valuation \(w_\theta\). All valuations, including the root valuation \(v_r\), are nonnegative, additive, nonatomic probability measures accessible through standard Robertson–Webb queries.
The capacity measure is \(\sigma(E)=\int_E s(x)\,dx\), where the nonnegative piecewise-constant density \(s\) is explicitly specified on \(m\) intervals by binary-rational breakpoints and heights. Let \(L\) be the total explicit input bit length.
An allocation consists of a root bundle \(A_r\) and, for each type, finitely many assignments \((M_{\theta j},F_{\theta j})\) with positive probabilities \(p_{\theta j}\) summing to \(1\). Bundles are finite unions of intervals; \(F_{\theta j}=\varnothing\) when \(b_\theta=0\), and bundles within each realized root–manager–leaf branch are pairwise disjoint, apart from endpoints.
Every assignment must satisfy \(v_r(A_r)\geq v_r(M_{\theta j})\) and \(v_\theta(M_{\theta j})\geq v_\theta(A_r)\); when a leaf is present, also require \(v_\theta(M_{\theta j})\geq v_\theta(F_{\theta j})\) and \(w_\theta(F_{\theta j})\geq w_\theta(M_{\theta j})\). Indifference is allowed.
Complete allocation means equality of measures: \(\mathbf1_{A_r}\,dx+\sum_\theta\mu_\theta\sum_jp_{\theta j}(\mathbf1_{M_{\theta j}}+\mathbf1_{F_{\theta j}})\,dx=\sigma\). Assume an allocation of this form exists. Let \(S\) count output assignments, interval endpoints, and probability entries, with exact real quantities represented in the Robertson–Webb model.
Does computing such an allocation admit a polynomial-time protocol in \(m,\tau,L,S\), using unit-cost exact arithmetic and Robertson–Webb queries, or is it NP-hard already with explicitly given rational piecewise-constant valuation densities?
What is the worst-case Robertson–Webb query complexity in \(m,\tau,L,S\)?
For a finite society on a rooted tree where each non-root vertex has degree at most \(2\), a complete locally envy-free allocation can be computed using \(O(n^2)\) cut queries and \(O(n^3)\) evaluation queries. [Source](https://arxiv.org/pdf/2211.06458)
No result settling this precise mass-weighted, finite-support allocation problem was located.
The two valuation-access models have different answers.
Here, the output-sensitive bound means polynomial time in the size of the allocation actually produced. It does not assert that this size is polynomial in the input.
Write \(\lambda\) for Lebesgue measure and put
\(q_{\theta j}=\mu_\theta p_{\theta j}>0.\)
These weights sum to \(1\). Away from the finitely many bundle endpoints, define
\(U_{\theta j}(x)=\mathbf 1_{M_{\theta j}\cup F_{\theta j}}(x).\)
Disjointness within each realized branch gives
\(\mathbf 1_{A_r}(x)+U_{\theta j}(x)\leq 1.\)
Completeness therefore implies
\(s(x)=\mathbf 1_{A_r}(x)+\sum_{\theta,j}q_{\theta j}U_{\theta j}(x)\leq 1\)
almost everywhere. It also implies that \(s=1\) almost everywhere on \(A_r\).
There is a stronger conclusion wherever \(s=1\) outside the root bundle: there,
\(\sum_{\theta,j}q_{\theta j}U_{\theta j}(x)=1.\)
Every summand has \(U_{\theta j}(x)\leq1\), and every weight is positive. Hence every \(U_{\theta j}(x)\) must equal \(1\).
In particular, if \(s\equiv1\) and there are no leaves, every realized manager bundle is the root’s complement, up to a Lebesgue-null set. For the absolutely continuous valuations used below, this also gives equality of their values.
Fix the following explicit data:
\(s\equiv1,\qquad \tau=2,\qquad \mu_1=\mu_2=\tfrac12,\qquad b_1=b_2=0.\)
The root valuation is \(v_r=\lambda\). Choose any measurable density \(f\) satisfying
\(\tfrac12\leq f(x)\leq\tfrac32,\qquad \int_0^1 f(x)\,dx=1,\)
and give the two managers densities \(f\) and \(2-f\), respectively. These are positive nonatomic probability measures.
Let
\(a=\lambda(A_r),\qquad u=\int_{A_r}f(x)\,dx.\)
By Section 1, every manager receives the complement of \(A_r\). The root’s envy inequalities imply \(a\geq1-a\), so \(a\geq\tfrac12\). The two managers’ inequalities imply
\(u\leq\tfrac12,\qquad 2a-u\leq\tfrac12.\)
Consequently,
\(1\leq2a\leq u+\tfrac12\leq1.\)
Thus every valid allocation must satisfy
\(\lambda(A_r)=\int_{A_r}f(x)\,dx=\tfrac12.\)
Conversely, any finite union satisfying these equalities gives a valid allocation by assigning its complement to both managers, with one probability-\(1\) assignment per type.
Every instance in this subclass is feasible with constant-size output. To see this, define the cumulative function
\(F(x)=\int_0^x f(t)\,dt\)
and the continuous function
\(h(t)=F(t+\tfrac12)-F(t),\qquad 0\leq t\leq\tfrac12.\)
Its endpoint values satisfy
\(h(0)=F(\tfrac12),\qquad h(\tfrac12)=1-F(\tfrac12).\)
They lie on opposite sides of \(\tfrac12\), or both equal it. The intermediate value theorem gives a \(t\) with \(h(t)=\tfrac12\). Taking
\(A_r=[t,t+\tfrac12]\)
works. Each manager’s complement has at most two intervals.
The remaining issue is whether queries can always locate *some* finite union giving this exact bisection.
The following adversary proves impossibility even when the protocol can query all three valuations and choose arbitrary real endpoints through exact arithmetic.
Maintain a finite ordered set of recorded endpoints
\(0=x_0<x_1<\cdots<x_k=1\)
and cumulative values \(F(x_i)\), with \(F(0)=0\), \(F(1)=1\), such that
\(\tfrac12<\dfrac{F(x_{i+1})-F(x_i)}{x_{i+1}-x_i}<\tfrac32.\)
Maintain also this invariant:
No union \(B\) of the current elementary intervals has both
\(\lambda(B)=\tfrac12\) and \(F(B)=\tfrac12\).
Here, \(F(B)\) means the sum of the relevant cumulative increments. Initially there is one elementary interval, so the invariant holds.
The manager cumulative functions are \(F(x)\) and
\(G(x)=2x-F(x).\)
Their slopes satisfy the same strict bounds.
Suppose a new endpoint \(z\) is prescribed inside an existing elementary interval.
The strict slope constraints leave a nonempty open interval of permissible values for \(F(z)\): the old affine interpolation supplies one permissible value, with room to perturb it.
Consider any union of the refined elementary intervals.
For each such union having length \(\tfrac12\), at most one value of \(F(z)\) makes its value \(\tfrac12\). There are finitely many unions. Excluding these finitely many values from a nonempty open interval leaves a permissible choice.
Thus prescribed endpoints can always be inserted while preserving the invariant.
For an evaluation query, insert its endpoints by the preceding procedure. Then answer by cumulative differences: \(F(y)-F(x)\), \(G(y)-G(x)\), or \(y-x\), as appropriate.
For a cut query to the \(F\)-manager, first insert its starting endpoint \(x\). Let the requested cumulative level be \(F(x)+\alpha\).
If that level already occurs at a recorded endpoint, return that endpoint. Otherwise, it lies strictly between two consecutive recorded cumulative values. Under the current affine interpolation, its inverse lies strictly inside that elementary interval. A nonempty open interval of nearby endpoints \(z\) remains compatible with the strict slope bounds when assigned the prescribed cumulative value.
Choose \(z\) from this open interval. Any new union selecting exactly one subinterval adjacent to \(z\) has length \(C+z\) or \(C-z\). At most one \(z\) gives length \(\tfrac12\). Excluding these finitely many endpoints preserves the invariant.
A cut query to the \(G\)-manager is handled identically, prescribing \(G(z)\), equivalently \(F(z)=2z-G(z)\). A cut query to the uniform root prescribes an endpoint, so Section 3.2 applies.
All valid standard Robertson–Webb queries can therefore be answered consistently.
Suppose the protocol terminates. Insert every endpoint occurring in its finite output by Section 3.2. This does not change any previous answer.
Complete \(F\) by affine interpolation between the recorded points. The resulting density is piecewise constant and strictly between \(\tfrac12\) and \(\tfrac32\). It defines a feasible instance by Section 2 and reproduces every query answer.
The output root bundle is a union of the final elementary intervals, apart from endpoints. By the invariant, it cannot bisect both \(\lambda\) and \(F\). Section 2 shows that the output is therefore invalid.
If the interaction continues forever, its recorded values remain consistent with
\(\tfrac12(y-x)\leq F(y)-F(x)\leq\tfrac32(y-x).\)
Extend \(F\) continuously to the closure of all recorded endpoints, and interpolate affinely across the remaining gaps. The extension satisfies these bounds everywhere. It is Lipschitz, hence absolutely continuous, with derivative between \(\tfrac12\) and \(\tfrac32\) almost everywhere.
Both \(F\) and \(G=2x-F\) are strictly increasing, so their cuts are unique. The resulting valuations reproduce the entire interaction. Section 2 again supplies a constant-size feasible allocation.
Thus an infinite interaction makes the protocol nonterminating on an actual promised feasible instance.
Conclusion. No deterministic exact Robertson–Webb protocol terminates correctly on every promised instance. In particular, no polynomial—or even finite—worst-case query bound exists. The obstruction persists with constant \(m,\tau,L\) and constant-size feasible witnesses.
Now suppose all valuation densities are explicitly given as rational piecewise-constant functions, with their descriptions included in \(L\).
Refine their breakpoints and the capacity breakpoints into common cells \(I_1,\ldots,I_K\). Let \(\ell_k=\lambda(I_k)\). On cell \(k\), write the densities as
\(s_k,\qquad d^r_k,\qquad d^\theta_k,\qquad e^\theta_k,\)
where the last is used only for types with leaves. The number \(K\) and all coefficient bit lengths are polynomially bounded by \(L\).
If any positive-length cell has \(s_k>1\), the instance is infeasible by Section 1. Otherwise introduce variables:
Impose nonnegativity and the constraints
\(0\leq a_k\leq\ell_k,\qquad a_k=0\text{ if }s_k\ne1,\)
\(x_{\theta k}+y_{\theta k}\leq\ell_k-a_k,\)
\(a_k+\sum_\theta\mu_\theta(x_{\theta k}+y_{\theta k})=s_k\ell_k.\)
Set \(y_{\theta k}=0\) for leafless types. The envy inequalities are
\(\sum_k d^r_k(a_k-x_{\theta k})\geq0,\)
\(\sum_k d^\theta_k(x_{\theta k}-a_k)\geq0,\)
and, for types with leaves,
\(\sum_k d^\theta_k(x_{\theta k}-y_{\theta k})\geq0,\)
\(\sum_k e^\theta_k(y_{\theta k}-x_{\theta k})\geq0.\)
Given an allocation, take the root lengths and the probability-weighted manager and leaf lengths in each cell.
Disjointness gives the length bounds, completeness gives the capacity equations, and Section 1 gives the restriction on root lengths. Averaging each realized envy inequality gives its displayed LP inequality.
Hence every valid allocation induces an LP solution.
Take a rational feasible LP solution. Allocate a prefix of length \(a_k\) in each cell to the root. Its complement within that cell is an interval of length
\(c_k=\ell_k-a_k.\)
If \(c_k=0\), all manager and leaf lengths there are zero. For every other cell, the ratios
\(\dfrac{x_{\theta k}}{c_k},\qquad \dfrac{y_{\theta k}}{c_k}\)
are rational. Choose a positive integer \(D\) divisible by all their denominators. Put
\(h_{\theta k}=D\,\dfrac{x_{\theta k}}{c_k},\qquad g_{\theta k}=D\,\dfrac{y_{\theta k}}{c_k}.\)
These are nonnegative integers with \(h_{\theta k}+g_{\theta k}\leq D\).
Partition each nonempty cell complement into \(D\) equal consecutive blocks. For type \(\theta\), create \(D\) assignments, indexed by \(j=0,\ldots,D-1\), each with probability \(1/D\). In cell \(k\), using cyclic block indices:
Manager and leaf blocks are disjoint. Each bundle contributes at most two intervals per cell.
Every assignment has manager length \(x_{\theta k}\) and leaf length \(y_{\theta k}\) in every cell. Since densities are constant within cells, every assignment has exactly the valuation vector used in the LP. Thus all realized envy inequalities hold.
Each block belongs to the manager–leaf union in exactly \(h_{\theta k}+g_{\theta k}\) shifts. Its expected occupancy for type \(\theta\) is therefore
\(\dfrac{x_{\theta k}+y_{\theta k}}{c_k}.\)
Outside the root, total expected occupancy equals
\(\dfrac{\sum_\theta\mu_\theta(x_{\theta k}+y_{\theta k})}{c_k} =\dfrac{s_k\ell_k-a_k}{\ell_k-a_k}.\)
If \(s_k=1\), this is \(1\). If \(s_k\ne1\), then \(a_k=0\), and it is \(s_k\). Root-occupied regions have \(s_k=1\). Hence completeness holds as an equality of measures.
This proves sufficiency.
The LP is rational, bounded, and has polynomially many variables and constraints with polynomial coefficient bit length. Polynomial-time rational linear programming therefore decides feasibility and returns a rational feasible solution of polynomial bit length.
The product of the ratio denominators is a valid \(D\), with polynomial bit length, although its numerical value can be exponential.
The construction uses \(D\tau\) assignments and \(O(K)\) work per assignment. Since the output count satisfies \(S\geq D\tau\), its running time is
\(\operatorname{poly}(L,m,\tau)+O(KS).\)
All output endpoints and probabilities are rational. No valuation queries are required.
Thus explicit-density feasibility is in \(\mathrm P\), and the stated output-sensitive search bound holds.
Let \(B\geq1\), put \(c=2^{-B}\), and use one leafless type of mass \(1\). Give both root and manager the uniform valuation. Set
\(s(x)=1\text{ on }[0,c],\qquad s(x)=c\text{ on }(c,1].\)
Here \(m=2\), \(\tau=1\), and \(L=O(B)\).
In any valid allocation, the two envy inequalities force every realized manager bundle to have the same length as the root. Write this length as \(a\). Integrating completeness gives
\(2a=\int_0^1s(x)\,dx=2c-c^2,\)
so
\(a=c-\tfrac12c^2<c.\)
Because capacity is positive everywhere, the union of all manager assignments must cover the root’s complement almost everywhere. If there are \(N\) assignments, subadditivity gives
\(1-a\leq Na.\)
Therefore,
\(N\geq\dfrac{1-a}{a}>\dfrac{1-c}{c}=2^B-1.\)
As \(N\) is an integer, every allocation has at least \(2^B\) assignments.
This lower bound is attained. Let \(D=2^B\), allocate \(A_r=[0,a]\), and partition \([c,1]\) into \(D\) equal intervals \(J_1,\ldots,J_D\). Use
\(M_j=[a,c]\cup J_j,\qquad p_j=c.\)
The probabilities sum to \(1\). Every manager bundle has length
\((c-a)+c(1-c)=\tfrac12c^2+c-c^2=a,\)
so both envy inequalities hold. Every assignment covers \([a,c]\), while each \(J_j\) is covered with probability \(c\). Completeness follows.
Thus the minimum number of assignments is exactly \(2^B\). An input-only polynomial-time algorithm cannot enumerate the required output.
The cited polynomial bound is Theorem 4 for the paper’s 2-star class, which also has depth at most two. Its completeness condition partitions the cake among individual vertices. [Ghalme–Huang–Machino–Rathi, Theorem 4](https://arxiv.org/pdf/2211.06458)
Mass-weighted completeness behaves differently. In the leafless instance of Section 2, both managers must receive the entire root complement. This forces simultaneous exact bisection and creates the query obstruction, even though the underlying root–manager graph is a star.
Accordingly, the proposed alternatives are not exhaustive: the general oracle problem is not finitely solvable, whereas the explicit rational-density problem admits the requested output-polynomial construction. Its feasibility is polynomial-time decidable; exponentially large mandatory output explains why an input-only enumeration bound is unavailable.
⟨structured verdict parsed — rendered above⟩
The prover resolves the task under the standard deterministic Robertson–Webb protocol interpretation. The oracle impossibility argument, the explicit-density LP characterization, and the exponential output lower bound are sound. I found no major or minor mathematical issues requiring repair.
The representation distinction is essential: the oracle impossibility does not contradict the algorithm that reads explicitly supplied valuation densities.
The weights \(q_{\theta j}=\mu_\theta p_{\theta j}\) are positive and sum to \(1\). Branchwise disjointness implies
\[
\mathbf 1_{A_r}(x)+U_{\theta j}(x)\leq 1
\]
outside finitely many endpoints. Thus the completeness identity implies \(s\leq1\) almost everywhere.
On the root bundle, all manager and leaf indicators vanish almost everywhere, so completeness forces \(s=1\) there. Outside the root, wherever \(s=1\), a weighted average of finitely many indicators with strictly positive weights equals \(1\). Every indicator must therefore equal \(1\).
These deductions are correct. In particular, with unit capacity and no leaves, every realized manager bundle equals the root complement up to Lebesgue-null sets. The prover explicitly restricts the subsequent value comparison to absolutely continuous valuations, for which this conclusion suffices.
Both manager densities are positive probability densities: the assumed bounds on \(f\) also hold for \(2-f\), and both integrate to \(1\).
Since every manager receives the root complement, the root inequality gives \(a\geq1/2\). The manager inequalities give \(u\leq1/2\) and \(2a-u\leq1/2\). The displayed chain
\[
1\leq2a\leq u+\tfrac12\leq1
\]
is valid and forces \(a=u=1/2\).
Conversely, these two equalities make all three relevant comparisons equalities when both managers receive the complement.
The feasibility argument also checks out. The cumulative function is continuous, so \(h\) is continuous. Its endpoint values sum to \(1\), and hence bracket \(1/2\), including the equality case. The intermediate value theorem therefore supplies the stated interval. The root uses one interval and each manager at most two, giving a constant-size feasible allocation.
This establishes both the exact constraint required of any output and the feasibility promise needed by the adversary.
Initially the only elementary interval is the whole cake. Its possible unions have lengths \(0\) and \(1\), so neither simultaneously bisects the two measures. The initial average slope is \(1\), satisfying the strict bounds.
Inside an existing elementary interval, affine interpolation gives a value satisfying both new slope constraints strictly. Consequently, the permissible values contain a nonempty open interval.
A refined union selecting both new subintervals, or neither, represents an old union. A union selecting exactly one has cumulative value affine in the new recorded value, with coefficient \(1\) or \(-1\). Each such union of length \(1/2\) excludes at most one value. There are only finitely many unions.
The finite-exclusion argument therefore preserves the invariant. Previously recorded endpoints require no insertion.
Evaluation responses are consistent cumulative differences after endpoint insertion.
For an \(F\)-cut, the requested level either is already recorded or falls strictly between consecutive recorded levels. In the latter case, the affine inverse lies inside the corresponding interval. Strict slope constraints remain valid for an open interval of nearby endpoint positions when the cumulative level is fixed.
For each refined union selecting exactly one new subinterval, its length has coefficient \(1\) or \(-1\) in the new endpoint. Excluding finitely many positions prevents length \(1/2\), which is sufficient to preserve the simultaneous-bisection invariant.
The same reasoning applies to \(G\)-cuts: the imposed relation \(F(z)=2z-G(z)\) remains compatible with the strict slope bounds near the affine inverse. Uniform-root cuts prescribe endpoints and use the already verified insertion procedure.
The argument correctly covers valid standard cut queries, including zero-value and boundary cuts through the recorded-endpoint case. Positivity of the constructed densities ensures cut uniqueness.
Inserting the finitely many output endpoints preserves all previous answers and the invariant. Affine completion then produces an absolutely continuous probability valuation with the stipulated density bounds.
The output root bundle is a union of final elementary intervals modulo endpoints. It fails simultaneous bisection by the invariant and is therefore invalid by Section 2. The completed instance is nevertheless feasible.
This is a valid finite-transcript contradiction.
The maintained interval slope bounds imply the stated non-strict bounds between any pair of recorded endpoints. They ensure a unique continuous extension to their closure. Affine interpolation across complementary gaps preserves those bounds.
The resulting function is Lipschitz and absolutely continuous, with derivative in the required range almost everywhere. Both cumulative functions are strictly increasing, so every recorded cut remains the unique correct cut. Evaluations are likewise preserved.
Thus the infinite transcript corresponds to one actual feasible instance. This step correctly addresses the distinction between defeating every finite transcript and forcing nontermination on a fixed input.
The stated impossibility follows for deterministic exact protocols. The write-up does not claim a separate randomized impossibility theorem, and none is needed for the standard protocol reading of the task.
The common refinement has polynomially many cells and rational coefficients of polynomial bit length.
Every displayed LP constraint is necessary:
The prover correctly treats averaged envy inequalities as necessity only. Sufficiency is supplied separately.
A rational feasible solution exists whenever the rational LP is feasible. Prefix allocation gives the prescribed root lengths and leaves one complement interval per cell.
Cells with \(c_k=0\) are handled before division. In every other cell, choosing a common denominator makes the block counts nonnegative integers satisfying \(h_{\theta k}+g_{\theta k}\leq D\).
The cyclic construction has the required properties:
The completeness calculation is correct. If \(s_k=1\), expected occupancy outside the root is \(1\). If \(s_k\ne1\), the LP forces \(a_k=0\), and expected occupancy is \(s_k\). Root-occupied regions have capacity \(1\).
Empty manager or leaf bundles cause no difficulty: the task permits them, and all assignment probabilities remain positive.
The invoked rational-LP theorem is stated sufficiently for this application: rational linear feasibility can be decided in polynomial time, with a rational feasible solution of polynomial bit length. The LP has polynomial description size and bounded variables.
The ratio denominators consequently have polynomial bit length, and their product has polynomial bit length because there are polynomially many ratios. Its numerical value may be exponential, as acknowledged.
Generating each cyclic bundle requires only constant endpoint work per cell, without enumerating all its constituent blocks. Thus the stated output-sensitive bound follows from \(D\tau\leq S\) and polynomially bounded \(K\).
The construction uses no Robertson–Webb queries because all relevant densities are supplied explicitly.
The uniform envy inequalities force every realized manager length to equal the root length \(a\). Integrating completeness gives
\[
2a=2c-c^2,
\]
so \(a=c-c^2/2<c\).
Positive capacity outside the root forces the finite union of manager bundles to cover its complement almost everywhere. Subadditivity yields \(1-a\leq Na\). The subsequent strict bound and integer rounding correctly give \(N\geq2^B\), including \(B=1\).
The proposed construction attains the bound:
The minimum assignment count is therefore exactly \(2^B\). This verifies the claimed obstruction to input-only polynomial-time enumeration.
The source confirms that Theorem 4 concerns depth-two 2-stars and gives the quoted polynomial cut and evaluation bounds. Its allocation is a partition among individual vertices. The prover correctly distinguishes that model from mass-weighted completeness. [Ghalme–Huang–Machino–Rathi, Theorem 4](https://arxiv.org/pdf/2211.06458)
The task’s informal degree condition alone does not impose depth two. The prover appropriately corrects the scope of the citation rather than applying it to the weighted problem.
The output establishes all claimed conclusions: deterministic oracle impossibility, absence of a finite worst-case query bound, polynomial explicit-density feasibility, and an output-polynomial explicit construction with zero valuation queries. No repair feedback is needed.
⟨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.