← back to the atlas

d4-conf-wine-2014-0012 (d4-conf-wine-2014-0012)

Answer: Deterministic polynomial-time solvable, with \(O(d^2\tau n)\) adaptive queries, query lengths \(O(dn)\), and answer lengths \(O(d(\tau L+n))\).

The anchor (named result in the paper)

Theorem 19 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateThe class Hlin is learnable from O(nd) revealed preference queries. 3These three inputs are irrelevant for learning linear functions, however they will be used to learn SPLC functions in Appendix 5.3.

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

The continuous mirror question, as graded

Let \(\mathcal A_{d,n}\) be the finite set of normalized vectors \(a\in\mathbb Q_{\ge0}^d\), with \(\sum_j a_j=1\) and coordinate bit length at most \(n\). An unknown rational distribution \(\mu\) has support size at most \(\tau\), with masses of bit length at most \(L\). An oracle queried at rational prices \(p\in\mathbb Q_{\ge0}^d\) and budget \(B\in\mathbb Q_{\ge0}\) returns \(D_\mu(p,B)=\sum_a\mu_a b_a(p,B)\), where \(b_a\) is the paper's tie-broken optimal bundle for type \(a\). Can an adaptive algorithm using time and queries polynomial in \(d,\tau,n,L\) and the query bit length output at most \(\tau\) rational type-mass pairs that induce the same \(D_\mu(p,B)\) for every rational \(p,B\)?

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

Let \(m=d\geq1\) be the number of divisible goods, with bundles in \([0,1]^d\). Define \(\mathcal A_{d,n}=\{a\in\mathbb Q_{\geq0}^d:\sum_j a_j=1\}\), restricted to coordinates whose reduced numerators and denominators each have binary length at most \(n\).
For \(a\in\mathcal A_{d,n}\), define \(b_a(p,B)\) by maximizing \(a\cdot x\) over \(x\in[0,1]^d\) with \(p\cdot x\leq B\), then minimizing expenditure among maximizers, then choosing the lexicographically smallest remaining bundle in the fixed coordinate order.
A society is represented by its support: its \(\tau\) distinct positive-mass types and their binary rational masses. Here this representation is hidden; \(\tau\) is the support size, not the number of possible types. Masses sum to \(1\), and each reduced mass numerator and denominator has binary length at most \(L\).
The learner knows \(d,\tau,n,L\) and has only an exact oracle returning \(D_\mu(p,B)=\sum_a\mu_a b_a(p,B)\) for adaptively chosen \(p\in\mathbb Q_{\geq0}^d\) and \(B\in\mathbb Q_{\geq0}\). Oracle answers use binary rational encodings.
The reconstruction problem asks for a distribution \(\widehat\mu\) on at most \(\tau\) types in \(\mathcal A_{d,n}\), with positive rational masses summing to \(1\), such that \(D_{\widehat\mu}(p,B)=D_\mu(p,B)\) for every rational nonnegative \((p,B)\).

Does this exact reconstruction problem admit a deterministic adaptive algorithm with time, query count, and query bit lengths polynomial in \(m=d,\tau,n,L\), or is it NP-hard in this oracle model? Account for binary query and answer processing in the running time.

For a single normalized rational linear-utility buyer, exact learning uses \(O(nd)\) revealed-preference queries ([Balcan et al.](https://arxiv.org/pdf/1407.7937v1)).
Polynomial-time aggregate-demand learning is known for linear Fisher markets with fixed buyer budgets and bundles in \(\mathbb R_{\geq0}^d\); that model differs from the capped bundles and query-selected common budget here ([Bei et al.](https://www.microsoft.com/en-us/research/wp-content/uploads/2016/06/aaai16_learnmarket.pdf)).

Modeling choices made when packaging the task

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

Result

The reconstruction problem admits a deterministic adaptive algorithm with running time polynomial in \(d,\tau,n,L\). It uses \(O(d^2\tau n)\) oracle queries, each of binary length \(O(dn)\). The canonical binary encoding of every answer used by the algorithm has length \(O(d(\tau L+n))\).

In fact, the algorithm recovers the original normalized types and their masses exactly, which is stronger than demand-equivalent reconstruction.

For \(d=1\), the only normalized type is \((1)\), so the answer is immediate. Henceforth assume \(d\geq2\).

1. Small-budget queries reveal cumulative masses

We first establish precisely what an individual buyer purchases in the queries we will use.

Lemma 1. Suppose every price satisfies \(p_i\geq1\), and the common budget is \(B=1/2\). Let \(h\) be the largest coordinate index maximizing \(a_i/p_i\). Then

\(b_a(p,1/2)=\frac{1}{2p_h}e_h.\)

Proof. Every feasible bundle satisfies \(x_i\leq1/(2p_i)\leq1/2\), so the upper bounds \(x_i\leq1\) impose no additional restriction.

Write \(c=\max_i a_i/p_i\). Normalization implies \(c>0\). For every feasible bundle,

\(a\cdot x=\sum_i\frac{a_i}{p_i}p_ix_i\leq c\sum_i p_ix_i\leq c/2.\)

Purchasing \(1/(2p_h)\) units of good \(h\) attains this bound. Equality requires spending the entire budget exclusively on goods maximizing \(a_i/p_i\). Thus all utility maximizers have the same expenditure.

Among these maximizers, the lexicographically smallest bundle places all expenditure on the largest maximizing index: each earlier coordinate can be set to zero, and lexicographic minimization requires doing so. This proves the formula. \(\square\)

This small-budget observation also underlies the single-buyer algorithm of [Balcan et al.](https://arxiv.org/pdf/1407.7937v1). We will use it to obtain cumulative-mass queries for a sparse distribution.

2. A finite grid separates every possible utility ratio

Set

\(Q=2^{2n},\qquad K=4n+3,\qquad M=2^{K+n-1}.\)

If \(a_j>0\), define \(r_k=a_k/a_j\) for \(k\neq j\). Each such ratio satisfies

\(0\leq r_k<2^n,\)

and its reduced denominator is less than \(Q\). Indeed, each positive coordinate is greater than \(2^{-n}\), and each coordinate is at most \(1\). Moreover, writing the coordinates as reduced fractions, the denominator of their ratio before reduction is a product of two positive integers less than \(2^n\).

For integers \(z\in\{0,\ldots,M\}\), define

\(t_z=\frac{2z+1}{2^K}.\)

These thresholds have three useful properties.

\(2^{1-K}<Q^{-2}\).

Define the label of a ratio by

\(\ell(r)=\min\{z\in\{0,\ldots,M\}:r<t_z\}.\)

Consequently, the label uniquely determines every possible ratio.

Fix a reference good \(j\), and index the other goods in their original coordinate order. For a label vector \(z=(z_k)_{k\neq j}\), make the query

\(p_j=2^K,\qquad p_k=2z_k+1\ \text{for }k\neq j,\qquad B=1/2.\)

All prices are positive integers. For a type with \(a_j>0\),

\(\frac{a_k}{p_k}<\frac{a_j}{p_j}\quad\Longleftrightarrow\quad\frac{a_k}{a_j}<t_{z_k}.\)

Equality is impossible by the threshold construction. Hence good \(j\) is the unique maximizer exactly when all these inequalities hold. A type with \(a_j=0\) never purchases good \(j\), since some coordinate has positive utility.

Lemma 1 therefore gives

\(F_j(z):=2^{K+1}D_\mu(p,1/2)=\sum_{a:a_j>0}\mu_a\,\mathbf 1\{\ell(a_k/a_j)\leq z_k\text{ for every }k\neq j\}.\)

Thus one demand query implements one lower-orthant cumulative-mass query for the label vectors of types with \(a_j>0\).

For a fixed reference \(j\), distinct normalized types yield distinct ratio vectors: the ratios determine the type through

\(a_j=\frac{1}{1+\sum_{k\neq j}r_k},\qquad a_k=r_ka_j.\)

Since labels uniquely determine ratios, distinct types also yield distinct label vectors. Therefore \(F_j\) represents a positive measure with at most \(\tau\) distinct atoms, whose masses are precisely the corresponding original masses.

3. Sparse positive measures can be recovered from cumulative queries

We now prove the reconstruction procedure needed for each reference good.

Lemma 2. Let \(\nu\) be a positive measure supported on at most \(s\) points of \(\{0,\ldots,M\}^k\). Given exact queries

\(F(z)=\nu(\{y:y_i\leq z_i\text{ for all }i\}),\)

one can recover every atom and its mass deterministically using at most

\(1+s\bigl(k\lceil\log_2(M+1)\rceil+1\bigr)\)

queries.

Proof. First query the total mass \(T=F(M,\ldots,M)\).

Suppose some atoms \((y^{(u)},w_u)\) have already been recovered correctly. Their contributions can be subtracted to evaluate

\(R(z)=F(z)-\sum_u w_u\,\mathbf 1\{y^{(u)}\leq z\}.\)

Here vector inequalities mean coordinatewise inequalities. By the induction hypothesis, \(R\) is exactly the cumulative function of the remaining positive measure.

If the recovered masses sum to \(T\), reconstruction is finished. Otherwise, locate the lexicographically smallest remaining support point \(v\), coordinate by coordinate.

Choose \(v_1\) as the smallest integer \(t\) such that

\(R(t,M,\ldots,M)>0.\)

This predicate is monotone in \(t\), so binary search suffices. Having chosen \(v_1,\ldots,v_{h-1}\), choose \(v_h\) as the smallest integer \(t\) such that

\(R(v_1,\ldots,v_{h-1},t,M,\ldots,M)>0.\)

To justify this search, induct on \(h\). After the preceding choices, every remaining support point satisfying the preceding upper bounds must have prefix exactly \((v_1,\ldots,v_{h-1})\): a smaller coordinate at the first differing position would contradict an earlier minimum. Thus the new search selects the minimum next coordinate among points with that exact prefix. Its predicate is positive at \(t=M\).

At the end, \(v\) is a remaining support point. Moreover, it is the only remaining support point dominated coordinatewise by \(v\). Indeed, any different such point would have a smaller coordinate at its first differing position, contradicting the corresponding search minimum. Therefore its exact mass is

\(w=R(v)>0.\)

Record \((v,w)\) and repeat. Each iteration removes one original atom, so there are at most \(s\) iterations. The stated query bound follows. \(\square\)

Positivity is essential here: a positive cumulative value certifies the existence of a remaining atom. The procedure uses only cumulative queries and subtraction of already recovered atoms.

4. Recovering exact ratios and the society

Apply Lemma 2 to each \(F_j\), with \(k=d-1\) and \(s\leq\tau\). It remains to decode each recovered label.

If \(\ell(r)=0\), then \(r=0\): any positive rational with denominator less than \(Q\) is greater than \(1/Q>t_0\).

For a positive label \(z\), the ratio satisfies

\(t_{z-1}<r<t_z.\)

Let the midpoint of this interval be

\(c_z=\frac{2z}{2^K}.\)

Writing \(r=u/v\) in lowest terms, we have \(v<Q\) and

\(\left|r-c_z\right|<2^{-K}=\frac{1}{8Q^2}<\frac{1}{2v^2}.\)

We use Legendre’s continued-fraction theorem: if a reduced rational \(u/v\), with \(v>0\), satisfies \(\left|\xi-u/v\right|<1/(2v^2)\), then it is a convergent of the continued fraction of \(\xi\). This statement applies to rational \(\xi\) as well; see the [formal theorem in Mathlib](https://leanprover-community.github.io/mathlib_docs/number_theory/diophantine_approximation.html#real.exists_rat_eq_convergent).

All its hypotheses have just been checked for \(\xi=c_z\). Compute the finite continued fraction of \(c_z\) by the Euclidean algorithm, and select the convergent with denominator less than \(Q\) lying in \((t_{z-1},t_z)\). Such a convergent exists by the theorem and is unique by the rational-separation bound. Since \(c_z\) has \(O(n)\)-bit numerator and denominator, this decoding takes polynomial time in \(n\).

Decode all ratios of each recovered atom, then normalize using

\(a_j=\frac{1}{1+\sum_{k\neq j}r_k},\qquad a_k=r_ka_j.\)

The injectivity proved in Section 2 guarantees that this recovers exactly one original type, with its original mass.

Finally, take the union of the recovered type lists over all reference goods. When a type occurs in several lists, retain one copy with its mass; do not add these duplicate masses. Each list recovers the same original mass for that type.

Every normalized type has at least one positive coordinate, so every original type appears in at least one list. Consequently, this union is exactly the original support with exactly the original masses. It contains \(\tau\) types, belongs to \(\mathcal A_{d,n}\), and has positive masses summing to \(1\). In particular,

\(D_{\widehat\mu}(p,B)=D_\mu(p,B)\)

for every rational nonnegative query, including queries with zero prices or binding caps.

5. Binary running time

Because \(\log_2 M=5n+2\), the total number of demand queries is at most

\(d\left[1+\tau\left((d-1)(5n+3)+1\right)\right]=O(d^2\tau n).\)

Every queried price has \(O(n)\) bits, and the budget is always \(1/2\). Thus each complete query has length \(O(dn)\).

To bound answer lengths, let \(H\) be the product of the reduced denominators of the original masses. Then

\(\log_2 H\leq\tau L.\)

By Lemma 1, for every query used here and every coordinate \(i\),

\(D_{\mu,i}(p,1/2)=\frac{1}{2p_i}\sum_{a:h(a,p)=i}\mu_a.\)

The subset sum has denominator dividing \(H\). Therefore the reduced denominator of this demand coordinate divides \(2p_iH\), and its numerator has no greater binary length, since the coordinate lies in \([0,1]\). Each coordinate answer consequently has \(O(\tau L+n)\) bits; the complete answer has \(O(d(\tau L+n))\) bits.

Cumulative values and residual values are sums of subsets of original masses, so their reduced denominators also divide \(H\). Reducing fractions after arithmetic therefore keeps their bit lengths polynomial. Evaluating a residual requires comparing at most \(\tau\) recovered label vectors and subtracting their masses. Continued-fraction decoding uses polynomial time, and normalization involves only \(d\) rationals with \(O(n)\)-bit components, hence polynomial-size intermediate arithmetic.

These bounds include reading and processing every coordinate of every oracle answer. They use the usual canonical binary rational encoding; arbitrary redundant padding would make a bit-time guarantee ill-posed independently of reconstruction.

The algorithm is therefore deterministic and polynomial in \(m=d,\tau,n,L\) in the stated exact-oracle model.

⟨structured verdict parsed — rendered above⟩

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

Verification report

Verdict: proved with minor gaps. The argument establishes deterministic polynomial-time exact reconstruction under the natural convention of canonical binary rational oracle answers. The mathematical construction is sound. One displayed formula omits a coordinate subscript, and the encoding convention should be identified explicitly as an assumption about the oracle interface.

No major issue or missing mathematical lemma was found.

1. Individual demand in the selected queries

Lemma 1 correctly accounts for all three stages of the buyer’s selection rule.

The conclusion also covers types with some zero utility coordinates.

The \(d=1\) case is correctly handled: the promised society necessarily consists of the sole normalized type with mass one.

2. Ratio bounds and threshold separation

The ratio bounds are correct under the stated binary-length restriction.

Every positive coordinate exceeds \(2^{-n}\), and every coordinate is at most one. Hence \(0\leq a_k/a_j<2^n\) when \(a_j>0\). The unreduced denominator of a ratio is a product of a coordinate denominator and a positive coordinate numerator, each less than \(2^n\), so its reduced denominator is less than \(Q=2^{2n}\).

The threshold construction passes all checks:

Thus the labels are well-defined and injective on the possible ratios. The exponentially large grid does not require enumeration; its indices have polynomial binary length.

3. Conversion to cumulative-mass queries

The price comparison is correct. A type with \(a_j>0\) purchases good \(j\) precisely when all its ratio labels satisfy the corresponding upper bounds. There are no ties involving good \(j\). A type with \(a_j=0\) cannot purchase it because normalization guarantees another coordinate with positive utility.

Minor issue — scalar/vector mismatch. The displayed definition of \(F_j\) uses \(2^{K+1}D_\mu(p,1/2)\), which is a vector, while its right-hand side is a scalar mass.

Minimum clarification: specify that the expression uses coordinate \(j\) of the oracle answer. The preceding argument determines this interpretation unambiguously, so no new mathematics is needed.

With that interpretation, the cumulative-mass identity is correct.

The normalization formulas correctly show that ratio vectors determine normalized types. Label injectivity therefore ensures that distinct types remain distinct atoms for each reference good where they have positive utility.

4. Sparse recovery from cumulative queries

Lemma 2 is valid.

Subtracting correctly recovered atoms leaves exactly the cumulative function of the remaining positive measure. Positivity makes the predicate \(R(z)>0\) an exact existence test.

The coordinate-search induction is sufficient: among remaining points satisfying the already selected upper bounds, any point with a smaller coordinate at its first differing position would contradict a previous minimum. Consequently, those bounds isolate the selected prefix.

At the completed vector \(v\), no different remaining support point can be dominated coordinatewise by \(v\). Hence \(R(v)\) is exactly the mass of that atom, rather than a sum of several unresolved masses.

Termination follows from removing one genuine atom per iteration. An empty reference-good measure is handled by the initial total-mass query. Binary search over \(M+1\) possibilities gives the stated query bound; the additional query per atom suffices to obtain its mass.

No assumption about a separation between positive masses is needed because comparisons are exact.

5. Exact ratio decoding

The zero-label case is correct: every positive reduced rational with denominator less than \(Q\) exceeds \(1/Q>t_0\).

For a positive label, threshold non-equality gives the claimed open interval. Its midpoint and approximation bound are correctly computed:
\(\lvert r-c_z\rvert<2^{-K}=1/(8Q^2)<1/(2v^2)\).

The invoked Legendre theorem is stated precisely, and its hypotheses are satisfied: the ratio is reduced, its denominator is positive, and the approximation inequality is strict. The cited theorem allows arbitrary real inputs, including rational inputs; there is no missing irrationality hypothesis. This is confirmed by the [Mathlib theorem cited by the prover](https://leanprover-community.github.io/mathlib_docs/number_theory/diophantine_approximation.html#real.exists_rat_eq_convergent).

Existence of the required convergent follows from that theorem. Uniqueness follows from the already established denominator separation and interval width. Computing the finite continued fraction and checking its convergents takes polynomial time in the binary lengths involved.

No decoding gap remains.

6. Reconstruction of the society

Normalization recovers the original type associated with each atom, and Lemma 2 recovers its original mass.

Taking the union over reference goods is valid because every normalized type has a positive coordinate. Retaining one copy of a repeated type, without adding its repeated masses, is essential and is explicitly prescribed.

Therefore the resulting list is exactly the original support and masses. It satisfies the membership, positivity, normalization, and support-size requirements. Equality of demand on every allowed query follows from equality of the distributions themselves; separate analysis of zero prices or binding caps is unnecessary.

7. Binary complexity

The complexity calculations are correct:

The argument therefore accounts for reading every coordinate of each canonical oracle answer.

Minor issue — oracle encoding convention. The task says “binary rational encodings,” whereas the answer-length proof assumes canonical encodings. The prover explicitly acknowledges this convention, which is the natural intended interpretation. However, a bound on reduced numerator and denominator lengths does not bound an arbitrarily padded transmitted representation.

Minimum clarification: state at the outset that oracle answers use canonical reduced binary rational encodings, or another encoding with polynomially bounded overhead. This is an interface clarification, not a mathematical reconstruction gap.

Actionable feedback

Only two expositional changes are needed:

The proof does not need a replacement argument or an additional mathematical lemma.

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