Answer: \(\text{Polynomial-time solvable, with exact expected-polynomial-time sampling}\)
Theorem 5.11 — class: algorithmic
PDF text-layer excerpt — equations and symbol order may be approximateIn PB with binary utilities, Algorithm 2 computes an integral outcome sampled from a lottery that is ex-ante Strong UFS, ex-post BB1, and ex-post EJR in poly- nomial time.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given rational project costs, budget B, a finite set of binary approval types T, and a rational mass distribution μ over T, compute in time polynomial in m, |T|, and input bit-length a feasible marginal vector p and a sampler over integral project portfolios W such that each type t receives approval mass at least the maximum attainable with budget μ_tB, every sampled W satisfies mass-scaled EJR, and every sampled W satisfies BB1.
Let \(C\) contain \(m\geq1\) projects, with binary-rational budget \(B>0\) and costs \(0\leq c_j\leq B\), satisfying \(\sum_{j\in C}c_j\geq B\); write \(c(Q)=\sum_{j\in Q}c_j\).
A society is given by its support: the list \(T\) of \(\tau\) distinct approval types with positive binary-rational masses \(\mu_t\), where \(\sum_{t\in T}\mu_t=1\). Each type specifies an approval set \(A_t\subseteq C\), possibly empty; \(\tau\) is the support size, not the number of possible approval sets. Let \(L\) be the total input bit length.
For \(b\in[0,B]\), let \(X(b)=\{x\in[0,1]^m:\sum_{j\in C}c_jx_j=b\}\). The required rational marginal vector \(p\in X(B)\) must satisfy Strong UFS: \(\sum_{j\in A_t}p_j\geq\max_{x\in X(\mu_tB)}\sum_{j\in A_t}x_j\) for every \(t\in T\).
A coalition is a vector \(a\) with \(0\leq a_t\leq\mu_t\) and \(\sum_ta_t>0\). A portfolio \(W\subseteq C\) satisfies mass-scaled EJR if, for every such coalition and every \(Q\subseteq\bigcap_{t:a_t>0}A_t\) with \(c(Q)\leq B\sum_ta_t\), some \(t\) with \(a_t>0\) has \(|A_t\cap W|\geq|Q|\).
A portfolio satisfies BB1 if either \(c(W)\leq B\) and some \(j\in C\setminus W\) has \(c(W\cup\{j\})\geq B\), or \(c(W)\geq B\) and some \(j\in W\) has \(c(W\setminus\{j\})\leq B\).
Construct \(p\) and an exact sampler for a lottery over portfolios, with \(\Pr(j\in W)=p_j\) for every project, whose every support portfolio satisfies mass-scaled EJR and BB1. Sampling time is measured in expected bit operations.
Is this construction problem solvable in polynomial time in \(m,\tau,L\), including expected time per sample, or is it \(\mathrm{NP}\)-hard?
For explicit finite voter lists, a polynomial-time randomized construction achieves ex-ante Strong UFS, ex-post EJR, and ex-post BB1 ([Aziz et al., 2024](https://arxiv.org/html/2404.05198v2)).
No result settling this exact rational-mass input construction was located in the literature search.
The construction is solvable in polynomial time in \(m,\tau,L\), with an exact sampler taking expected polynomial time per sample.
The construction uses equal shares, followed by fractional completion and dependent rounding. This is the approach underlying the finite-voter result of [Aziz et al.](https://arxiv.org/html/2404.05198v2). The proof below establishes that it can be implemented directly on rational masses, with polynomial bit complexity.
For \(R\subseteq T\), write \(\mu(R)=\sum_{t\in R}\mu_t\).
A portfolio \(W\) satisfies mass-scaled EJR if and only if the following condition holds:
For every nonempty \(R\subseteq T\) and every \(Q\subseteq\bigcap_{t\in R}A_t\) satisfying \(c(Q)\leq B\mu(R)\), some \(t\in R\) satisfies \(|A_t\cap W|\geq |Q|\).
Necessity follows by taking \(a_t=\mu_t\) for \(t\in R\) and \(a_t=0\) otherwise.
For sufficiency, let \(a\) be an arbitrary coalition and set \(R=\{t:a_t>0\}\). Then \(R\neq\emptyset\) and \(\sum_ta_t\leq\mu(R)\). Consequently, every portfolio affordable to \(a\) is affordable to the full masses of \(R\), and the stated condition supplies the required type.
Thus, there is no need to enumerate or approximate fractional coalitions.
Let \(Z=\{j:c_j=0\}\), \(C^+=C\setminus Z\), and \(A_t^+=A_t\cap C^+\). Include every project in \(Z\) in every sampled portfolio.
Run the following procedure on the positive-cost projects. Maintain a selected set \(S^+\), initially empty, and one balance \(b_t\) per type, initially \(b_t=B\). The aggregate remaining money of type \(t\) is \(\mu_tb_t\).
For an unselected project \(j\), define
\( \displaystyle F_j(\rho)=\sum_{t:j\in A_t^+}\mu_t\min\{b_t,\rho\}. \)
Project \(j\) is affordable exactly when
\( \displaystyle \sum_{t:j\in A_t^+}\mu_tb_t\geq c_j. \)
For each affordable project, compute the smallest \(\rho_j\) satisfying \(F_j(\rho_j)=c_j\). This exists because \(F_j\) is continuous, starts at zero, and eventually equals the total remaining money of its supporters.
Select a project minimizing \(\rho_j\), breaking ties by a fixed project order. If its price is \(\rho\), update each approving type by
\( \displaystyle b_t\leftarrow b_t-\min\{b_t,\rho\}. \)
Other balances remain unchanged. Stop when no unselected project is affordable.
There are at most \(m\) selection rounds. Since every selected project is paid for exactly,
\[ \displaystyle c(S^+)+\sum_{t\in T}\mu_tb_t=B. \tag{1} \]
Hereafter, \(b_t\) denotes the terminal balance, and \(S=Z\cup S^+\).
We use the established equal-shares theorem: for a finite electorate of \(n\) voters with approval utilities and positive project costs, equal shares starting with budget \(B/n\) per voter returns a set \(V\) such that every nonempty voter group \(G\) and common approved set \(Q\) with \(c(Q)\leq B|G|/n\) have some member approving at least \(|Q|\) projects in \(V\). The theorem permits arbitrary tie-breaking. See [Peters, Pierczyński, and Skowron, Theorem 2](https://arxiv.org/pdf/2008.13276).
To check its applicability, choose a common denominator \(H\) for the masses and write \(\mu_t=w_t/H\), where the \(w_t\) are positive integers summing to \(H\). Consider, only for this proof, an electorate with \(w_t\) copies of type \(t\).
At every stage, each copy of type \(t\) has balance \(b_t/H\). A price \(\rho/H\) in the finite electorate produces total payment
\( \displaystyle \sum_{t:j\in A_t^+}w_t\min\{b_t/H,\rho/H\}=F_j(\rho). \)
Therefore the compressed procedure exactly reproduces finite-voter equal shares, including its project choices and balance updates. Its positive costs and binary utilities satisfy the theorem’s hypotheses.
For nonempty \(R\subseteq T\), take all copies of types in \(R\). Their electorate fraction is \(\mu(R)\). The theorem therefore gives the full-type EJR condition from Section 1 on the positive-cost projects.
Now let \(Q\) also contain zero-cost projects. Apply this condition to \(Q^+=Q\cap C^+\). If \(Q^+\neq\emptyset\), it supplies a type \(t\in R\) with \(|A_t^+\cap S^+|\geq|Q^+|\). Since \(Z\subseteq S\), this type additionally receives every project in \(Q\cap Z\), and hence \(|A_t\cap S|\geq|Q|\). If \(Q^+=\emptyset\), every type in \(R\) already receives all of \(Q\).
Thus \(S\) satisfies mass-scaled EJR. Every superset of \(S\) also satisfies it, because approval counts can only increase.
The virtual electorate is never constructed by the algorithm.
For each type with \(A_t^+\setminus S^+\neq\emptyset\), choose a cheapest project \(h_t\) in this set and assign all its remaining money \(\mu_tb_t\) to \(h_t\).
Define funded amounts \(f_j\), for \(j\in C^+\), by
\( \displaystyle f_j= \begin{cases} c_j,&j\in S^+,\\ \sum_{t:h_t=j}\mu_tb_t,&j\notin S^+. \end{cases} \)
For every unselected project \(j\), termination of equal shares implies
\( \displaystyle \sum_{t:j\in A_t^+}\mu_tb_t<c_j. \)
The types assigning money to \(j\) are a subset of its supporters. Consequently, \(0\leq f_j<c_j\) for every unselected project. Moreover, by (1),
\( \displaystyle \sum_{j\in C^+}f_j\leq c(S^+)+\sum_t\mu_tb_t=B. \)
Increase these funded amounts, without exceeding their costs, until their sum equals \(B\). Explicitly, scan the projects in a fixed order and add to \(f_j\) the minimum of its unused capacity and the remaining budget.
This succeeds because \(\sum_{j\in C^+}c_j=c(C)\geq B\).
Finally, set
\( \displaystyle p_j= \begin{cases} 1,&j\in Z,\\ f_j/c_j,&j\in C^+. \end{cases} \)
Then \(p\in[0,1]^m\), \(p_j=1\) for all \(j\in S\), and \(\sum_jc_jp_j=B\). Hence \(p\in X(B)\).
Fix a type \(t\). Write \(z=|A_t\cap Z|\), and order its positive-cost approved projects as \(g_1,\ldots,g_s\), with costs \(d_1\leq\cdots\leq d_s\).
Put \(\beta=\mu_tB\). Let \(k\) be the largest integer with
\( \displaystyle D_k:=\sum_{r=1}^kd_r\leq\beta, \qquad D_0=0. \)
If \(k=s\), the type’s fractional optimum is \(z+s\): all its approved projects can be funded, and any remaining budget can be spent elsewhere.
If \(k<s\), define
\( \displaystyle \delta=\frac{\beta-D_k}{d_{k+1}}, \qquad 0\leq\delta<1. \)
Then its fractional optimum is \(z+k+\delta\). To verify the upper bound explicitly, for any fractional allocation to its positive approvals,
\( \displaystyle \sum_{r=1}^sd_rx_{g_r} =d_{k+1}\sum_{r=1}^sx_{g_r} +\sum_{r=1}^s(d_r-d_{k+1})x_{g_r} \geq D_k+d_{k+1}\left(\sum_{r=1}^sx_{g_r}-k\right). \)
The inequality uses \(x_{g_r}\leq1\) for the nonpositive coefficients with \(r\leq k\), and \(x_{g_r}\geq0\) for the remaining nonnegative coefficients. An allocation in \(X(\beta)\) spends at most \(\beta\) on these approvals, so its utility is at most \(z+k+\delta\). Funding the first \(k\) projects and a fraction \(\delta\) of the next attains this bound.
Let \(q=|A_t^+\cap S^+|\). The positive-cost EJR property proved above, applied to the single full type and the set \(\{g_1,\ldots,g_k\}\), gives \(q\geq k\); for \(k=0\), this is immediate.
If \(k=s\), all approvals are already selected. If \(q\geq k+1\), then the selected projects alone give utility exceeding \(z+k+\delta\). It remains to handle \(q=k<s\).
Let \(h_r\) be the \(r\)-th positive-cost approved project selected for type \(t\), and let \(y_r\) be this type’s aggregate payment for it. We claim
\[ \displaystyle y_r\leq d_r. \tag{2} \]
Immediately before \(h_r\) is selected, only \(r-1\) projects approved by this type have been selected. Thus some project \(g\in\{g_1,\ldots,g_r\}\) remains available, with \(c_g\leq d_r\).
Suppose instead that \(y_r>d_r\). If \(b\) is the type’s balance at that moment and \(\rho\) is the selected price, then
\( \displaystyle \mu_t\min\{b,\rho\}=y_r>d_r. \)
Therefore both \(b\) and \(\rho\) exceed \(\theta=d_r/\mu_t\). At price \(\theta\), type \(t\) alone contributes \(d_r\) toward \(g\), so \(F_g(\theta)\geq d_r\geq c_g\). Continuity implies that \(g\) is affordable at a price at most \(\theta<\rho\), contradicting the selected project’s minimum price. This proves (2).
Since \(q=k\), the terminal aggregate balance consequently satisfies
\[ \displaystyle \mu_tb_t=\beta-\sum_{r=1}^ky_r\geq\beta-D_k. \tag{3} \]
Among the first \(k+1\) cheapest approvals, at least one is unselected. Therefore the cheapest unselected approval \(h_t\) has cost \(c_{h_t}\leq d_{k+1}\).
The completion assigns \(\mu_tb_t\) to this project. Subsequent completion only increases funded amounts, so
\( \displaystyle \sum_{j\in A_t}p_j \geq z+k+\frac{\mu_tb_t}{c_{h_t}} \geq z+k+\frac{\beta-D_k}{d_{k+1}} =z+k+\delta. \)
This proves Strong UFS for every type, including empty approval sets.
Round in funded-cost coordinates. Initially put \(v_j=c_jp_j\) for \(j\in C^+\). Projects in \(Z\) remain included deterministically.
While at least two coordinates satisfy \(0<v_j<c_j\), choose two such coordinates \(i,j\) and set
\( \displaystyle \alpha=\min\{c_i-v_i,v_j\}, \qquad \gamma=\min\{v_i,c_j-v_j\}. \)
Both numbers are positive. Make the update
\( \displaystyle (v_i,v_j)\leftarrow \begin{cases} (v_i+\alpha,v_j-\alpha),&\text{with probability }\gamma/(\alpha+\gamma),\\ (v_i-\gamma,v_j+\gamma),&\text{with probability }\alpha/(\alpha+\gamma). \end{cases} \)
Each update preserves the total funded cost, keeps every coordinate within its interval, and makes at least one coordinate integral, meaning either zero or its full cost.
It also preserves conditional expectations. For example,
\( \displaystyle \frac{\gamma(v_i+\alpha)+\alpha(v_i-\gamma)}{\alpha+\gamma}=v_i. \)
The same calculation applies to \(v_j\). Integral coordinates are never changed.
If one fractional coordinate \(h\) remains, set it to \(c_h\) with probability \(v_h/c_h\), and otherwise to zero. Output
\( \displaystyle W=Z\cup\{j\in C^+:v_j=c_j\}. \)
There are at most \(m\) updates. Preservation of conditional expectations gives
\( \displaystyle \Pr(j\in W)=p_j \)
for every positive-cost project; the equality also holds for zero-cost projects.
Since all projects in \(S\) begin integral, every output contains \(S\). Hence every support portfolio satisfies mass-scaled EJR.
To prove BB1, first suppose rounding finishes without a final fractional coordinate. Then \(c(W)=B\). Because \(B>0\), \(W\) contains a positive-cost project whose removal leaves cost at most \(B\).
Otherwise, immediately before the last rounding step, let \(W_0\) contain the fully funded projects together with \(Z\). Cost preservation gives
\( \displaystyle c(W_0)+v_h=B, \qquad 0<v_h<c_h. \)
If \(h\) is excluded, then \(c(W_0)<B<c(W_0\cup\{h\})\), supplying the first BB1 witness.
If \(h\) is included, then \(c(W_0\cup\{h\})>B\), and removing \(h\) leaves cost below \(B\), supplying the second witness.
Thus every support portfolio satisfies BB1.
It remains to justify polynomial bit lengths; a polynomial number of rational operations alone would not suffice.
Choose common denominators \(H,K\) such that
\( \displaystyle \mu_t=w_t/H,\qquad c_j=C_j/K,\qquad B=B_0/K, \)
where \(w_t,C_j,B_0\) are integers and \(\sum_tw_t=H\). Products of input denominators suffice, so these integers have bit lengths \(O(L)\).
Suppose all current balances have a common denominator \(D\), with \(K\mid D\). Initially \(D=K\).
For an affordable project \(j\), let \(R_j\) be its supporters with \(b_t<\rho_j\), and \(U_j\) its supporters with \(b_t\geq\rho_j\). At the smallest root, \(U_j\neq\emptyset\): otherwise the function would already have attained its final value at a smaller price.
Put \(s_j=\sum_{t\in U_j}w_t\), so \(1\leq s_j\leq H\). The affordability equation gives
\( \displaystyle \rho_j=\frac{Hc_j-\sum_{t\in R_j}w_tb_t}{s_j}. \)
Its numerator has denominator dividing \(D\), because \(K\mid D\). Thus \(\rho_j\) has denominator dividing \(Ds_j\).
When project \(j\) is selected, all updated balances can therefore be represented with common denominator \(D'=Ds_j\). After at most \(m\) selections,
\( \displaystyle D=K\prod_{\ell=1}^rs_\ell,\qquad r\leq m,\qquad \log D\leq\log K+m\log H. \)
Balances lie between zero and \(B\), so their numerators also have polynomial bit length. Unselected candidate prices have the same polynomial bound.
To find a project’s smallest affordable price, sort its supporters’ balances and scan the resulting linear pieces of \(F_j\). This takes \(O(\tau\log\tau)\) arithmetic operations per candidate. There are at most \(m\) candidates in each of at most \(m\) rounds. All comparisons and arithmetic involve polynomial-length integers.
Let \(D\) be the terminal common balance denominator and set \(E=HD\). Each aggregate residual amount \(\mu_tb_t\) has denominator dividing \(E\). Since \(K\mid E\), project costs and the budget also lie on this grid.
Both completion stages use sums, differences, and minima of numbers on this grid. Consequently every final funded amount has denominator dividing \(E\). Each marginal \(p_j=f_j/c_j\) has polynomial bit length.
The deterministic preprocessing and explicit output of \(p\) therefore take polynomial time.
During pair rounding, every funded coordinate stays on the same grid with denominator \(E\). Hence \(\alpha,\gamma\) and all branch probabilities have polynomial bit length. The final probability \(v_h/c_h\) does too.
An exact Bernoulli draw with rational probability \(a/d\) can be implemented using unbiased random bits: generate a uniform integer from the range of size \(2^{\lceil\log_2d\rceil}\), reject it if it is at least \(d\), and otherwise return success exactly when it is below \(a\). For \(d>1\), the acceptance probability exceeds one half. Thus the expected number of trials is less than two, with polynomial bit operations per trial. Deterministic probabilities are handled directly.
There are at most \(m\) such draws per sample. The sampler therefore has expected polynomial running time.
The compressed construction produces a rational \(p\in X(B)\) satisfying Strong UFS and an exact sampler with those marginals. Every support portfolio satisfies mass-scaled EJR and BB1. Both preprocessing and expected sampling time are polynomial in \(m,\tau,L\).
⟨structured verdict parsed — rendered above⟩
Verdict: proved with minor gaps. The construction is sound in substance and establishes polynomial preprocessing and exact sampling in expected polynomial time. I found two routine omissions, neither requiring new mathematics. No central assertion or computation is false.
The equivalence in Section 1 is correct.
This reduction preserves all required quantifiers. It does not entail enumerating subsets of types.
The compressed procedure is well-defined. For a positive-cost project, the stated affordability inequality is necessary and sufficient for the existence of a root of \(F_j\). Continuity and eventual saturation justify selecting its smallest root.
Balances remain nonnegative. The aggregate debit for each selected project equals its cost, so the accounting identity
\[
c(S^+)+\sum_t\mu_tb_t=B
\]
is correct.
The approval EJR guarantee invoked by the prover is supported by the cited paper. The source permits arbitrary positive project costs and arbitrary tie-breaking; its approval specialization provides the stated representation guarantee. Its formal framework also assumes that every project has at least one supporter. [Peters, Pierczyński, and Skowron, Definitions 1 and 3 and Theorem 2](https://arxiv.org/pdf/2008.13276).
The virtual-electorate scaling calculation is correct:
Using all copies of types in \(R\) gives electorate fraction \(\mu(R)\), as required.
Issue 1 — minor: an omitted source hypothesis. The assertion that the virtual instance satisfies the theorem’s hypotheses overlooks positive-cost projects approved by nobody. These are allowed by USER_TASK, whereas the cited framework excludes them.
For a concrete instance exhibiting the mismatch, take \(B=1\), two projects of cost \(1\), and one type of mass \(1\) approving only the first project. The second project violates the source’s supporter assumption. This is a failure of the applicability statement as written, not a counterexample to the construction.
Minimum clarification: explicitly justify the theorem transfer in the presence of unsupported projects, including the case where every approval set is empty.
The zero-cost extension is correct. Every member of \(R\) approves all zero-cost projects in the common set \(Q\), and all such projects are included deterministically. Adding their count to the positive-cost guarantee yields the required count for \(Q\).
The case \(Q^+=\emptyset\) is handled explicitly. EJR is preserved by taking supersets because every relevant approval count can only increase.
The completion argument is correct.
For an unselected positive-cost project, termination gives a strict inequality between its supporters’ remaining aggregate money and its cost. Types assigning residual money to that project are among its supporters, so its initial funded amount is strictly below its cost.
Selected projects remain fully funded. Residual money from types without an unselected positive approval is omitted, consistent with the stated bound \(\sum_j f_j\leq B\).
The final scan can reach expenditure \(B\) because total project capacity is at least \(B\). All updates respect individual capacities. Division occurs only by positive costs, while zero-cost marginals are defined separately.
Thus the constructed vector belongs to \(X(B)\) and gives marginal \(1\) to every project in \(S\).
The definition of \(k\) is valid, including \(k=0\) and \(s=0\). When \(k<s\), maximality gives \(0\leq\delta<1\).
The displayed upper-bound calculation is correct. For indices through \(k\), the coefficients \(d_r-d_{k+1}\) are nonpositive; for later indices they are nonnegative. The coordinate bounds therefore give exactly the stated inequality.
Every feasible allocation spends at most \(\beta\) on approved projects, so this establishes the required utility upper bound.
Issue 2 — minor: exact-expenditure feasibility is not justified explicitly. In the case \(k=s\), the sentence “any remaining budget can be spent elsewhere” needs justification under the equality constraint defining \(X(\beta)\). This includes an empty approval set. The input assumptions provide the necessary capacity, but the write-up does not explicitly establish that fact here.
Minimum clarification: justify that funding all approved projects can be extended to an allocation in \(X(\beta)\), without reducing their funded amounts.
For \(k<s\), the described approved allocation already spends exactly \(\beta\), so there is no analogous missing expenditure argument.
This omission concerns the claimed characterization of the optimum. The later Strong UFS argument only needs its upper bound.
Applying positive-cost EJR to the single full type and its first \(k\) cheapest approvals correctly yields \(q\geq k\). The \(k=0\) case is immediate, and \(k=s\) then forces all positive approvals to be selected.
The proof of \(y_r\leq d_r\) is correct.
Before the \(r\)-th approved selection, at least one of the first \(r\) cheapest approvals remains available. If \(y_r>d_r\), both the current balance and selected price exceed \(d_r/\mu_t\). At that price, the type alone can cover the remaining cheap project. Continuity then gives a strictly cheaper affordable candidate, contradicting price minimization.
The argument uses only \(\mu_t>0\), which is guaranteed.
When \(q=k<s\), summing the payment bounds correctly gives
\[
\mu_tb_t\geq\beta-D_k.
\]
At least one of the first \(k+1\) cheapest approvals is unselected, so the chosen cheapest unselected approval has cost at most \(d_{k+1}\). Its residual funding is counted separately from the selected approvals, and later completion cannot reduce it.
Both inequalities in the final utility bound have the correct direction. Empty approval sets have required utility zero. Subject to the routine theorem clarification above, Strong UFS follows.
The rounding argument is correct.
The process has a deterministic bound on its number of updates. Iterating conditional expectations therefore gives the claimed marginals after the final Bernoulli rounding.
Every output contains \(S\), so EJR survives.
The BB1 cases are exhaustive and valid:
These are support-wise guarantees, not merely guarantees in expectation.
The bit-complexity argument is correct.
Products of input denominators yield \(H\) and \(K\) with bit lengths \(O(L)\). At a smallest positive-cost root, at least one supporter has balance at least the root, so \(s_j\) is a positive integer at most \(H\). The root formula therefore increases the common balance denominator by at most a factor \(H\) per selected project.
Consequently,
\[
\log D\leq\log K+m\log H
\]
is polynomially bounded. Balance numerators are bounded using \(0\leq b_t\leq B\). Candidate roots are likewise bounded by the maximum supporter balance, and the stated denominator calculation controls their representation size.
Sorting balances and scanning linear pieces requires polynomially many operations on polynomial-length integers.
Completion and pair rounding preserve the grid with denominator \(E=HD\). Marginals and branch probabilities consequently have polynomial bit lengths.
The rational Bernoulli rejection sampler is exact. For \(d>1\), its acceptance probability exceeds one half, including when \(d\) is a power of two. Deterministic probabilities are handled separately. With at most \(m\) draws, expected bit-operation complexity is polynomial.
Only two expositional clarifications are needed:
No blocking mathematical issue remains.
⟨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.