← back to the atlas

d4-conf-wine-2012-0015 (d4-conf-wine-2012-0015)

Answer: \(\inf_M\rho(M)=e/(e-1)<2\), attained by a truthful, individually rational, budget-feasible mechanism computable in polynomial time.

The anchor (named result in the paper)

Theorem 4 — class: hardness

PDF text-layer excerpt — equations and symbol order may be approximateFor all $\varepsilon>0$, there is no truthful, individually rational, budget feasible DCLEF mechanism that is also $2-\varepsilon$-approximate with respect to $OPT$.

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

The continuous mirror question, as graded

Given a rational distribution \(\mu\) over complete types \(t=(a_t,d_t,v_t)\), with public predictor coefficient \(a_t\), verified data value \(d_t\), and private unit cost \(v_t\), consider direct mechanisms that observe cost reports and assign each user an inclusion probability and expected scaled transfer. Require dominant-strategy truthfulness and individual rationality for each user, and integrated transfers within budget \(B\). For \(\theta_t\in[0,1]\), define residual weight \(R=\sum_t\mu_t|a_t|(1-\theta_t)\); selected users incur privacy cost \(v_t|a_t|/R\). What is the best worst-case approximation ratio for maximizing \(\sum_t\mu_t|a_t|\theta_t\), relative to the cost-aware benchmark \(\mathrm{OPT}=\max_{\theta\in[0,1]^\tau}\{\sum_t\mu_t|a_t|\theta_t:\sum_t\mu_t|a_t|(v_t+B)\theta_t\le B\sum_t\mu_t|a_t|\}\), and can a truthful mechanism achieve a ratio below \(2\)?

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

A society is an atomless population of total mass \(1\), represented by the support list of \(\tau\) complete types \(t=(a_t,d_t,v_t)\), with positive binary rational masses \(\mu_t\) summing to \(1\); \(\tau\) counts supported types, not possible types. All input numbers are binary rationals, \(a_t\ne0\), \(v_t>0\), \(B>0\), and verified data lie in a fixed bounded interval \([D_{\min},D_{\max}]\) with \(D_{\min}<D_{\max}\). Coefficients are public; only costs can be reported falsely.
A direct mechanism observes the reported distribution \(\nu\), not the true cost distribution, and supplies menus \(\theta_\nu(a,d,r)\in[0,1]\) and \(p_\nu(a,d,r)\ge0\) for every positive rational cost report \(r\), including reports outside its support. These are inclusion probabilities and expected transfers per unit population mass, in the same units as \(B\).
For each reported distribution, write \(\theta_t=\theta_\nu(a_t,d_t,r_t)\), \(p_t=p_\nu(a_t,d_t,r_t)\), and require \(R_\nu=\sum_t\nu_t|a_t|(1-\theta_t)>0\) and \(\sum_t\nu_t p_t\le B\). A selected user of true cost \(v\) incurs cost \(v|a|/R_\nu\); an excluded user incurs zero cost.
A unilateral report changes neither \(\nu\) nor \(R_\nu\). For every \(\nu,a,d,v,r\), dominant-strategy truthfulness requires \(p_\nu(a,d,v)-v|a|\theta_\nu(a,d,v)/R_\nu\ge p_\nu(a,d,r)-v|a|\theta_\nu(a,d,r)/R_\nu\); individual rationality requires the truthful utility to be nonnegative. Both conditions concern expected utility, with residual weight computed from inclusion probabilities.
On truthful input \(\mu\), the objective is \(S_M(\mu)=\sum_t\mu_t|a_t|\theta_t\), and the cost-aware benchmark is \(\mathrm{OPT}(\mu)=\max\{\sum_t\mu_t|a_t|z_t:z\in[0,1]^\tau,\ \sum_t\mu_t|a_t|(v_t+B)z_t\le B\sum_t\mu_t|a_t|\}\). Define \(\rho(M)=\sup_\mu\mathrm{OPT}(\mu)/S_M(\mu)\), with ratio \(+\infty\) when \(S_M(\mu)=0\). State running times in \(\tau\), total input bit length \(L\), and any approximation parameter; the statistic is scalar, so \(m=1\).

What is the infimum worst-case approximation ratio \(\inf_M\rho(M)\) over these truthful, individually rational, budget-feasible mechanisms; in particular, can any such mechanism guarantee \(\rho(M)<2\)?

For finite agents with binary inclusion, no truthful, individually rational, budget-feasible canonical Laplace mechanism guarantees \(2-\varepsilon\) for any \(\varepsilon>0\); a \(5\)-approximation exists, improved to \(2\) for equal absolute weights. [Source](https://ece.northeastern.edu/fac-ece/ioannidis/static/pdf/2014/priv-auction-singlecol_1.pdf).
The finite-agent fractional benchmark without truthfulness has a polynomial-time optimum; this does not settle the atomless truthful problem specified here. No result settling that exact problem was located. [Source](https://ece.northeastern.edu/fac-ece/ioannidis/static/pdf/2014/priv-auction-singlecol_1.pdf).

Modeling choices made when packaging the task

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

Result

Under the fixed-distribution notion of unilateral deviation in the question,

\[ \inf_M \rho(M)=\frac{e}{e-1}\approx 1.582<2. \]

The infimum is attained by a mechanism computable in \(\mathop{\mathrm{poly}}(\tau,L)\) time. The proof below gives both a truthful mechanism achieving this bound and finite rational instances establishing its optimality.

The fixed-distribution assumption is essential: a unilateral report changes the selected menu entry but leaves the menu and its residual weight unchanged. The finite-agent lower bound in the [cited paper](https://ece.northeastern.edu/fac-ece/ioannidis/static/pdf/2014/priv-auction-singlecol_1.pdf) therefore does not establish a lower bound of \(2\) for this model.

1. Normalize the benchmark

For any reported input, define \(w_t=\nu_t|a_t|\), \(W=\sum_t w_t\), and normalized reported costs \(c_t=r_t/B\). Thus \(W>0\).

Let \(c_1<\cdots<c_k\) be the distinct normalized costs, with \(k\le\tau\), and let

\[ F_i=\frac{1}{W}\sum_{t:c_t\le c_i}w_t. \]

In particular, \(F_k=1\). Define the weighted cost quantile function \(c(u)=c_i\) when \(F_{i-1}<u\le F_i\), with \(F_0=0\).

On truthful input, write \(x_*=\mathrm{OPT}(\mu)/W\). The benchmark constraint, divided by \(BW\), is

\[ \sum_t\frac{w_t}{W}(1+c_t)z_t\le1. \]

For any prescribed selected weight fraction \(x\), its minimum possible cost is \(\int_0^x(1+c(u))\,du\). Indeed, if some higher-cost weight is selected while lower-cost weight remains unselected, transferring selected weight from the former to the latter weakly decreases cost. Repeating this exchange selects costs in increasing order, with possible fractional selection at the last cost.

Consequently, \(x_*\) is the unique solution of

\[ \int_0^{x_*}(1+c(u))\,du=1. \]

Existence and uniqueness follow because the integrand is positive, the integral starts at zero, and its value at \(1\) exceeds \(1\). Thus \(0<x_*<1\).

2. A truthful threshold-mixture mechanism

For each reported distribution, solve the finite linear program

\[ y=\max_{\lambda_1,\ldots,\lambda_k\ge0} \left\{ \sum_i\lambda_iF_i: \sum_i\lambda_i\le1,\quad \sum_i\lambda_i(1+c_i)F_i\le1 \right\}. \]

Choose an optimal solution and set \(R=W(1-y)\). For every public pair \((a,d)\) and every positive rational report \(r\), including off-support reports, define

\[ \theta_\nu(a,d,r)=\sum_i\lambda_i\mathbf{1}_{\{r/B\le c_i\}}, \qquad p_\nu(a,d,r)=\frac{B|a|}{R} \sum_i\lambda_i c_i\mathbf{1}_{\{r/B\le c_i\}}. \]

These formulas define a mechanism on every reported input of the stipulated form.

Positive residual and valid probabilities. Since \(\sum_i\lambda_i\le1\), every inclusion probability belongs to \([0,1]\). Moreover,

\[ 1\ge\sum_i\lambda_i(1+c_i)F_i\ge(1+c_1)y. \]

Therefore \(y<1\), so \(R>0\). Summing inclusion probabilities against the input weights gives selected weight \(Wy\), hence the residual computed from the mechanism is exactly \(W-Wy=R\).

Budget feasibility. Its total expected transfer is

\[ \sum_t\nu_t p_t =\frac{BW}{R}\sum_i\lambda_i c_iF_i \le\frac{BW}{R}(1-y)=B. \]

Truthfulness and individual rationality. Fix \(\nu,a,d\), and a true cost \(v\). Reporting \(r\) gives utility

\[ \frac{B|a|}{R} \sum_i\lambda_i(c_i-v/B)\mathbf{1}_{\{r/B\le c_i\}}. \]

At \(r=v\), each positive summand is included and each negative summand is excluded. Any other report can only remove nonnegative summands or add nonpositive summands. Thus truthful reporting maximizes utility. The truthful utility is nonnegative.

This argument uses precisely the stipulated fact that a unilateral report leaves \(\nu\) and \(R\) fixed.

3. Approximation guarantee

We prove \(y\ge(1-1/e)x_*\).

The dual of the threshold-mixture linear program is

\[ y=\min_{\alpha,\gamma\ge0} \left\{ \alpha+\gamma: \alpha(1+c_i)F_i+\gamma\ge F_i \text{ for every }i \right\}. \]

The primal is feasible and bounded, and the dual is feasible, for example at \((\alpha,\gamma)=(1,0)\). Finite-dimensional linear-programming duality therefore supplies an optimal dual solution with objective \(y\).

Because \(y<1\), its \(\alpha\) is positive: if \(\alpha=0\), the constraint at \(F_k=1\) would imply \(\gamma\ge1\). Set

\[ K=\frac1\alpha,\qquad H=\frac{\gamma}{\alpha}. \]

Then \(Ky=1+H\). Since \(y\ge\alpha\) and \(y<1\), we have \(K>1\). The dual constraints imply

\[ c_i\ge K-1-\frac{H}{F_i}. \]

For \(F_{i-1}<u\le F_i\), using \(H\ge0\) and \(F_i\ge u\) gives the pointwise bound

\[ c(u)\ge\max\left\{0,K-1-\frac{H}{u}\right\}. \]

If \(H=0\), integrating yields \(1\ge Kx_*\), so \(x_*\le1/K=y\).

Now suppose \(H>0\), and define \(z=H/(K-1)\). Since \(Ky=1+H<K\), we have \(0<z<1\), and

\[ y=\frac{1+(K-1)z}{K} =z+\frac{1-z}{K}>z. \]

If \(x_*\le z\), then \(x_*<y\). Otherwise, integrate the quantile lower bound over \((z,x_*)\):

\[ 1=\int_0^{x_*}(1+c(u))\,du \ge Kx_*-H-H\log(x_*/z). \]

Substituting \(Ky=1+H\) and writing \(\eta=(K-1)/K<1\) gives

\[ y\ge x_*-\eta z\log(x_*/z). \]

For \(t>1\), the function \(\log(t)/t\) has derivative \((1-\log t)/t^2\), so its maximum is \(1/e\), attained at \(t=e\). Taking \(t=x_*/z\), we obtain

\[ y\ge x_*\left(1-\frac{\eta}{e}\right) \ge x_*\left(1-\frac1e\right). \]

Thus, on every truthful input,

\[ \frac{\mathrm{OPT}(\mu)}{S_M(\mu)} =\frac{x_*}{y}\le\frac{e}{e-1}. \]

4. An upper bound on what any truthful menu can purchase

For the lower bound, consider inputs with one public pair, \(a=1\), total mass \(1\), and \(B=1\). Fix any allowed mechanism.

Let the supported costs be \(v_1<\cdots<v_m\), with masses \(\mu_i\), and define \(F_i=\sum_{\ell\le i}\mu_\ell\). Write its supported allocation and payment entries as \(\theta_i,p_i\), its selected mass as \(S\), and its residual as \(R=1-S>0\). Define \(q_i=Rp_i\).

Adding the truthfulness inequalities between costs \(v_i<v_j\) gives

\[ (v_j-v_i)(\theta_i-\theta_j)\ge0. \]

Hence \(\theta_1\ge\cdots\ge\theta_m\). Define \(\theta_{m+1}=0\) and \(\delta_i=\theta_i-\theta_{i+1}\). Then \(\delta_i\ge0\) and \(\sum_i\delta_i=\theta_1\le1\).

Truthfulness for cost \(v_i\) against report \(v_{i+1}\) gives \(q_i\ge q_{i+1}+v_i\delta_i\). Individual rationality at \(v_m\) gives \(q_m\ge v_m\theta_m\). Induction therefore yields

\[ q_i\ge\sum_{j=i}^m v_j\delta_j. \]

Summing against masses, and using \(S=\sum_j\delta_jF_j\), gives

\[ \sum_i\mu_iq_i\ge\sum_jv_j\delta_jF_j. \]

Budget feasibility implies \(\sum_i\mu_iq_i\le R=1-S\), so necessarily

\[ 1\ge\sum_j\delta_j(1+v_j)F_j. \]

In particular, if an input satisfies

\[ (1+v_j)F_j\ge nF_j-h \quad\text{for every }j, \]

then

\[ 1\ge nS-h\theta_1\ge nS-h, \qquad\text{and therefore}\qquad S\le\frac{1+h}{n}. \]

This bound applies to every allowed mechanism, independently of its off-support behavior.

5. Finite rational instances approaching the bound

Fix any \(q<e/(e-1)\). We construct an input whose approximation ratio exceeds \(q\).

Let \(h_0=1/(e-2)\). Choose \(s_*\) with \(h_0<s_*<eh_0\), sufficiently close to \(eh_0\), that

\[ \frac{s_*}{1+h_0}>q. \]

Define

\[ I(h,s)=\int_h^s(1-h/u)\,du =s-h-h\log(s/h). \]

Since \(I(h_0,eh_0)=h_0(e-2)=1\), and \(I(h_0,s)\) is strictly increasing for \(s>h_0\), we have \(I(h_0,s_*)<1\).

By continuity and density of rational numbers, choose positive rational \(h,s_J\) such that

\[ s_J>h,\qquad \frac{s_J}{1+h}>q,\qquad I(h,s_J)<1. \]

Choose rational \(h<s_0<s_1<\cdots<s_J\), with \(s_0\) sufficiently close to \(h\) and the partition sufficiently fine, that

\[ C=s_0-h+\sum_{j=1}^J(s_j-s_{j-1})(1-h/s_j)<1. \]

This is possible because the sum is a right Riemann sum, and \(C\) converges to \(I(h,s_J)\) as \(s_0\) decreases to \(h\) and the mesh tends to zero.

Choose an integer \(n\) satisfying

\[ n>s_J,\qquad n(1-h/s_0)>1. \]

Use cumulative masses \(F_j=s_j/n\) and corresponding costs

\[ v_j=n-1-\frac{nh}{s_j}, \qquad 0\le j\le J. \]

Add a final type with cumulative mass \(1\) and cost \(v_{\mathrm{tail}}=n-1-h\). All individual masses are positive: they are \(s_0/n\), successive differences \((s_j-s_{j-1})/n\), and \(1-s_J/n\). The costs are positive and strictly increasing.

Every supported cost satisfies

\[ (1+v_j)F_j=nF_j-h, \]

including the tail. Section 4 therefore implies that every allowed mechanism purchases at most \((1+h)/n\).

On the other hand, the benchmark can select all types through cumulative mass \(s_J/n\). Its normalized benchmark cost is exactly \(C<1\). Consequently,

\[ \mathrm{OPT}\ge\frac{s_J}{n}, \qquad \frac{\mathrm{OPT}}{S_M} \ge\frac{s_J}{1+h}>q. \]

If \(S_M=0\), the ratio is infinite, and the conclusion still holds.

The construction uses finite rational inputs. It also works if “binary rational” is interpreted as requiring dyadic values: choose \(h,s_j\) dyadic and \(n\) a power of two, then round each cost upward on a sufficiently fine dyadic grid. The strict cost ordering and benchmark slack \(C<1\) survive sufficiently small rounding, while the inequalities \((1+v_j)F_j\ge nF_j-h\) are preserved.

All types can use the same rational verified datum in the given interval. For any prescribed \(B>0\), multiplying the constructed costs by \(B\) gives the identical normalized argument.

Since \(q<e/(e-1)\) was arbitrary, every allowed mechanism has \(\rho(M)\ge e/(e-1)\).

6. Running time and conclusion

The upper-bound mechanism needs only the distinct costs and their cumulative weighted masses.

Its linear program can be solved by examining the convex hull of the points \((F_i,(1+c_i)F_i)\), together with the origin. Maximizing the first coordinate subject to the second coordinate being at most \(1\) has an optimum at a feasible original point or at an intersection of a segment between two points with the line of second coordinate \(1\).

Enumerating all such pairs takes \(O(\tau^2)\) rational arithmetic operations after sorting. Every candidate uses rational numbers with bit length polynomial in \(L\). Thus preprocessing takes \(O(\tau^2\mathop{\mathrm{poly}}(L))\) bit time. An optimal menu uses at most two nonzero thresholds. No approximation parameter is needed; the mechanism is computed exactly, and \(m=1\).

Combining the bounds proves

\[ \inf_M\rho(M)=\frac{e}{e-1}<2. \]

⟨structured verdict parsed — rendered above⟩

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

The prover’s claim is proved. The argument establishes the exact infimum \(\inf_M\rho(M)=e/(e-1)<2\), supplies a mechanism attaining it, and gives finite rational instances proving the matching lower bound. I found no major or minor mathematical issues.

The definitions \(w_t=\nu_t|a_t|\), \(W=\sum_t w_t\), and \(c_t=r_t/B\) are valid because masses are positive, coefficients are nonzero, and \(B>0\).

Dividing the benchmark constraint by \(BW\) gives exactly the stated normalized constraint. The exchange argument correctly uses selected *weight*, so differing masses and absolute coefficients cause no difficulty. Fractional selection permits filling the cheapest available weight up to any prescribed fraction.

The resulting quantile integral is continuous and strictly increasing. Its value at \(1\) exceeds \(1\), since every cost is positive. Therefore the asserted unique solution \(x_*\in(0,1)\) exists. Cost ties are handled by the quantile blocks.

The linear program is feasible at the zero vector. Its feasible region is closed and bounded by \(\lambda_i\ge0\) and \(\sum_i\lambda_i\le1\), so an optimum exists.

The menu formulas cover every positive rational report, including reports outside the support. They also cover every admissible public pair \((a,d)\); dependence on \(d\) is unnecessary.

The probability bound follows from nonnegative mixture coefficients with total at most \(1\). The estimate
\[ 1\ge(1+c_1)y \]
ensures \(y<1\), because \(c_1>0\). Thus the residual is strictly positive.

Summing the supported allocations gives \(Wy\), confirming that the declared residual \(W(1-y)\) equals the residual required by the task.

The budget calculation is correct: the linear-program constraint gives \(\sum_i\lambda_i c_iF_i\le1-y\), and substitution into the total transfer expression yields the required bound \(B\). All payments are nonnegative.

With the distribution and residual fixed, the displayed utility formula follows directly from the allocation and payment definitions.

Truthful reporting includes every threshold term with positive coefficient \(c_i-v/B\) and excludes every term with negative coefficient. Terms at equality contribute zero. A different report can only remove nonnegative terms or add nonpositive terms.

This proves the required dominant-strategy inequality for arbitrary truthful costs and reports, including off-support reports. It also proves nonnegative truthful utility.

The proof uses precisely the task’s fixed-distribution deviation model; it does not assume that a unilateral deviation changes the aggregate input.

The stated dual has the correct objective, constraints, and nonnegativity restrictions. The primal is feasible and bounded, and the displayed dual feasible point is valid. Finite-dimensional linear-programming duality therefore applies with the hypotheses identified in the write-up.

At an optimal dual solution, \(\alpha=0\) would force \(\gamma\ge1\) through the constraint \(F_k=1\), contradicting \(y<1\). Thus division by \(\alpha\) is justified.

The identities \(Ky=1+H\) and \(K>1\) follow correctly. The passage from the discrete dual constraints to the quantile bound has the correct inequality direction: \(F_i\ge u\) and \(H\ge0\) imply \(-H/F_i\ge-H/u\).

For \(H=0\), integration gives \(x_*\le y\), as claimed.

For \(H>0\), the proof correctly establishes \(0<z<1\) and \(y>z\). Thus the case \(x_*\le z\) already satisfies the desired bound. In the remaining case, the integral calculation is correct:
\[ \int_0^{x_*}\left(1+\max\{0,K-1-H/u\}\right)\,du =Kx_*-H-H\log(x_*/z). \]

Substitution and division by \(K\) give the stated inequality involving \(\eta=(K-1)/K\). The derivative of \(\log(t)/t\), its maximum \(1/e\), and the applicable domain \(t=x_*/z>1\) are all correct.

Consequently \(y\ge(1-1/e)x_*\). Since \(x_*>0\), this also ensures positive selected weight, so the final ratio calculation is legitimate.

The lower bound uses admissible inputs with one public pair, so comparisons between supported costs invoke the task’s truthfulness requirement directly.

Multiplication by the fixed positive residual justifies the normalization \(q_i=Rp_i\). Adding the two truthfulness inequalities gives the stated monotonicity of allocations.

The differences \(\delta_i\) are nonnegative and telescope to \(\theta_1\le1\). The adjacent truthfulness inequality and final individual-rationality inequality have the correct signs and indices. Their iteration yields exactly the payment lower bound written in the proof.

Summation against masses correctly produces the cumulative masses \(F_j\), both in the selected-mass identity and in the transfer lower bound. Budget feasibility then yields
\[ 1\ge\sum_j\delta_j(1+v_j)F_j. \]

Under the stated input inequalities, the deduction \(S\le(1+h)/n\) is valid. The direction of the last inequality uses \(h\ge0\) and \(\theta_1\le1\) correctly.

This argument applies to arbitrary admissible menus; restricting attention to supported report comparisons weakens the available constraints but does not invalidate the necessary bound.

The constants are consistent:
\[ I(h_0,eh_0)=1,\qquad \frac{eh_0}{1+h_0}=\frac{e}{e-1}. \]
Therefore the required choice of \(s_*\) exists for every \(q<e/(e-1)\). Strict inequalities permit the subsequent rational choices by continuity and density.

The Riemann-sum construction is valid. Its integrand is continuous on the relevant positive interval, and the initial contribution tends to zero as \(s_0\) tends to \(h\). Hence the strict benchmark slack \(C<1\) can be achieved with a finite rational partition.

An integer \(n\) satisfying both requirements exists because \(1-h/s_0>0\). The masses are positive and sum to \(1\). The condition \(n(1-h/s_0)>1\) makes the first cost positive; subsequent costs increase. The tail is strictly above the preceding cost because \(n>s_J\), so it too is positive.

The identity \((1+v_j)F_j=nF_j-h\) holds for every constructed support point, including the tail. The benchmark expenditure for selecting through \(s_J/n\) is exactly the displayed \(C\). Thus both the universal upper bound on mechanism selection and the benchmark lower bound are established.

The zero-selection case is handled using the task’s infinite-ratio convention. Since \(q\) can approach the claimed constant from below, the construction proves the lower bound for every mechanism.

The dyadic variant is also justified: sufficiently small upward rounding preserves the required lower-bound inequalities, while finite positive ordering gaps and strict benchmark slack preserve admissibility and benchmark feasibility. Choosing \(n\) as a power of two makes the constructed masses dyadic. A common rational verified datum exists in the stipulated nondegenerate interval, and scaling costs by \(B\) preserves the normalized argument.

The convex-hull reformulation represents exactly the attainable pairs of selected fraction and normalized expenditure. An optimum under expenditure at most \(1\) can be chosen at a feasible original point or at a segment intersection with the expenditure boundary. Including the origin handles mixtures whose coefficients sum to less than \(1\).

Enumerating pairs therefore suffices and produces an optimum with at most two nonzero thresholds. Sorting, rational arithmetic, and candidate comparison have polynomial bit complexity. The stated \(O(\tau^2\operatorname{poly}(L))\) preprocessing bound is consistent with the construction.

No approximation parameter is needed: the irrational constant appears in the guarantee, while the computed menu uses exact rational quantities.

The output fully resolves its assignment. No additional lemma or clarification is required. The polynomial classification concerns the explicit mechanism attaining the optimal worst-case guarantee; the proof does not claim pointwise optimality among all truthful menus on each individual input.

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