Answer: —
Theorem 4.1 — class: other
Given a finite downward-closed family \(\mathcal B\) of integral bundle patterns, type masses \(\mu\), per-capita supplies \(q\), and valuations \(v_t\), define \(M_t=\max\{\lambda:\exists z_b\ge0,\ \sum_b z_b=1,\ \sum_b b_jz_b\le q_j,\ z_b>0\Rightarrow v_t(b)\ge\lambda\}\). Run the paper's increasing-cardinality minimum-bundle greedy rule on mass, allowing legal tie-breaking, and determine the largest \(\alpha\) guaranteed to exhaust all type mass using bundles with \(v_t(b)\ge\alpha M_t\).
Let \(m\ge1\) be the number of goods categories and let \(\mathcal B\subseteq\mathbb Z_{\ge0}^m\) be an explicitly listed, nonempty, finite downward-closed family of feasible bundle patterns. Supplies \(q_j\) and item values \(w_{t,j}\) are nonnegative binary rationals; on feasible patterns, \(v_t(b)=\sum_j w_{t,j}b_j\).
A society is given by its support: the list of the \(\tau\) types with positive mass, each with its mass as a binary rational. Here \(\sum_t\mu_t=1\), and \(\tau\) is the support size, not the number of possible types. State any running times in \(m,\tau,L,|\mathcal B|\), where \(L\) is the total input bit length, and any additional parameters.
For each type, define \(M_t=\max\{\lambda\ge0:\exists(z_b)_{b\in\mathcal B}\ge0,\ \sum_bz_b=1,\ \sum_bb_jz_b\le q_j\ \forall j,\ z_b>0\Rightarrow v_t(b)\ge\lambda\}\). These benchmarks remain fixed throughout allocation; types with \(M_t=0\) receive the empty pattern.
For a threshold \(\alpha\in(0,1]\), initialize remaining type masses \(a_t=\mu_t\) for positive-benchmark types and remaining supplies \(r=q\). A pair \((t,b)\) is eligible when \(a_t>0\), \(b\in\mathcal B\), \(v_t(b)\ge\alpha M_t\), and \(r_j>0\) whenever \(b_j>0\).
Repeatedly choose any eligible pair minimizing \(|b|=\sum_jb_j\), allocate pattern \(b\) to mass \(d=\min\{a_t,\min_{j:b_j>0}r_j/b_j\}\), and update \(a_t\leftarrow a_t-d\), \(r\leftarrow r-db\). Stop when no pair is eligible; unused supply is permitted. Every such choice among minimum-cardinality pairs is legal tie-breaking.
What is the supremum \(\alpha_*\in[0,1]\) of thresholds for which this mass greedy rule exhausts every type's mass on every admissible instance under every legal tie-breaking, and is the supremum itself guaranteed?
For finite agents with hereditary valuations and the usual MMS benchmark, minimum-cardinality greedy guarantees \(4/11\), while its universal guarantee is at most \(40/107\), even for identical agents and partition matroids. [Li–Vetta](https://arxiv.org/pdf/1812.09561v2)
A different discrete procedure establishes existence of \(1/2\)-MMS allocations for hereditary valuations; this does not settle the specified greedy rule. [Hummel](https://arxiv.org/abs/2404.11582)
No result settling the precise mass greedy guarantee above was located in the literature search.
The exact supremum remains undetermined. I prove the sharper bounds
$$
\frac{4}{11}\leq \alpha_*\leq C_\infty,
\qquad
C_\infty=
\left(1+\sum_{i=1}^{\infty}\frac{1}{k_i-1}\right)^{-1},
$$
where
$$
k_1=2,\qquad k_{i+1}=k_i(k_i-1)+1.
$$
Numerically,
$$
C_\infty\approx 0.3716048959573.
$$
This improves the upper bound $40/107$ in the notes. I also prove that the actual supremum $\alpha_*$ is guaranteed, without assuming monotonicity of the universal guarantee in the threshold.
The upper-bound construction uses one type, integer supplies, and a single deterministic pattern witnessing its benchmark.
Write $K=|\mathcal B|$. Nonemptiness and downward closure imply $0\in\mathcal B$.
For a type $t$ and a candidate value $\lambda$, let
$$
\mathcal B_t(\lambda)=\{b\in\mathcal B:v_t(b)\geq\lambda\}.
$$
The candidate is feasible in the benchmark definition exactly when
$$
z_b\geq0,\qquad
\sum_{b\in\mathcal B_t(\lambda)}z_b=1,\qquad
\sum_{b\in\mathcal B_t(\lambda)}b_jz_b\leq q_j
\quad\text{for all }j
$$
is feasible.
Every distribution on the finite family has nonempty support, whose minimum value is one of the finitely many values $v_t(b)$. Consequently, $M_t$ is the largest feasible member of
$$
\{v_t(b):b\in\mathcal B\}.
$$
The value $0$ is feasible, using the empty pattern. Thus $M_t$ exists, is attained, and is rational.
The feasible region at $M_t$ is a nonempty rational polytope contained in a simplex. It has a vertex, and the linear equations defining a vertex have rational coefficients; solving an independent defining subsystem gives rational coordinates. Hence a rational benchmark witness $z^t$ exists.
Now fix any positive threshold, possibly irrational. Every selected pattern is nonempty, because its recipient has positive benchmark. Eligibility makes every supply ratio in the definition of $d$ positive, so $d>0$. Each step exhausts either a remaining type mass or a previously positive category supply. Such quantities never become positive again. Therefore every execution has at most
$$
m+\tau
$$
steps.
All states and allocated masses are rational: their updates use subtraction, multiplication by integer coordinates, and division by positive integer coordinates. The threshold affects the choices, but does not enter these arithmetic updates.
I use the finite-agent theorem stated in the task: for a common hereditary feasible-set family, nonnegative item weights, and valuations extended by maximizing over feasible subsets, minimum-cardinality greedy with fixed targets $(4/11)\operatorname{MMS}(i)$ serves every agent under every legal tie-breaking. This is the guarantee of [Li–Vetta, Theorem 3.1](https://arxiv.org/html/1812.09561v2).
Here is the reduction checking its applicability.
Fix a mass instance and one execution at threshold $4/11$. Choose a positive integer $N$ clearing the denominators of:
There are finitely many such rationals by Section 1.
Construct $N$ finite agents, with $N\mu_t$ agents of type $t$, and $Nq_j$ distinct items of category $j$. A finite item set is feasible when its category-count vector belongs to $\mathcal B$. This family is hereditary because taking a subset decreases that vector coordinatewise.
A type-$t$ agent gives each category-$j$ item weight $w_{t,j}$. On arbitrary sets, extend the valuation by maximizing the weight of a feasible subset.
For a positive-benchmark type, take $Nz_b^t$ copies of each pattern $b$ in its benchmark witness. These give $N$ feasible bundles, each worth at least $M_t$, consuming at most $Nq$. They can be realized with distinct items. Distribute unused items arbitrarily among the bundles; the extended valuations cannot decrease. Therefore
$$
\operatorname{MMS}_N(t)\geq M_t.
$$
Conversely, suppose a partition into $N$ parts gives type $t$ value at least $\lambda$ in every part. Choose a maximizing feasible subset of each part. The uniform distribution on their patterns has expected consumption at most $q$, and every support pattern is worth at least $\lambda$. Thus $\lambda\leq M_t$, proving
$$
\operatorname{MMS}_N(t)=M_t.
$$
The reverse argument also proves this equality for zero-benchmark types, since their finite MMS cannot be positive.
Replace a mass allocation of pattern $b$ to mass $d$ of type $t$ by $Nd$ consecutive allocations of that pattern to finite agents of type $t$.
At the start of the batch,
$$
Nd\leq Na_t,\qquad Ndb_j\leq Nr_j.
$$
After $\ell<Nd$ allocations, at least $Nd-\ell$ intended recipients remain, and the remaining category-$j$ item count is at least
$$
(Nd-\ell)b_j.
$$
Thus every allocation in the batch is physically possible.
At the beginning of the batch, a qualifying finite bundle of smaller cardinality would induce a smaller eligible mass pattern. Its recipient type still has positive remaining mass, and every category it uses has positive remaining supply. This contradicts the selected mass pair’s minimum cardinality.
Removing items and agents cannot create a smaller qualifying bundle during the batch. Hence all allocations in the batch are legal finite greedy choices.
At the end of all batches, finite residual supplies and agent counts are $N$ times the mass residuals. If the mass execution has stopped, any qualifying finite bundle would induce an eligible mass pair, a contradiction. Zero-benchmark agents receive empty bundles.
A failing mass execution would therefore give a failing finite execution, contrary to the cited theorem. Consequently,
$$
\frac{4}{11}\in G,
\qquad
\alpha_*\geq\frac{4}{11},
$$
where $G$ denotes the universally guaranteed thresholds. The replication is a proof device, not an algorithmic expansion of the input.
Define
$$
T_n=1+\sum_{i=1}^{n}\frac{1}{k_i-1},
\qquad
c_n=\frac{1}{T_n}.
$$
The first terms of the integer sequence are
$$
2,\ 3,\ 7,\ 43,\ 1807,\ 3263443.
$$
I construct an admissible rational instance failing at every threshold in
$$
\left(c_n,\ c_n\frac{k_n}{k_n-1}\right]\cap(0,1].
$$
These intervals together cover every threshold above $C_\infty$.
The recurrence gives
$$
k_{i+1}-1=k_i(k_i-1),
$$
and hence
$$
\frac{1}{k_i-1}-\frac{1}{k_{i+1}-1}
=\frac{1}{k_i}.
$$
Summing and using $k_1-1=1$ yields
$$
S_n:=\sum_{i=1}^{n}\frac{1}{k_i}
=1-\frac{1}{k_{n+1}-1}<1.
$$
Also,
$$
\frac{1/(k_{i+1}-1)}{1/(k_i-1)}=\frac{1}{k_i}\leq\frac12.
$$
Thus the series defining $C_\infty$ converges, and $c_n$ decreases strictly to $C_\infty$.
Fix $n\geq1$, and put $h=k_n-1$. Use one type of mass $1$, with categories
$$
A_1,\ldots,A_n,F.
$$
Set the supplies to
$$
q_{A_i}=1,\qquad q_F=h.
$$
The feasible family is
$$
\mathcal B=
\left\{
b\in\mathbb Z_{\geq0}^{n+1}:
b_{A_i}\leq k_i\text{ for every }i,\quad b_F\leq h
\right\}.
$$
The input lists every vector in this rectangle. Its size is
$$
K_n=(h+1)\prod_{i=1}^{n}(k_i+1).
$$
Thus the construction uses an explicitly listed finite downward-closed family, although its list can be large.
Give the type weights
$$
w_{A_i}=\frac{c_n}{k_i-1},
\qquad
w_F=\frac{c_n}{h}.
$$
All input data are nonnegative rationals.
The pattern
$$
p=(1,\ldots,1,h)
$$
is feasible and consumes exactly $q$. Its value is
$$
v(p)
=c_n\left(\sum_{i=1}^{n}\frac{1}{k_i-1}+1\right)
=c_nT_n=1.
$$
The deterministic distribution on $p$ proves $M\geq1$.
On the other hand, $w\cdot q=1$. Any benchmark-feasible distribution supported on patterns worth at least $\lambda$ satisfies
$$
\lambda
\leq \mathbb E[v(b)]
=w\cdot\mathbb E[b]
\leq w\cdot q
=1.
$$
The last inequality uses nonnegative weights. Hence
$$
M=1.
$$
Suppose
$$
c_n<\alpha\leq c_n\frac{k_n}{k_n-1}.
$$
Choose successively the patterns
$$
k_1A_1,\ k_2A_2,\ \ldots,\ k_nA_n.
$$
Before step $i$, exactly the categories $A_i,\ldots,A_n,F$ have positive supply. Their weights satisfy
$$
w_{A_i}\geq w_{A_{i+1}}\geq\cdots\geq w_{A_n}=w_F.
$$
Therefore every available pattern of cardinality at most $k_i-1$ has value at most
$$
(k_i-1)w_{A_i}=c_n<\alpha.
$$
Meanwhile, the proposed pattern qualifies because
$$
v(k_iA_i)
=c_n\frac{k_i}{k_i-1}
\geq c_n\frac{k_n}{k_n-1}
\geq\alpha.
$$
Here $k_i\leq k_n$, and $x/(x-1)$ decreases for $x>1$. Thus each proposed choice has minimum eligible cardinality.
The mass allocated at step $i$ is exactly $1/k_i$. Indeed, its category supply is $1$, and before that step the remaining mass is
$$
1-S_{i-1}
=\frac{1}{k_i}+\frac{1}{k_{i+1}-1}
>\frac{1}{k_i}.
$$
Consequently the supply constraint determines the allocation and exhausts $A_i$.
After all $n$ steps, unallocated mass remains:
$$
1-S_n=\frac{1}{k_{n+1}-1}>0.
$$
Only $F$ has positive supply. Every feasible pattern using only $F$ has value at most
$$
hw_F=c_n<\alpha.
$$
The execution therefore stops with positive mass unallocated.
Let
$$
H_n=c_n\frac{k_n}{k_n-1}.
$$
For $n=1$, $c_1=1/2$ and $H_1=1$.
For $n\geq2$,
$$
T_n=T_{n-1}+\frac{1}{k_n-1},
$$
so
$$
H_n=
\frac{k_n}{(k_n-1)T_{n-1}+1}.
$$
Since $T_{n-1}>1$,
$$
k_nT_{n-1}>(k_n-1)T_{n-1}+1,
$$
which proves
$$
H_n>c_{n-1}.
$$
Now fix any real $\alpha\in(C_\infty,1]$. Because $c_n$ decreases to $C_\infty$, there is a least $n$ with $c_n<\alpha$.
If $n=1$, then $\alpha\leq H_1=1$. If $n\geq2$, minimality gives
$$
\alpha\leq c_{n-1}<H_n.
$$
In both cases,
$$
c_n<\alpha\leq H_n,
$$
so the corresponding rational instance has the legal failing execution just proved.
Therefore
$$
G\subseteq(0,C_\infty],
\qquad
\alpha_*\leq C_\infty.
$$
Some finite truncations are:
| $n$ | $k_n$ | $c_n$ | Unallocated mass |
|---:|---:|---:|---:|
| $4$ | $43$ | $42/113$ | $1/1806$ |
| $5$ | $1807$ | $301/810$ | $1/3263442$ |
| $6$ | $3263443$ | $3263442/8782021$ | $1/10650056950806$ |
The instance with $n=4$ has $m=5$, $\tau=1$, and $K=181632$. Since
$$
C_\infty<\frac{42}{113}<\frac{40}{107},
$$
the improvement over the previous upper bound is strict.
For numerical control, the geometric ratio bound gives
$$
0<T_\infty-T_n\leq\frac{2}{k_{n+1}-1}.
$$
Together with the displayed rational value for $n=6$, this justifies the stated approximation to $C_\infty$.
This argument applies to any finite explicitly listed family in the question.
Suppose an execution fails at a positive threshold $\alpha_0$. Before each selected pair $(t,b)$, consider every pair $(u,e)$ whose type has positive remaining mass, whose used categories have positive remaining supply, and whose cardinality is smaller than $|b|$. Minimum cardinality implies
$$
\frac{v_u(e)}{M_u}<\alpha_0.
$$
Only positive-benchmark types are considered.
At the terminal state, consider every pair satisfying the remaining-mass and positive-supply conditions, without a cardinality restriction. Termination likewise implies
$$
\frac{v_u(e)}{M_u}<\alpha_0.
$$
There are finitely many states, types, and patterns. Let $\gamma$ be the maximum of these ratios together with $0$. Then
$$
\gamma<\alpha_0.
$$
Replay the selected sequence at any threshold
$$
\gamma<\alpha\leq\alpha_0.
$$
Inductively, the states remain unchanged:
At the terminal state every available pair remains below threshold. Thus the same execution fails throughout
$$
(\gamma,\alpha_0].
$$
Section 2 shows that $G$ is nonempty and $\alpha_*>0$. If $\alpha_*\notin G$, a failing execution at $\alpha_*$ would exclude some interval $(\gamma,\alpha_*]$ from $G$. But the definition of supremum supplies an element of $G$ greater than $\gamma$, necessarily at most $\alpha_*$. This is a contradiction.
Hence
$$
\boxed{\alpha_*\in G.}
$$
This proves attainment of the actual supremum; it does not assert that the upper bound $C_\infty$ is guaranteed.
For $m=1$, every threshold $\alpha\in(0,1]$ is guaranteed.
Indeed, downward closure gives
$$
\mathcal B=\{0,1,\ldots,C\}
$$
for some integer $C\geq0$. Set
$$
k=\min\{C,\lfloor q\rfloor\}.
$$
For every type with weight $w_t>0$,
$$
M_t=w_tk.
$$
The deterministic pattern $k$ attains this value. A larger benchmark would require every support pattern to have integer size at least $k+1$, which either exceeds $C$ or forces expected consumption greater than $q$.
If $k=0$, all benchmarks are zero. Otherwise, every positive-benchmark type has the same minimum qualifying size
$$
h=\lceil\alpha k\rceil,\qquad 1\leq h\leq k.
$$
Let $P\leq1$ be their total initial mass, and let $D$ be the mass already allocated. While some positive-benchmark mass remains,
$$
\frac{r}{h}
=\frac{q}{h}-D
\geq1-D
\geq P-D>0.
$$
In particular, $r/h$ is at least every individual remaining type mass. Each greedy step therefore allocates pattern $h$ to the chosen type’s entire remaining mass. All types are exhausted.
Thus the unresolved universal constant concerns instances with multiple categories.
Benchmarks can be computed in time polynomial in $m,\tau,L,K$. Compute and sort each type’s $K$ pattern values, then binary-search feasibility of the linear system in Section 1. This uses
$$
O\bigl(\tau\log(K+1)\bigr)
$$
rational LP feasibility tests, each with at most $K$ variables, $m$ supply constraints, one normalization constraint, and nonnegativity constraints.
For a rational threshold of bit length $A$, a specified execution can be implemented by scanning all type-pattern pairs at each step. Since there are at most $m+\tau$ steps, this takes
$$
O\bigl((m+\tau)\tau mK\bigr)
$$
rational arithmetic operations after preprocessing, with polynomial bit complexity in $m,\tau,L,K,A$.
To check the bit bound, start with a common denominator for supplies and masses. Each update introduces at most one additional positive integer pattern-coordinate factor into that denominator. There are at most $m+\tau$ updates, and every coordinate has input-bounded bit length. All states therefore retain polynomial bit length.
Exploring every legal tie-breaking gives an exhaustive verification algorithm for a supplied rational-threshold instance in time
$$
(\tau K+1)^{m+\tau}\operatorname{poly}(m,\tau,L,K,A).
$$
This follows from branching over at most $\tau K$ eligible minimum-cardinality choices at each state and the execution-length bound. It does not compute the universal constant over all instances.
The rigorous conclusion is
$$
\boxed{
\frac{4}{11}\leq\alpha_*\leq
\left(1+\sum_{i=1}^{\infty}\frac{1}{k_i-1}\right)^{-1}
\approx0.3716048959573,
\qquad \alpha_*\text{ is guaranteed}.
}
$$
Determining the exact value requires either a stronger universal lower bound, a smaller counterexample bound, or both. No equality with either endpoint has been proved here.
⟨structured verdict parsed — rendered above⟩
Overall assessment: partial, with sound partial results. The output does not determine the exact value of $\alpha_*$ requested by USER_TASK. It explicitly acknowledges this limitation. Its lower bound, sharper upper bound, and proof that the actual supremum is guaranteed withstand verification. I found no false central step or substantive gap in those partial results.
The unresolved exact value is a major completeness issue, not an error in the established arguments.
The benchmark analysis is correct.
Finding: correct; no issue.
The finite theorem invoked is the minimum-cardinality procedure with the $4/11$ guarantee supplied in USER_TASK. Its hereditary valuation model and arbitrary qualifying choices agree with the cited [Li–Vetta procedure and Theorem 3.1](https://arxiv.org/html/1812.09561v2).
The reduction checks the necessary hypotheses:
The proof correctly establishes membership of $4/11$ in $G$, without requiring an algorithmic replication of the input.
Finding: correct; no issue.
The recurrence and reciprocal calculation are correct:
$$ k_{i+1}-1=k_i(k_i-1), \qquad \frac{1}{k_i-1}-\frac{1}{k_{i+1}-1} =\frac{1}{k_i}. $$
The telescoping sum gives the stated formula for $S_n$. The successive-term ratio is $1/k_i\leq 1/2$, so the convergence assertion and strict decrease of $c_n$ are justified.
The rectangular family is finite, explicitly listable, nonempty, and downward closed. Its cardinality is correctly counted as
$$ K_n=(h+1)\prod_{i=1}^{n}(k_i+1). $$
All supplies and weights are nonnegative rationals. The deterministic pattern $p$ is feasible, consumes exactly $q$, and has value $1$.
The upper benchmark inequality correctly uses linearity and nonnegative weights:
$$ \lambda\leq\mathbb E[v(b)] =w\cdot\mathbb E[b] \leq w\cdot q=1. $$
Thus $M=1$ is established.
At step $i$, the asserted ordering of weights among categories with positive supply is correct. Consequently, every available pattern of cardinality at most $k_i-1$ has value at most $c_n<\alpha$.
The proposed pattern has cardinality $k_i$ and value at least $\alpha$ throughout the specified interval. It therefore has minimum eligible cardinality. The proof needs only one legal failing tie-breaking to disprove a universal guarantee, and it supplies one.
The remaining-mass calculation is correct:
$$ 1-S_{i-1} =\frac{1}{k_i}+\frac{1}{k_{i+1}-1} >\frac{1}{k_i}. $$
Hence the allocation is exactly $1/k_i$ and exhausts category $A_i$. After the last step, positive mass remains, while every feasible pattern using only $F$ has value at most $c_n<\alpha$. Termination with unallocated mass follows.
The inequality $H_n>c_{n-1}$ is correct. Choosing the least index with $c_n<\alpha$ covers every $\alpha\in(C_\infty,1]$, including thresholds equal to earlier truncation values.
Therefore the conclusion
$$ \alpha_*\leq C_\infty $$
is justified.
I independently recomputed the displayed sequence terms, truncation values, residual masses, and the family size for $n=4$. They agree with the output.
In particular,
$$ c_6=\frac{3263442}{8782021} \approx 0.3716048959573200747. $$
The stated tail bound is valid and sufficient to justify the displayed approximation
$$ C_\infty\approx0.3716048959573. $$
The strict comparison with $40/107$ also holds.
Finding: correct; no issue.
This argument correctly avoids assuming monotonicity of $G$.
For a failing execution at $\alpha_0$, every available smaller pattern before a selected allocation has normalized value strictly below $\alpha_0$. The same strict inequality holds for every available pair at termination.
There are finitely many relevant pairs and states. Including $0$ makes the maximum $\gamma$ well-defined even if no such pairs exist, and positivity of $\alpha_0$ ensures
$$ \gamma<\alpha_0. $$
For every threshold in $(\gamma,\alpha_0]$:
Thus the same failure persists throughout that interval.
Since $G$ is nonempty, its positive supremum cannot itself have such a failing interval immediately below it: the defining property of the supremum would provide an element of $G$ inside that interval.
The conclusion $\alpha_*\in G$ follows. The output correctly distinguishes this from guaranteeing $C_\infty$.
Finding: correct; no issue.
The characterization
$$ \mathcal B=\{0,1,\ldots,C\} $$
is valid. The benchmark formula with $k=\min\{C,\lfloor q\rfloor\}$ correctly accounts for integer pattern sizes and possibly nonintegral supply.
Zero weights and $k=0$ are handled. When $k>0$, all positive-benchmark types have the same minimum qualifying size $h=\lceil\alpha k\rceil$.
The supply calculation
$$ \frac rh=\frac qh-D\geq1-D\geq P-D>0 $$
is correct whenever positive-benchmark mass remains. It also shows that supply suffices to serve the chosen type’s entire remaining mass. Hence every threshold in $(0,1]$ succeeds for one category.
Finding: correct; no issue.
The computational claims are justified for the stated representation.
These results concern benchmark computation, individual executions, and exhaustive verification of a fixed instance. They do not compute the universal constant.
Finding: correct; no issue.
Major issue — exact value remains unresolved.
USER_TASK asks for the supremum itself, together with whether it is guaranteed. The output settles the attainment question but establishes only an interval for the value:
$$ \frac4{11}\leq\alpha_*\leq C_\infty. $$
The endpoints differ, and no argument identifies the supremum within that interval.
Minimum additional work required: establish an exact value by proving matching universal-guarantee and exclusion bounds, or another result that determines $\alpha_*$. No clarification or routine expositional repair can supply this missing conclusion.
The prover accurately labels its work as partial. The established arguments are genuine progress and merit another round.
⟨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.