Answer: —
Theorem 6.1 — class: hardness
PDF text-layer excerpt — equations and symbol order may be approximateFor all k ≥2 it holds that r∗ k ≤r∗ 1. Further, r∗ k ≤rk for all 2 ≤k ≤8, with values of rk given in Table 1.
statement extracted from the paper’s text layer; consult the paper for the exact wording
For fixed \(k\), let a society have finite-support rational distributions \(\mu\) and \(\nu\) over seller and buyer valuation schedules \(w\) and \(v\), respectively, with each schedule increasing and submodular. Give each pair \((w,v)\) mass \(\mu_w\nu_v\), and let \(q_p(w,v)\) be the quantity traded under the paper’s sequential fixed-price mechanism at common per-unit price \(p\). Determine the worst-case population guarantee \(\rho_k^{\mathrm{pop}}=\inf_{\mu,\nu}\sup_{p\ge 0} W_{\mu,\nu}(p)/O_{\mu,\nu}\), where \(W_{\mu,\nu}(p)=\sum_{w,v}\mu_w\nu_v\bigl(v(q_p(w,v))+w(k-q_p(w,v))\bigr)\) and \(O_{\mu,\nu}=\sum_{w,v}\mu_w\nu_v\max_{0\le q\le k}\bigl(v(q)+w(k-q)\bigr)\).
Fix an integer \(k\ge 2\). A seller initially owns \(k\) indivisible units and a buyer owns none. Their types are strictly increasing submodular schedules \(w,v:\{0,\ldots,k\}\to\mathbb{Q}_{\ge0}\), with \(w(0)=v(0)=0\).
A society is given by its support: two nonempty lists of seller and buyer types, each with positive binary-rational mass; each list's masses sum to \(1\). Let \(\tau\) be the total number of listed types, not the number of possible schedules. Draw the two types independently, giving pair \((w,v)\) mass \(\mu_w\nu_v\). Let \(L\) be the total input bit length; state any running times in \(m=k\), \(\tau\), \(L\), and any additional parameters.
At a common per-unit price \(p\in\mathbb{R}_{\ge0}\), offer successive units until the first rejection: after \(q-1\) trades, unit \(q\) trades exactly when \(w(k-q+1)-w(k-q)\le p\le v(q)-v(q-1)\). Both agents accept equality. Denote the resulting quantity by \(q_p(w,v)\).
Define \(W_{\mu,\nu}(p)=\sum_{w,v}\mu_w\nu_v\bigl(v(q_p(w,v))+w(k-q_p(w,v))\bigr)\) and \(O_{\mu,\nu}=\sum_{w,v}\mu_w\nu_v\max_{q\in\{0,\ldots,k\}}\bigl(v(q)+w(k-q)\bigr)\).
What is the tight worst-case welfare approximation guarantee \(\rho_k^{\mathrm{pop}}=\inf_{\mu,\nu}\sup_{p\ge0}W_{\mu,\nu}(p)/O_{\mu,\nu}\), where the infimum ranges over all such societies with unrestricted finite support size?
For indivisible units with independent integrable valuation priors, the known approximation upper bounds satisfy \(r_k^*\le r_1^*\) for every \(k\ge2\), and are respectively \(0.7291,0.7277,0.7284,0.7276,0.7272,0.7286,0.7278\) for \(k=2,\ldots,8\); a universal lower bound of \(0.65\) holds for \(k=2\). [Verified bounds](https://ojs.aaai.org/index.php/AAAI/article/download/38741/42703).
A subsequent preprint supplies a strictly positive finite rational two-unit instance with ratio below \(0.7290804\), directly bounding \(\rho_2^{\mathrm{pop}}\); it leaves the exact two-unit and higher-unit guarantees open. [Verified subsequent results](https://arxiv.org/html/2609.35888v1).
The tight value of $\rho_k^{\mathrm{pop}}$ is not determined below. The main new result is a uniform bound on the support size and bit length needed to approximate the worst case.
Write $m=k$. For every rational $0<\epsilon\le1$, I prove that an explicit finite collection of societies contains one whose ratio is at most $\rho_m^{\mathrm{pop}}+\epsilon$. Each society in this collection has at most
$$ O\!\left(\frac{m}{\epsilon^2}\right) $$
types per side, dyadic masses, and total input bit length
$$ O\!\left(\frac{m^2}{\epsilon^2}\log\frac{m}{\epsilon}\right). $$
Consequently, exhaustive search gives a certified interval of width $\epsilon$ containing $\rho_m^{\mathrm{pop}}$. This advances the instance-dependent approximation in the notes to a uniform finite reduction, but does not supply the exact constant.
For each seller and buyer type, define
$$ a_q(w)=w(m-q+1)-w(m-q), \qquad b_q(v)=v(q)-v(q-1), \qquad 1\le q\le m. $$
Strict increase and submodularity imply
$$ 0<a_1(w)\le\cdots\le a_m(w), \qquad b_1(v)\ge\cdots\ge b_m(v)>0. $$
Conversely, any positive vectors satisfying these orders define admissible schedules through
$$ w(j)=\sum_{q=m-j+1}^{m}a_q, \qquad v(j)=\sum_{q=1}^{j}b_q. $$
Indeed, the increments of $w$ are $a_m,\ldots,a_1$, and those of $v$ are $b_1,\ldots,b_m$. Both increment sequences are positive and nonincreasing.
Let $A_q=a_q(w)$ and $B_q=b_q(v)$ under the independent draws. Define
$$ h_p(a,b)=a+(b-a)\mathbf1_{\{a\le p\le b\}}. $$
Lemma 1. Posted-price and efficient welfare satisfy
$$ W(p)=\sum_{q=1}^{m}\mathbb E h_p(A_q,B_q), \qquad O=\sum_{q=1}^{m}\mathbb E\max\{A_q,B_q\}. $$
Proof. If $a_q\le p\le b_q$, then for every $r<q$,
$$ a_r\le a_q\le p\le b_q\le b_r. $$
Thus acceptance of unit $q$ implies acceptance of every preceding unit. Its trade indicator is therefore exactly $\mathbf1_{\{a_q\le p\le b_q\}}$. Initial welfare is $\sum_q a_q$, and trade $q$ changes welfare by $b_q-a_q$, proving the first identity.
After $j$ trades, welfare is
$$ \sum_{q=1}^{m}a_q+\sum_{q=1}^{j}(b_q-a_q). $$
The differences $b_q-a_q$ are nonincreasing, so their positive terms form a prefix. Taking that prefix maximizes welfare, giving
$$ \sum_{q=1}^{m}a_q+\sum_{q=1}^{m}(b_q-a_q)_+ = \sum_{q=1}^{m}\max\{a_q,b_q\}. $$
Taking expectations proves the second identity. $\square$
In particular, only the coordinate marginal distributions matter. Dependence between coordinates on the same side does not affect either expression; independence between the two sides remains essential.
Write
$$ S=\sup_{p\ge0}W(p), \qquad R=\frac SO. $$
Pointwise, posted-price welfare is an available allocation’s welfare, so $0<S\le O$ and $0<R\le1$.
This section also repairs the bit-complexity imprecision identified in the verifier report.
Let $\tau$ be the total number of listed types. The set of marginal events is
$$ \mathcal E= \{a_q(w):w\text{ listed},\ 1\le q\le m\} \cup \{b_q(v):v\text{ listed},\ 1\le q\le m\}. $$
It has at most $m\tau$ distinct values.
Every positive marginal gain is active on a closed interval $[a_q(w),b_q(v)]$. If $p$ lies strictly between consecutive events $x<y$, moving to $x$ preserves every positive-gain trade active at $p$. Outside the event range, no positive gain occurs. Hence
$$ S=\max_{p\in\mathcal E}W(p). $$
For an exact sweep, maintain
$$ F_q(p)=\Pr(A_q\le p), \qquad C_q(p)=\mathbb E[A_q\mathbf1_{\{A_q\le p\}}], $$
$$ H_q(p)=\Pr(B_q\ge p), \qquad T_q(p)=\mathbb E[B_q\mathbf1_{\{B_q\ge p\}}]. $$
Independence gives expected marginal gain
$$ G_q(p)=F_q(p)T_q(p)-H_q(p)C_q(p). $$
Before the first event, initialize $F_q=C_q=0$, $H_q=1$, and $T_q=\mathbb E B_q$. At each event $x$:
$$ \alpha(T_q-xH_q). $$
$$ -\beta(xF_q-C_q). $$
Maintaining $\sum_qG_q$ requires constant arithmetic work per atom.
Efficient welfare is accumulated simultaneously. When a seller atom $A_q=x$ is processed, the maintained buyer tail includes precisely $B_q\ge x$, and
$$ \mathbb E\max\{x,B_q\}=x(1-H_q)+T_q. $$
Multiplying by the seller atom’s mass and summing yields $O$.
Thus exact evaluation takes
$$ O\!\left(m\tau\log(m\tau)\right) $$
rational arithmetic operations.
For total input bit length $L$, the sweep quantities and welfare totals have $O(L)$ bits. Their expanded expressions involve input masses, at most one marginal value per term, and sums; a common denominator divides the product of input denominators. Their magnitudes also have logarithmic size $O(L)$.
The final ratio needs a separate argument: dividing two fractions of $O(L)$ bit length produces another fraction of $O(L)$ bit length, even though its denominator need not divide that common denominator. Reduced-fraction arithmetic therefore gives the conservative bit running time
$$ O\!\left(m\tau\log(m\tau)L^3\right). $$
Multiplying all marginal values and prices by the same positive number preserves every trade pattern and scales $S$ and $O$ equally. Normalize the instance so that
$$ O=1. $$
Lemma 1 then implies
$$ \sum_{q=1}^{m}\mathbb E A_q\le1, \qquad \sum_{q=1}^{m}\mathbb E B_q\le1. $$
Consequently,
$$ \sum_{q=1}^{m}(\mathbb E A_q)(\mathbb E B_q) \le \left(\sum_q\mathbb E A_q\right) \left(\sum_q\mathbb E B_q\right) \le1. $$
The argument below also applies to independent real-valued ordered marginal vectors with finite expected total values.
Lemma 2. For every $M>0$,
$$ S\le\sup_{0\le p\le M}W(p)+\frac1M. $$
Proof. For $p>M$, if $a\le M$, every trade occurring at $p$ also occurs at $M$, with the same welfare. Thus $h_p(a,b)\le h_M(a,b)$.
If $a>M$, then $h_M(a,b)=a$, and
$$ h_p(a,b)-h_M(a,b)\le b. $$
Combining the cases,
$$ h_p(a,b)\le h_M(a,b)+b\mathbf1_{\{a>M\}}. $$
Independence and Markov’s inequality give
$$ \mathbb E[B_q\mathbf1_{\{A_q>M\}}] = (\mathbb E B_q)\Pr(A_q>M) \le \frac{(\mathbb E A_q)(\mathbb E B_q)}M. $$
Summing over coordinates bounds the extra welfare by $1/M$. Taking the supremum proves the claim. $\square$
This bound controls large prices using first moments, without bounding individual marginal values.
For a positive integrable random variable $X$, let
$$ F_X(x)=\Pr(X\le x), \qquad Q_X(t)=\inf\{x:F_X(x)\ge t\}, \qquad 0<t<1. $$
Fix an integer $N\ge1$. Partition $(0,1)$ into intervals
$$ I_i=\left(\frac{i-1}{N},\frac{i}{N}\right), \qquad 1\le i\le N, $$
and define
$$ x_i=N\int_{I_i}Q_X(t)\,dt. $$
Let $\widehat X$ take the values $x_1,\ldots,x_N$, each with probability $1/N$.
Quantile integration gives
$$ \mathbb E\widehat X = \frac1N\sum_i x_i = \int_0^1Q_X(t)\,dt = \mathbb EX. $$
These identities follow by representing $X$ in distribution as $Q_X(U)$ for a uniform random variable $U$.
Every $x_i$ is finite by integrability. It is positive because $X>0$ almost surely: right continuity of $F_X$ at zero implies $Q_X(t)>0$ for every $t>0$.
The approximation satisfies
$$ \sup_x|F_{\widehat X}(x)-F_X(x)|\le\frac1N. $$
To verify this, fix $x$ and put $f=F_X(x)$. Up to endpoints of measure zero, $Q_X(t)\le x$ exactly for $t\le f$. Every interval entirely below $f$ has mean at most $x$, and every interval entirely above $f$ has mean greater than $x$. At most one interval straddles $f$. Hence the number of averages at most $x$, divided by $N$, differs from $f$ by at most $1/N$.
Taking left limits also gives
$$ \sup_p \left| \Pr(\widehat X\ge p)-\Pr(X\ge p) \right| \le\frac1N. $$
Apply this construction to every coordinate, using the same intervals within each side:
$$ \widehat a_{q,i} = N\int_{I_i}Q_{A_q}(t)\,dt, \qquad \widehat b_{q,i} = N\int_{I_i}Q_{B_q}(t)\,dt. $$
Almost-sure order $A_q\le A_{q+1}$ implies
$$ F_{A_q}(x)\ge F_{A_{q+1}}(x), $$
and therefore
$$ Q_{A_q}(t)\le Q_{A_{q+1}}(t). $$
Integrating proves
$$ \widehat a_{1,i}\le\cdots\le\widehat a_{m,i}. $$
The buyer coordinates satisfy the reverse order by the same argument.
Thus the $N$ seller vectors and $N$ buyer vectors are admissible types. Select their indices independently and uniformly. If $N$ is a power of two, their masses are dyadic; duplicate vectors can be combined.
Normalization and preservation of means give the useful bound
$$ 0<\widehat a_{q,i}\le N\mathbb E A_q\le N, \qquad 0<\widehat b_{q,i}\le N\mathbb E B_q\le N. $$
Denote the averaged instance’s quantities by $\widehat W$, $\widehat S$, and $\widehat O$.
For one coordinate, define
$$ F(p)=\Pr(A\le p), \qquad H(p)=\Pr(B\ge p), $$
$$ K(p)=\mathbb E(p-A)_+, \qquad L(p)=\mathbb E(B-p)_+. $$
Splitting $B-A=(B-p)+(p-A)$ on the trading event, and using independence, gives
$$ G(p)=\mathbb E[(B-A)\mathbf1_{\{A\le p\le B\}}] = F(p)L(p)+H(p)K(p). $$
For a nonnegative random variable $X$,
$$ \mathbb E(p-X)_+=\int_0^pF_X(t)\,dt. $$
Therefore the uniform distribution-function error implies
$$ |\widehat K(p)-K(p)|\le\frac pN. $$
Also,
$$ \mathbb E(B-p)_+ = \mathbb EB-p+\mathbb E(p-B)_+. $$
Since quantile averaging preserves $\mathbb EB$,
$$ |\widehat L(p)-L(p)|\le\frac pN. $$
Using $L(p)\le\mathbb EB$, $K(p)\le p$, and probabilities at most one,
$$ \begin{aligned} |\widehat G(p)-G(p)| &\le |\widehat F-F|L +\widehat F|\widehat L-L|\\ &\quad+ |\widehat H-H|K +\widehat H|\widehat K-K|\\ &\le \frac{\mathbb EB+3p}{N}. \end{aligned} $$
The seller baseline is preserved exactly. Summing over coordinates yields, for $0\le p\le M$,
$$ |\widehat W(p)-W(p)| \le \frac{1+3mM}{N}. $$
The averaged instance preserves both sides’ first moments, so Lemma 2 applies to it with the same bound. Consequently,
$$ \widehat S \le S+\frac{1+3mM}{N}+\frac1M. $$
First,
$$ \widehat O\le O=1. $$
Indeed, represent the original coordinate pair as $Q_{A_q}(U),Q_{B_q}(V)$ for independent uniform $U,V$. Conditional on $U\in I_i$ and $V\in I_j$, the expected maximum is at least each conditional mean, hence at least
$$ \max\{\widehat a_{q,i},\widehat b_{q,j}\}. $$
Averaging over $i,j$ and summing over coordinates proves the inequality.
For the opposite bound, use
$$ \max\{A,B\}=A+B-\min\{A,B\}. $$
Means are preserved, so
$$ O-\widehat O = \sum_q \left( \mathbb E\min\{\widehat A_q,\widehat B_q\} - \mathbb E\min\{A_q,B_q\} \right). $$
Independence and integration of nonnegative tails give
$$ \mathbb E\min\{A,B\} = \int_0^\infty\Pr(A>t)\Pr(B>t)\,dt. $$
On $[0,M]$, the product of the two survival functions changes by at most $2/N$. On $(M,\infty)$, the averaged tail satisfies
$$ \begin{aligned} \int_M^\infty \Pr(\widehat A_q>t)\Pr(\widehat B_q>t)\,dt &\le \Pr(\widehat A_q>M) \int_M^\infty\Pr(\widehat B_q>t)\,dt\\ &\le \frac{(\mathbb E A_q)(\mathbb E B_q)}M. \end{aligned} $$
Dropping the nonnegative original tail and summing proves
$$ 0\le1-\widehat O \le \frac{2mM}{N}+\frac1M. $$
The averaged instance has at most $2mN$ distinct marginal values. List them as
$$ 0<x_1<\cdots<x_J\le N, \qquad J\le2mN. $$
Choose a positive integer $D$, and put
$$ Q=2mN+1. $$
Replace every occurrence of $x_j$ by
$$ z_j=\frac{\lfloor Dx_j\rfloor}{D}+\frac{j}{DQ}. $$
The floor terms are nondecreasing and the rank terms strictly increase. Thus
$$ 0<z_1<\cdots<z_J, \qquad |z_j-x_j|<\frac1D. $$
Every replacement belongs to the universal grid
$$ \mathcal G= \left\{ \frac{\ell}{DQ}:1\le\ell\le H \right\}, \qquad H=Q(DN+1). $$
Strict preservation of the global event order preserves every price-induced trade pattern: an event price corresponds to its replacement event, and an intervening interval corresponds to the intervening interval with the same index. Equality cases are preserved as well.
For corresponding prices, each marginal welfare term selects the seller value in both instances or the buyer value in both. Therefore, writing $S_{\mathrm{rat}}$ and $O_{\mathrm{rat}}$ for the rationalized instance,
$$ |S_{\mathrm{rat}}-\widehat S|\le\frac mD, \qquad |O_{\mathrm{rat}}-\widehat O|\le\frac mD. $$
The efficient-welfare bound follows because changing both arguments by less than $1/D$ changes their maximum by less than $1/D$.
Reconstructing schedules from these positive ordered marginals produces admissible rational types.
Fix rational $0<\epsilon\le1$. Set
$$ M=\frac{16}{\epsilon}, $$
let $N$ be the smallest power of two satisfying
$$ N\ge\frac{256m}{\epsilon^2}, $$
and choose
$$ D=\left\lceil\frac{16m}{\epsilon}\right\rceil. $$
Then
$$ \frac{mM}{N}\le\frac{\epsilon}{16}, \qquad \frac1N\le\frac{\epsilon}{256}, \qquad \frac1M=\frac{\epsilon}{16}, \qquad \frac mD\le\frac{\epsilon}{16}. $$
The posted-price bounds give
$$ S_{\mathrm{rat}} \le S+\frac{65\epsilon}{256}+\frac{\epsilon}{16} = S+\frac{81\epsilon}{256}. $$
The efficient-welfare bounds give
$$ O_{\mathrm{rat}} \ge 1-\frac{\epsilon}{8}-\frac{\epsilon}{16}-\frac{\epsilon}{16} = 1-\frac{\epsilon}{4}. $$
Since the normalized original ratio is $R=S\le1$,
$$ \begin{aligned} \frac{S_{\mathrm{rat}}}{O_{\mathrm{rat}}}-R &\le \frac{R+81\epsilon/256}{1-\epsilon/4}-R\\ &= \frac{81\epsilon/256+R\epsilon/4}{1-\epsilon/4}\\ &\le \frac{145\epsilon/256}{3/4}\\ &= \frac{145}{192}\epsilon < \epsilon. \end{aligned} $$
This proves the following uniform statement.
Theorem 3. Every admissible society with ratio $R$ has an admissible rational approximation with ratio at most $R+\epsilon$, at most $N$ types per side, dyadic masses, and all marginal values in the explicit grid $\mathcal G$ above.
The proof also applies to independent integrable real-valued admissible priors.
Let $u_{m,\epsilon}$ be the minimum ratio among societies obtained by selecting $N$ seller vectors and $N$ buyer vectors from $\mathcal G^m$, with the required coordinate orders, and assigning probability $1/N$ to every selected vector. Repeated vectors are combined.
This is a finite nonempty collection of valid societies, so
$$ \rho_m^{\mathrm{pop}}\le u_{m,\epsilon}. $$
Theorem 3 applies to every society in the definition of $\rho_m^{\mathrm{pop}}$. Taking the infimum of its original ratio gives
$$ u_{m,\epsilon}\le\rho_m^{\mathrm{pop}}+\epsilon. $$
Thus the exact finite-search output certifies
$$ \boxed{ u_{m,\epsilon}-\epsilon \le \rho_m^{\mathrm{pop}} \le u_{m,\epsilon}. } $$
No attainment of the unrestricted infimum is assumed.
The parameters satisfy
$$ N=O\!\left(\frac{m}{\epsilon^2}\right), \qquad D=O\!\left(\frac{m}{\epsilon}\right), \qquad H=O\!\left(\frac{m^4}{\epsilon^5}\right). $$
Each candidate has $\tau\le2N$. Its schedules have denominator $DQ$ and numerators at most $mH$, while its masses have denominator $N$. Its total bit length is therefore bounded by
$$ L_* = O\!\left(mN\log(mND)\right) = O\!\left( \frac{m^2}{\epsilon^2}\log\frac{m}{\epsilon} \right). $$
There are at most $H^{2mN}$ candidate arrays. Using the exact evaluator from Section 2, exhaustive search takes at most
$$ H^{2mN}\, O\!\left(mN\log(mN)L_*^3\right) $$
bit operations, apart from polynomial work in the encoding length of $\epsilon$ to form the parameters. Equivalently, the search contribution is bounded by
$$ \exp\!\left( O\!\left( \frac{m^2}{\epsilon^2}\log\frac{m}{\epsilon} \right) \right). $$
This proves computability with a certified error bound; the running time is not practical.
There is also an immediate extension of the finite-prior equivalence in the notes. Let $r_m^{\mathrm{int}}$ be the infimum over independent integrable real-valued admissible priors. Subclass inclusion gives $r_m^{\mathrm{int}}\le\rho_m^{\mathrm{pop}}$. Applying Theorem 3 to every such prior gives the reverse inequality up to arbitrary $\epsilon>0$. Hence
$$ r_m^{\mathrm{int}}=\rho_m^{\mathrm{pop}}. $$
The numerical gap remains. The supplied two-unit lower theorem applies because our priors are independent, our schedules are strictly increasing and submodular, and finite support ensures integrability. It gives $\rho_2^{\mathrm{pop}}\ge0.65$. [AAAI paper, Theorem 1.2](https://ojs.aaai.org/index.php/AAAI/article/download/38741/42703). The subsequent finite-instance result gives $\rho_2^{\mathrm{pop}}<0.7290804$. [Preprint, Theorem D and Appendix E](https://arxiv.org/html/2609.35888v1#S13).
The finite reduction proved here does not identify the minimizing distributions or establish matching bounds. It gives certified additive approximations to the target constant, while leaving its exact value open.
⟨structured verdict parsed — rendered above⟩
Overall assessment: correct partial progress. The uniform finite reduction is sound as written. I found no false central step or gap requiring new mathematics within that reduction. However, the output does not determine the tight guarantee requested in USER_TASK; it explicitly leaves that question open.
The seller’s marginal costs are positive and nondecreasing; the buyer’s marginal values are positive and nonincreasing. The reconstruction formulas yield strictly increasing submodular schedules with value zero at zero.
Acceptance of unit $q$ implies acceptance of every earlier unit, including all equality cases. Thus the indicator used in $h_p$ correctly represents sequential trading.
The differences $b_q-a_q$ are nonincreasing, so taking their positive prefix maximizes welfare. Zero differences do not affect the optimum. Both identities in Lemma 1 follow.
The assertion that only coordinate marginal distributions matter is correct for these welfare expressions. It does not assert that arbitrary coordinate marginals can be assembled into admissible types; Section 4 separately establishes the required ordering.
There are at most $m\tau$ marginal events. Every positive gain is supported on a closed interval, so moving an interior price to its preceding event preserves all gains active at that price. Outside the event range, welfare is the seller baseline. Consequently,
$$
S=\max_{p\in\mathcal E}W(p).
$$
Independence correctly gives
$$
G_q=F_qT_q-H_qC_q.
$$
Both update formulas are correct. Adding seller atoms before evaluation and removing buyer atoms afterward implements inclusive acceptance, including coincident seller and buyer events.
When processing a seller atom at $x$, the buyer tail contains exactly the atoms with $B_q\ge x$. Hence the formula for its efficient-welfare contribution is correct.
The arithmetic-operation count includes sorting and linear processing of the atoms. The bit bound is also justified: expanded welfare expressions use one seller mass, one buyer mass, and a selected marginal value per term. Marginal differences introduce input schedule denominators already accounted for in the product of input denominators. Magnitudes and reduced numerators and denominators therefore have $O(L)$ bits. The stated conservative bound
$$
O\!\left(m\tau\log(m\tau)L^3\right)
$$
is valid.
Strict positivity ensures $O>0$, so normalization is legitimate. For an original rational finite society, the normalization factor is rational.
The first-moment bounds follow from Lemma 1. The bound on the sum of products follows from nonnegativity.
For $p>M$, the pointwise comparison in Lemma 2 is correct in both cases $a\le M$ and $a>M$. Independence justifies factoring the expectation, and Markov’s inequality applies because the variables are nonnegative and integrable.
Although the averaged instance need not have efficient welfare exactly one, the later application remains valid: the proof uses the preserved first-moment bounds, which that instance still satisfies.
Quantile integration preserves the mean. Integrability makes every interval average finite; almost-sure positivity makes each average strictly positive.
For each threshold, at most one quantile interval straddles its distribution-function level. This proves the stated uniform error of $1/N$. Taking left limits correctly transfers the bound to inclusive upper-tail probabilities, including atoms.
Almost-sure coordinate ordering implies stochastic ordering and the corresponding quantile ordering. Averaging over common intervals therefore produces admissible ordered vectors. Drawing the seller and buyer indices independently preserves independence between sides.
The bound on each averaged marginal follows from its interval integral being at most the full quantile integral. Dyadic masses follow from choosing $N$ as a power of two.
The decomposition
$$
G(p)=F(p)L(p)+H(p)K(p)
$$
correctly splits the gain on the trading event. Equality cases cause no error because the corresponding positive-part term vanishes at equality.
The integral formulas for positive parts are valid for nonnegative integrable variables. Preservation of the buyer mean yields the asserted upper positive-part error.
The four-term product estimate correctly gives
$$
|\widehat G(p)-G(p)|
\le\frac{\mathbb EB+3p}{N}.
$$
Summation, preservation of the seller baseline, and Lemma 2 establish the claimed bound on $\widehat S$.
The conditional-mean comparison establishes $\widehat O\le O$. It is applied coordinate by coordinate, which is sufficient because Lemma 1 expresses efficient welfare as a sum of coordinate expectations.
The identity involving the minimum is correct. Independence supplies the product-tail representation, and nonnegativity permits tail integration.
On the bounded interval, the product-tail error is at most $2/N$. The averaged tail estimate uses monotonicity, Markov’s inequality, and preservation of means correctly. Dropping the original nonnegative tail is appropriate for the desired upper bound. Thus
$$
0\le1-\widehat O\le\frac{2mM}{N}+\frac1M
$$
follows.
The replacement values are positive and strictly ordered. Since $j<Q$, their displacement from the original values is strictly less than $1/D$. Their numerators lie within the stated grid.
Replacing each distinct value consistently preserves ties as well as strict comparisons. Thus event prices and intervening intervals retain their trade patterns, including equality acceptance.
For corresponding prices, each coordinate welfare contribution selects the same side’s marginal value. The bounds on optimal posted-price welfare and efficient welfare therefore follow. Reconstruction retains all admissibility requirements.
All four parameter inequalities hold for $m\ge2$ and $0<\epsilon\le1$. The posted-price error before rationalization is
$$
\frac{\epsilon}{256}
+\frac{3\epsilon}{16}
+\frac{\epsilon}{16}
=\frac{65\epsilon}{256}.
$$
Rationalization raises this to $81\epsilon/256$.
The efficient-welfare losses total at most $\epsilon/4$. The resulting denominator is at least $3/4$, and the final ratio estimate
$$
\frac{145}{192}\epsilon<\epsilon
$$
is correct. Theorem 3 is established.
Every candidate is an admissible society, so its minimum ratio bounds the unrestricted infimum from above. Theorem 3 bounds that finite minimum from above by the unrestricted infimum plus $\epsilon$. This argument does not require attainment of the unrestricted infimum.
The bounds on $N$, $D$, $H$, candidate bit length, and candidate count are consistent. Exact enumeration and evaluation give the advertised certified interval and exponential search bound, with the separately stated polynomial dependence on the encoding length of $\epsilon$.
The equality between the finite rational and integrable real-valued infima follows from subclass inclusion and the established approximation theorem. Strict positivity and finite first moments are maintained throughout.
The lower-bound theorem concerns the same independent, integrable, strictly increasing submodular model and gives the stated two-unit guarantee. Finite rational societies satisfy its hypotheses. [AAAI paper, Theorem 1.2](https://ojs.aaai.org/index.php/AAAI/article/download/38741/42703).
The preprint’s Theorem D and Appendix E describe a strictly positive finite rational ordered instance under inclusive acceptance, with the stated strict upper bound. This agrees with the verified result supplied in USER_TASK. [Preprint, Section 13 and Appendix E](https://arxiv.org/html/2609.35888v1#S13).
Major — unresolved assigned target, rather than an error in the partial proof. The requested tight value of $\rho_k^{\mathrm{pop}}$ is not determined. A certified approximation algorithm supplies substantive information about the constant but does not establish an exact value or matching welfare bounds.
No additional clarification is needed to verify the finite reduction. Resolving the original assignment requires an exact characterization with a proof of tightness, or matching universal lower and upper bounds. The prover already acknowledges this limitation accurately.
References to unspecified “notes” and a previous verifier report are unnecessary context; the reduction itself is self-contained.
⟨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.