← back to the atlas

d4-conf-atal-2021-0073 (d4-conf-atal-2021-0073)

Answer: \(\mathrm{NP}\)-complete for every fixed positional scoring rule satisfying the stated assumptions.

The anchor (named result in the paper)

Theorem 3 — class: hardness

PDF text-layer excerpt — equations and symbol order may be approximateFor every positional scoring rule r, Maxr{>} is NP-complete.

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

The continuous mirror question, as graded

Given a fixed positional scoring rule \(r\), candidates \(C\), a target \(c^\star\), a tie-breaking order \(\tau\), an integer \(k\), and a finite support of partial-order types \(P\) with positive binary-rational masses \(\mu_P\) summing to \(1\), does there exist a completion plan \(x_{P,\pi}\geq 0\), indexed by linear extensions \(\pi\in\mathrm{LE}(P)\), such that \(\sum_{\pi\in\mathrm{LE}(P)}x_{P,\pi}=\mu_P\) for each \(P\) and \(\mathrm{rank}_x(c^\star)>k\)? Here \(S_x(c)=\sum_{P,\pi}x_{P,\pi}r(|C|,\mathrm{pos}_\pi(c))\), and rank is determined by these scores with ties resolved by \(\tau\).

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

Fix a positional scoring rule \(r\): its scores are nonnegative integers, nonincreasing in position, with \(r(m,1)>r(m,m)\) and greatest common divisor one; \(r(m,j)\) is computable in polynomial time in \(m\).
An instance has candidates \(C\), with \(m=|C|\geq2\), a target \(c^\star\in C\), a tie-breaking linear order \(\sigma\), and an input integer \(1\leq k\leq m\).
A society is given by its support: the list of the \(\tau\) partial-order types \(P\) on \(C\) with positive binary-rational masses \(\mu_P\), summing to \(1\). Here \(\tau\) is the support size, not the number of possible types. Each partial order is encoded explicitly by its relation; \(L\) is the total input bit length.
Write \(\mathrm{LE}(P)\) for the strict linear orders extending \(P\). A completion plan assigns real masses \(x_{P,\pi}\geq0\), for \(\pi\in\mathrm{LE}(P)\), satisfying \(\sum_{\pi\in\mathrm{LE}(P)}x_{P,\pi}=\mu_P\).
Define \(S_x(c)=\sum_P\sum_{\pi\in\mathrm{LE}(P)}x_{P,\pi}r(m,\mathrm{pos}_\pi(c))\), where positions start at \(1\). Rank candidates by decreasing score, resolving equal scores by \(\sigma\); ranks start at \(1\).
The decision problem asks whether some completion plan satisfies \(\mathrm{rank}_x(c^\star)>k\). State running times in \(m,\tau,L,k\).

For each fixed rule \(r\) satisfying these assumptions, is this continuous decision problem in P or NP-hard?

For discrete voters, the corresponding decision problem is NP-complete for every such rule and W[1]-hard parameterized by \(k\); for fixed \(k\), it is polynomial-time solvable when scores are polynomially bounded in \(m\). [Source](https://www.ifaamas.org/Proceedings/aamas2021/pdfs/p638.pdf)
No result settling exactly this continuous decision problem was identified in the literature search.

Modeling choices made when packaging the task

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

Classification

For every fixed scoring rule \(r\) satisfying the assumptions, the continuous decision problem is \(\mathrm{NP}\)-complete.

Moreover, it is \(\mathrm{W}[1]\)-hard parameterized by \(k\), and admits a deterministic algorithm with running time
\(\displaystyle \binom{m-1}{k}\operatorname{poly}(\tau m^{k+1},m,L,k)\).
Consequently, for every fixed \(k\), it is polynomial-time solvable without requiring polynomially bounded scores.

The case \(k=m\) always has answer no. Below, assume \(1\leq k<m\).

Write \(s_j=r(m,j)\), and let \(b(m)=\lceil\log_2(s_1+1)\rceil\). Polynomial-time computability of the scores implies that \(b(m)\) is polynomially bounded in \(m\). Their numerical values need not be.

1. A score-calibration construction

We first prove a construction used in the hardness reduction.

Fix \(m\), a distinguished candidate \(c^\star\), and an index \(p\) with \(s_p>s_{p+1}\). Such an index exists because \(s_1>s_m\). Put \(\Delta=s_p-s_{p+1}>0\) and \(R=\sum_{j=1}^m s_j\).

Calibration claim. Given integers \(h_a\), one for each candidate, with \(\sum_a h_a=0\), we can construct a collection of complete orders with positive integer weights whose score contribution to candidate \(a\) is
\(K+\Delta h_a\), where \(K\) is common to all candidates. The collection uses at most \(2m(m-1)\) orders before duplicate orders are combined.

To prove this, for each \(a\neq c^\star\), choose an order \(\pi_a^+\) placing \(a,c^\star\) at positions \(p,p+1\). Let \(\pi_a^-\) swap those two candidates and leave all other positions unchanged. Their score vectors differ by \(\Delta\) at \(a\), by \(-\Delta\) at \(c^\star\), and by zero elsewhere.

For any order \(\pi\), its \(m\) cyclic rotations place each candidate once at every position. Giving every rotation weight \(B\) therefore contributes score \(BR\) to every candidate.

Set \(B=1+\max_{a\neq c^\star}|h_a|\). For each \(a\neq c^\star\), include the cyclic rotations of both \(\pi_a^+\) and \(\pi_a^-\), initially each with weight \(B\). Change the weight of the unrotated \(\pi_a^+\) to \(B+h_a\), and that of the unrotated \(\pi_a^-\) to \(B-h_a\). All weights remain positive, and these changes preserve total weight.

Before the changes, every candidate receives \(K=2(m-1)BR\). The changes add \(\Delta h_a\) to each \(a\neq c^\star\), and add
\(-\Delta\sum_{a\neq c^\star}h_a=\Delta h_{c^\star}\)
to \(c^\star\). This proves the claim.

The total weight of this collection is \(2m(m-1)B\). Duplicate complete orders can be combined by adding their weights.

2. Hardness under arbitrary real splitting

We reduce from Independent Set: given a simple undirected graph \(G=(V,E)\), with \(n=|V|\), and \(1\leq q\leq n\), decide whether it has an independent set of size at least \(q\).

The graph gadget uses the saturation principle underlying the discrete reduction in Theorem 3.2 of [Imber and Kimelfeld](https://www.ifaamas.org/Proceedings/aamas2021/pdfs/p638.pdf). The following construction proves its soundness for real-valued splitting and supplies an explicit calibration with polynomial bit length.

2.1 Candidates and edge types

Choose \(m\) to be the smallest power of two satisfying \(m\geq n+2\). Thus \(m<2(n+2)\). Use candidates
\(C=V\cup\{c^\star\}\cup F\), where \(F\) is a set of dummy candidates.

Evaluate the scoring vector at this \(m\), choose a strict drop \(p\), and define \(\Delta=s_p-s_{p+1}>0\).

For each edge \(e=\{u,v\}\), construct a partial order \(P_e\) as follows:

Explicitly, the first \(p-1\) fixed candidates precede both endpoints, and both endpoints precede the remaining fixed candidates. This poset has exactly two linear extensions, corresponding to the two orders of \(u,v\).

Temporarily give every edge type weight one. For a fractional completion, let \(z_{e,u}\) be the fraction putting \(u\) at position \(p\). Then
\(0\leq z_{e,u}\leq1\) and \(z_{e,u}+z_{e,v}=1\).

Let \(A_x(a)\) denote candidate \(a\)'s aggregate contribution from these unit-weight edge types. For each vertex candidate \(u\), let \(M_u\) be its individual maximum contribution. It is computable directly: on every incident edge use \(s_p\), and on every nonincident edge use its fixed-position score. Therefore

\(\displaystyle A_x(u)=M_u-\Delta\sum_{e\ni u}(1-z_{e,u}).\)

The target and dummy candidates have fixed contributions; denote them by \(A_{c^\star}\) and \(A_d\), respectively.

Define integer quantities

\(\displaystyle t_u=M_u\quad(u\in V),\qquad t_{c^\star}=A_{c^\star},\qquad t_d=A_d+1\quad(d\in F).\)

Put \(Q=\sum_{a\in C}t_a\) and \(H=Q/m\).

2.2 Calibrating the thresholds

Now give every edge type the integer weight \(W=m\Delta\).

For each candidate, define \(h_a=Q-mt_a\). These are integers and satisfy
\(\sum_a h_a=mQ-m\sum_a t_a=0\).

Apply the calibration construction from Section 1. Its complete orders contribute

\(\displaystyle K+\Delta h_a=K+W(H-t_a)\)

to candidate \(a\).

After adding the weighted edge types, the unnormalized scores are consequently

\(\displaystyle T_x(c^\star)=K+WH,\)

\(\displaystyle T_x(u)=K+WH-W\Delta\sum_{e\ni u}(1-z_{e,u})\quad(u\in V),\)

and

\(\displaystyle T_x(d)=K+WH-W\quad(d\in F).\)

Thus every vertex's score is at most the target's score, with equality precisely when all its incident edges put their entire mass on that vertex at position \(p\). Every dummy is strictly below the target.

2.3 Normalizing to positive dyadic masses

We ensure that the construction works even if “binary-rational” means dyadic.

Let \(B\) be the positive integer used in the calibration construction. The total unnormalized weight is

\(\displaystyle N=W|E|+2m(m-1)B.\)

This is a positive multiple of \(m\). Let \(Z\) be the smallest power of two with \(Z\geq N\). Since \(m\) is a power of two and \(N\geq m\), \(Z\) is also divisible by \(m\). Hence \(g=(Z-N)/m\) is a nonnegative integer.

If \(g>0\), add all \(m\) cyclic rotations of any complete order, each with weight \(g\). They add total weight \(Z-N\) and add the same score \(gR\) to every candidate. Finally, divide every weight by \(Z\).

All resulting masses are positive dyadic rationals and sum to one. Combine duplicate types by adding their masses. Normalization and the added common score preserve every score comparison above.

Choose \(\sigma\) to put all vertex candidates before \(c^\star\), and all dummies after it. Set the output parameter \(k=q\).

2.4 Correctness for real-valued completion plans

For any completion plan \(x\), define

\(\displaystyle I_x=\{u\in V:z_{e,u}=1\text{ for every edge }e\ni u\}.\)

Because every summand \(1-z_{e,u}\) is nonnegative, the score formulas show that a vertex ties the target exactly when it belongs to \(I_x\). All such ties favor the vertex; every other vertex and every dummy is below the target. Therefore

\(\displaystyle \operatorname{rank}_x(c^\star)=1+|I_x|.\)

Furthermore, \(I_x\) is independent. Indeed, if adjacent vertices \(u,v\) both belonged to \(I_x\), their common edge would satisfy \(z_{e,u}=z_{e,v}=1\), contradicting \(z_{e,u}+z_{e,v}=1\). This argument applies to arbitrary real fractions.

Conversely, let \(I\subseteq V\) be independent. For every edge incident to a vertex of \(I\), put its entire mass on the extension placing that vertex at position \(p\). These choices are consistent because an edge has at most one endpoint in \(I\). Complete all other edge types arbitrarily. Every vertex in \(I\) then ties and outranks the target.

Consequently,

\(\displaystyle \exists x:\operatorname{rank}_x(c^\star)>q \quad\Longleftrightarrow\quad G\text{ has an independent set of size at least }q.\)

In fact, the maximum achievable rank in the constructed instance is \(1+\alpha(G)\), where \(\alpha(G)\) is its independence number.

2.5 Size and running time of the reduction

Each \(t_a\) lies between zero and \(|E|s_1+1\). Hence
\(|h_a|\leq m(|E|s_1+1)\), and \(B\), \(W\), \(N\), and \(Z\) all have \(O(b(m)+\log m)\) bits, using \(|E|\leq m^2\).

The support size satisfies

\(\displaystyle \tau\leq |E|+2m(m-1)+m=O(m^2).\)

Every supported poset has at most two linear extensions. Its explicit relation uses polynomial space in \(m\), so the total output length \(L\) is polynomial in \(m\) for fixed \(r\). Scores, weights, and relations can all be constructed in polynomial time in the graph input length.

This proves \(\mathrm{NP}\)-hardness for every allowed rule. It uses no assumption of purity or polynomially bounded numerical scores.

The reduction preserves \(k=q\). Together with the standard \(\mathrm{W}[1]\)-hardness of Independent Set parameterized by its requested size, it also proves \(\mathrm{W}[1]\)-hardness parameterized by \(k\).

3. Membership in \(\mathrm{NP}\)

The availability of real masses requires a rational-witness argument.

Fix a set \(A\subseteq C\setminus\{c^\star\}\) of size \(k\). We test whether every candidate in \(A\) can outrank the target simultaneously.

Use all completion variables \(x_{P,\pi}\), and introduce \(0\leq\varepsilon\leq1\). Impose the type-mass equalities and, for every \(a\in A\), impose

\(\displaystyle S_x(a)-S_x(c^\star)\geq0\)

if \(\sigma\) puts \(a\) before \(c^\star\), and

\(\displaystyle S_x(a)-S_x(c^\star)\geq\varepsilon\)

otherwise. Maximize \(\varepsilon\).

These constraints describe a finite rational linear program. Its feasible region is compact: the completion variables belong to a product of finite simplexes, and \(\varepsilon\in[0,1]\).

There is a plan making every member of \(A\) outrank the target exactly when this program has an optimum with \(\varepsilon>0\). For the forward implication, choose the minimum of one and the finitely many required positive score differences. If there are no strict comparisons, choose \(\varepsilon=1\). The reverse implication follows directly from the inequalities and tie-breaking order.

Introduce one nonnegative slack variable for each of the \(k\) score inequalities and one for \(\varepsilon\leq1\). The resulting standard-form program has at most

\(\displaystyle d=\tau+k+1\)

equality rows. A basic optimal solution therefore has at most \(d\) nonzero variables, including completion variables and auxiliary variables.

After clearing the denominators in the mass equations, every coefficient and right-hand side has \(O(L+b(m))\) bits. Cramer's rule and the determinant bound for a \(d\)-dimensional basis imply that every basic coordinate has

\(\displaystyle O\!\left(d\bigl(L+b(m)+\log d\bigr)\right)\)

bits. Thus every yes-instance has a rational completion witness supported on at most \(\tau+k+1\) type-extension pairs, with polynomial total bit length.

A certificate lists \(A\), those linear orders, and their rational masses. The verifier checks extension validity, type totals, and score comparisons using exact rational arithmetic. Its running time is \(\operatorname{poly}(m,\tau,L,k)\) for fixed \(r\).

This proves membership in \(\mathrm{NP}\), completing the \(\mathrm{NP}\)-completeness proof.

4. A fixed-\(k\) algorithm

We give the claimed running-time bound explicitly.

4.1 Testing specified positions

Lemma. Given a poset on \(m\) candidates and prescribed distinct positions for some candidates, existence of a linear extension realizing those positions is decidable in \(O(m^3)\) time.

For each candidate \(v\), start with an allowed position interval \([a_v^0,b_v^0]\). It is the prescribed singleton for a marked candidate and \([1,m]\) otherwise.

Process the poset in topological order to obtain

\(\displaystyle a_v=\max\bigl(\{a_v^0\}\cup\{a_u+1:u\prec_P v\}\bigr).\)

Process it in reverse topological order to obtain

\(\displaystyle b_v=\min\bigl(\{b_v^0\}\cup\{b_w-1:v\prec_P w\}\bigr).\)

Every valid extension respects these propagated intervals, by induction along the respective processing orders.

Form a bipartite graph joining candidate \(v\) to every integer position in \([a_v,b_v]\). Reject if it has no perfect matching.

To prove sufficiency, choose topological labels \(h_v\) that strictly increase along the poset. Among all perfect matchings, choose a position assignment \(f\) maximizing \(\sum_v h_vf(v)\); a maximizer exists because there are finitely many matchings.

Suppose \(u\prec_P v\) but \(f(u)>f(v)\). Propagation gives

\(\displaystyle a_u<a_v\leq f(v)<f(u)\leq b_u<b_v.\)

Therefore swapping \(f(u)\) and \(f(v)\) keeps both positions inside their respective allowed intervals. The swap increases the objective by
\((h_v-h_u)(f(u)-f(v))>0\), contradicting maximality. Hence the maximizing assignment respects every precedence relation and is the required extension.

Propagation takes \(O(m^2)\) time on an explicit relation. A perfect matching can be tested by the elementary augmenting-path algorithm in \(O(m^3)\) time. This proves the lemma.

4.2 Projecting onto the relevant candidates

Enumerate every set \(A\) of \(k\) challengers. For a fixed \(A\), mark the \(k+1\) candidates in \(A\cup\{c^\star\}\).

For each supported type \(P\), enumerate their injective position tuples. There are at most \(m^{k+1}\). Apply the lemma to each tuple and retain the feasible ones. Each retained tuple determines a score vector for these \(k+1\) candidates.

Introduce a nonnegative mass variable for each retained type-tuple pair, summing to \(\mu_P\) within each type. Use their score vectors in the margin linear program from Section 3.

This projection is exact:

Thus the linear program answers whether the chosen \(k\) challengers can simultaneously outrank the target.

For each \(A\), tuple enumeration and feasibility testing take
\(O(\tau m^{k+4})\) time. The linear program has at most \(\tau m^{k+1}+1\) variables, polynomially many encoded coefficients, and coefficient bit lengths bounded by \(O(L+b(m))\).

The overall deterministic running time is therefore

\(\displaystyle \binom{m-1}{k}\operatorname{poly}(\tau m^{k+1},m,L,k) = m^{O(k)}\operatorname{poly}(\tau,L)\)

for fixed \(r\). This proves polynomial-time solvability for each fixed \(k\), even when the scores are numerically exponential or larger.

⟨structured verdict parsed — rendered above⟩

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

Verification report

Verdict: proved. The output establishes \(\mathrm{NP}\)-completeness for every fixed rule in the task, including when completion masses may be arbitrary real numbers. Its additional parameterized hardness and fixed-\(k\) algorithm claims are also justified. I found no major or minor issues requiring repair.

1. Scope and assumptions

The proof addresses the support representation specified in USER_TASK: masses are encoded compactly, rather than expanded into discrete voters.

The preliminary observations are correct:

The proof does not use the greatest-common-divisor assumption. This is harmless: its argument applies to a broader class containing every allowed rule.

2. Calibration construction

The calibration claim is valid.

For each \(a\ne c^\star\), swapping positions \(p,p+1\) changes only the scores of \(a\) and \(c^\star\), by \(\Delta\) and \(-\Delta\), respectively.

Each family of \(m\) cyclic rotations contributes \(BR\) to every candidate. Consequently, the stated baseline
\[ K=2(m-1)BR \]
is correct.

The weight changes contribute \(\Delta h_a\) to each non-target candidate. The target’s change is
\[ -\Delta\sum_{a\ne c^\star}h_a=\Delta h_{c^\star}, \]
using the stated zero-sum hypothesis.

Since \(B>|h_a|\), all modified weights remain positive. Each pair of modifications has total change zero, so the claimed total weight is also correct. Combining duplicate orders preserves contributions and total weight.

3. Hardness reduction

Edge types and score formulas

Each edge poset has exactly two linear extensions: every position except the adjacent endpoint pair is fixed.

The fractions satisfy \(z_{e,u}+z_{e,v}=1\), and the vertex score formula
\[ A_x(u)=M_u-\Delta\sum_{e\ni u}(1-z_{e,u}) \]
correctly accounts for the loss from the individual maximum on every incident edge. Nonincident contributions are fixed.

The chosen candidate count satisfies \(m<2(n+2)\), and \(q\le n<m\), so the output parameter is valid.

Threshold calibration

The integers \(h_a=Q-mt_a\) satisfy the calibration claim’s zero-sum condition. The identity
\[ \Delta h_a=W(H-t_a) \]
holds because \(W=m\Delta\) and \(H=Q/m\). No integrality assumption on \(H\) is needed.

Substituting the definitions of \(t_a\) gives exactly the three stated score formulas. Thus vertices cannot score above the target, and dummies are strictly below it.

Dyadic normalization

The normalization is correct, including under the stricter interpretation that binary-rational masses must be dyadic.

The total weight \(N\) is a positive multiple of \(m\). Since \(m\) is a power of two and \(Z\ge N\ge m\), \(Z\) is divisible by \(m\). Therefore \(g=(Z-N)/m\) is a nonnegative integer.

When padding is needed, its cyclic rotations add the same score to every candidate. Dividing by \(Z\) preserves all comparisons and produces positive dyadic masses summing to one. Duplicate-type aggregation preserves these properties.

Correctness under real splitting

This is the central step, and it is sound.

Every loss term \(1-z_{e,u}\) is nonnegative. Hence a vertex ties the target exactly when every incident fraction equals one. The selected tie-breaking order then gives
\[ \operatorname{rank}_x(c^\star)=1+|I_x|. \]

Adjacent vertices cannot both satisfy this saturation condition: their common edge would require both endpoint fractions to equal one despite their sum being one. Thus \(I_x\) is independent even for arbitrary real completion masses.

Conversely, an independent set permits all its incident edges to be assigned entirely toward its vertices without conflicting choices. Its vertices then tie and outrank the target.

The equivalence uses the correct threshold: rank greater than \(q\) means at least \(q\) candidates outrank the target. Isolated vertices are correctly included through the vacuous saturation condition; edgeless graphs also cause no failure.

The attribution to the saturation idea in Theorem 3.2 is consistent with the [cited paper](https://www.ifaamas.org/Proceedings/aamas2021/pdfs/p638.pdf). The continuous reduction is nevertheless established by the output’s own argument.

Reduction size and parameter preservation

The numerical and support bounds check out.

The bounds on \(t_a\) imply the stated bound on \(|h_a|\). Using \(|E|\le m^2\), the weights and normalization denominator have \(O(b(m)+\log m)\) bits. The support has \(O(m^2)\) types, each with a polynomial-size explicit relation.

Thus the reduction has polynomial output length and running time for every fixed allowed rule. It preserves \(k=q\), so the stated application of parameterized Independent Set hardness is valid.

4. Membership in \(\mathrm{NP}\)

The margin linear program correctly distinguishes weak comparisons, where tie-breaking favors the challenger, from strict comparisons.

For any successful plan, finitely many required strict margins have a positive minimum. Capping this minimum at one supplies a valid positive \(\varepsilon\). If no strict comparisons are required, \(\varepsilon=1\) works. Conversely, positive \(\varepsilon\) guarantees all required strict comparisons.

The feasible region is finite-dimensional and compact. Consequently, whenever it has a positive optimum, an optimal basic solution exists after standard-form conversion.

There are at most \(\tau+k+1\) equality rows. The basic-solution support bound therefore applies; dependent rows can only decrease the bound. Clearing mass denominators gives polynomial-bit coefficients, and the stated determinant estimate yields polynomial-bit basic coordinates despite the potentially exponential number of columns.

The resulting certificate lists only polynomially many extensions and rational masses. Extension validity, type totals, and score comparisons can all be checked exactly in polynomial time. This establishes \(\mathrm{NP}\) membership for real completion plans.

5. Fixed-\(k\) algorithm

Prescribed-position lemma

Both directions of the lemma are justified.

Propagation gives necessary position intervals. Along every precedence relation \(u\prec_P v\), it also gives \(a_u<a_v\) and \(b_u<b_v\).

For an inverted matched pair, the displayed inequality chain ensures that exchanging its assigned positions preserves both allowed intervals. The objective increases by the stated positive quantity because the topological labels increase along precedence relations. Thus an objective-maximizing perfect matching respects the poset.

The maximization is used only to establish existence; the decision algorithm needs only a perfect-matching test. Its \(O(m^3)\) bound is valid.

Projection and running time

Feasible position tuples capture exactly the score vectors needed for the chosen challengers and target. Aggregating extension masses produces a projected solution, and selecting one extension per feasible tuple lifts any projected solution back to a completion plan.

There are at most \(m^{k+1}\) tuples per type. Combining this count with the lemma gives the stated \(O(\tau m^{k+4})\) enumeration time.

The projected program has polynomial encoding length in the stated parameters. Rational linear programming therefore supports the overall bound
\[ \binom{m-1}{k}\operatorname{poly}(\tau m^{k+1},m,L,k) = m^{O(k)}\operatorname{poly}(\tau,L) \]
for fixed \(r\). Polynomial score bit length suffices; polynomial numerical score bounds are unnecessary.

6. Required feedback

No repair or additional clarification is necessary. The universal hardness claim, rational-witness argument, and fixed-\(k\) algorithm all survive verification.

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