← back to the atlas

d4-conf-ijcai-2018-0116 (d4-conf-ijcai-2018-0116)

Answer: —

The anchor (named result in the paper)

Theorem 3.11 — class: hardness

PDF text-layer excerpt — equations and symbol order may be approximateAny protocol for the proportional chore division makes at least Ω(n log n) queries in the worst case.

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

The continuous mirror question, as graded

Given a rational mass profile \(\mu\) over \(\tau\) complete valuation types, a cohort scale \(N\) with \(N\mu_t\in\mathbb{Z}\), and Robertson–Webb EVAL and CUT oracles for each type valuation \(v_t\), what is the optimal worst-case query complexity of returning a partition \((X_{t,j})\) of \([0,1]\) into one bundle for each of the \(N\mu_t\) agents of type \(t\), such that \(v_t(X_{t,j})\le 1/N\) for every agent?

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

A society is given by its support: a list of \(\tau\) complete valuation types with positive binary-rational masses \(\mu_t\), where \(\sum_t\mu_t=1\); \(\tau\) counts supported types, not possible types. Each type specifies a nonnegative atomless additive measure \(v_t\) on \([0,1]\), normalized by \(v_t([0,1])=1\), accessible only through Robertson–Webb EVAL and CUT oracles.
The input also contains a binary integer \(N\ge2\) such that \(k_t=N\mu_t\in\mathbb Z_{>0}\); \(L\) is the total bit length of the masses and \(N\). There is no finite item parameter \(m\).
A deterministic protocol must return an explicit partition \((X_{t,j})_{t,\,1\le j\le k_t}\) of \([0,1]\), with every bundle a finite union of intervals and \(v_t(X_{t,j})\le1/N\). Shared endpoints may be assigned arbitrarily. Output interval endpoints must belong to \(\{0,1\}\) or have been returned by CUT queries; when a CUT answer is nonunique, the oracle may return any valid answer.
Complexity counts oracle calls, with exact real answers; arithmetic and output time are not charged.

What is the asymptotically optimal deterministic worst-case Robertson–Webb query complexity of this allocation problem as a function of \(N\), \(\tau\), and \(L\)?

For an explicit list of \(N\) agents, proportional chore division requires \(\Omega(N\log N)\) queries, and an \(O(N\log N)\) protocol is known. [Farhadi–Hajiaghayi](https://www.ijcai.org/proceedings/2018/0031.pdf)
No result settling the dependence on support size for this precise input and individual-bundle output model was located.

Modeling choices made when packaging the task

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

Partial solution and new bounds

Let $\mathbf{k}=(k_1,\ldots,k_\tau)$ be any fixed admissible multiplicity vector, so that
$$ k_t\in\mathbb Z_{>0}, \qquad \sum_{t=1}^{\tau}k_t=N, \qquad \mu_t=\frac{k_t}{N}. $$
Write $Q^*(\mathbf{k})$ for the optimal deterministic worst-case query complexity for these masses, with exactly $\tau$ distinct supported valuation measures.

Define
$$ B(\mathbf{k}) = \max_{\varnothing\ne H\subseteq\{1,\ldots,\tau\}} \frac{\sum_{t\in H}k_t}{\max_{t\in H}k_t}. $$

I prove the following bounds:
$$ \boxed{ \Omega\!\left(N+B(\mathbf{k})\log N\right) \ \le\ Q^*(\mathbf{k}) \ \le\ O(N+\tau\log\tau). } $$

The lower bound is new relative to the notes. It repairs the distinct-type issue and applies to unequal multiplicities. In particular:

$$ Q^*(\mathbf{k}) = \Omega\!\left( N+\frac{\tau\log N}{1+\log(N/\tau)} \right). $$

A matching bound for every mass vector, and a complete statement conditioned on exact $L$, remain open here. All unqualified logarithms below have base two.

1. Uniform upper bound

We first establish the upper bound independently of the notes.

Represent type $t$ by $k_t$ labeled conceptual copies. A recursive node consists of an interval $I=[a,b]$ and a multiset $S$ containing $n$ copies. Maintain the invariant
$$ v_t(I)\le\frac nN $$
for every type represented in $S$.

At the root, $n=N$ and $I=[0,1]$, so normalization establishes the invariant. A node containing one copy assigns its interval to that copy.

For a node with $n\ge2$, put $h=\lfloor n/2\rfloor$. For every represented type $t$, query
$$ s_t=\operatorname{EVAL}_t(a,b). $$
If $s_t>0$, query
$$ c_t=\operatorname{CUT}_t\!\left(a,\frac hn s_t\right). $$
If $s_t=0$, set $c_t=a$.

Atomlessness makes the cumulative interval value continuous. When $s_t>0$, the requested value lies strictly between zero and $s_t$, so a valid cut exists and every valid answer satisfies $a<c_t<b$.

Order types by decreasing $c_t$, breaking ties deterministically, and place each type’s copies consecutively. Let $x$ be the mark of the copy in position $h$. Assign the first $h$ copies to $[a,x]$ and the others to $[x,b]$.

For a positive-value type represented on the left, $c_t\ge x$, hence
$$ v_t([a,x]) \le v_t([a,c_t]) =\frac hn s_t \le\frac hN. $$
For a positive-value type represented on the right, $c_t\le x$, hence
$$ v_t([x,b]) =s_t-v_t([a,x]) \le s_t-v_t([a,c_t]) =\frac{n-h}{n}s_t \le\frac{n-h}{N}. $$
These inequalities also hold when $s_t=0$, by nonnegativity. Thus both children satisfy the invariant.

Recursion terminates with $N$ leaves. Each leaf owner values its interval at most $1/N$. Subdivision partitions the parent up to endpoints, which have zero value. Every subdivision endpoint is a CUT answer or an inherited permitted endpoint. This also proves correctness for arbitrary valid choices of nonunique CUT answers.

For the query count, let $I_d$ be the number of type incidences among nodes at depth $d$. Because copies of each type are consecutive, at most one type occurs in both children of any split. Consequently,
$$ I_0=\tau, \qquad I_{d+1}\le I_d+2^d, \qquad I_d\le\tau+2^d-1. $$
The depth is at most $D=\lceil\log N\rceil$. Each internal incidence costs at most two queries, so
$$ Q \le2\sum_{d=0}^{D-1}I_d =O(\tau\log N+N). $$
Since $\tau\le N$,
$$ \tau\log N =\tau\log\tau+\tau\log(N/\tau) \le\tau\log\tau+\frac{N}{\ln2}. $$
Therefore
$$ Q=O(N+\tau\log\tau). $$
Processing the masses requires no oracle calls, so this upper bound has no additional dependence on $L$.

2. Endpoint lower bound

For any admissible masses, choose distinct numbers
$$ \varepsilon_t=\frac{t}{2N(\tau+1)} $$
and define valuation densities
$$ f_t(x)=1+\varepsilon_t(2x-1). $$
They are positive, normalized, and pairwise distinct. Moreover,
$$ f_t(x)>1-\frac1{2N}. $$

If $X$ is a permissible bundle for type $t$, then
$$ \frac1N\ge v_t(X) \ge\left(1-\frac1{2N}\right)|X|, $$
where $|X|$ denotes Lebesgue measure. Thus
$$ |X|\le\frac1{N-\frac12}. $$

Suppose the protocol obtains $r$ distinct interior CUT endpoints. These endpoints divide the interval into $r+1$ elementary open intervals. Ownership cannot change inside one such interval, because every output endpoint must be permitted. Each elementary interval therefore lies in one bundle and has length at most $1/(N-\frac12)$.

Their lengths sum to one, giving
$$ 1\le\frac{r+1}{N-\frac12}. $$
Integrality implies $r+1\ge N$, and hence
$$ \boxed{Q\ge r\ge N-1.} $$

For $\tau=1$, this is exact: the cumulative cuts at levels $j/N$, for $1\le j<N$, suffice.

3. Removing the distinct-type obstruction

Call a measure full-support if every nonempty open subinterval has positive value.

Finite-transcript perturbation lemma.
Given finitely many normalized, atomless, full-support measures $v_1,\ldots,v_\tau$ and a finite set $P\subseteq[0,1]$ containing $0,1$, there exist pairwise distinct measures $\widetilde v_1,\ldots,\widetilde v_\tau$ with the same properties such that
$$ \widetilde v_t([a,b])=v_t([a,b]) \qquad \text{for all }a,b\in P,\ a\le b. $$

Proof. Choose consecutive points $a<b$ of $P$. For a given measure $v_t$, continuity and full support provide $c\in(a,b)$ such that
$$ v_t([a,c])=v_t([c,b])=\frac12v_t([a,b])>0. $$
For $\lambda\in(-1,1)$, multiply the measure by $1+\lambda$ on $(a,c)$ and by $1-\lambda$ on $(c,b)$, leaving it unchanged elsewhere.

The two changes cancel, so normalization and the value of every interval with endpoints in $P$ are preserved. The multiplier is positive, preserving atomlessness and full support. Different $\lambda$ give different measures.

Choose the modified measures successively. At each step, only finitely many choices are forbidden by equality with previously chosen measures, whereas infinitely many choices are available. The resulting measures are pairwise distinct. $\square$

Now let a protocol be correct and bounded by $Q$ queries on distinct supported measures with fixed masses. Run its deterministic instructions on an arbitrary labeled family of full-support measures, allowing repetitions.

Every finite query transcript can be realized by distinct measures: apply the lemma with $P$ containing all query coordinates and CUT answers. EVAL answers are preserved. Full support makes valid CUT answers unique, and their defining equalities are preserved. Failed CUT queries remain failed because the remaining value to $1$ is preserved.

The run therefore cannot issue a $(Q+1)$st query. It also cannot enter a nonterminating computation after a finite transcript: the same transcript is realized on an admissible distinct instance, on which the computation must terminate.

At termination, include all output endpoints in $P$. The endpoint restriction makes this a finite set of previously available coordinates. Perturbation preserves every output-bundle value, as well as the output itself. Correctness on the distinct perturbed instance therefore proves correctness on the original labeled family.

Thus a bounded protocol for distinct types also works, with the same query bound, on labeled full-support measures that repeat. This is the extension needed below.

4. The published adversary used in the lower bound

I use the following property of Farhadi–Hajiaghayi’s balanced-value-tree adversary.

For a sufficiently large power of three $n$, its valuations are normalized, atomless, full-support, and have positive constant density on each of $n$ equal grid intervals, with density at most $2$. Put
$$ M(n)=\left\lfloor\frac{(\ln n)/6-1}{2}\right\rfloor. $$
The adversary maintains a realizable transcript for its first $M(n)$ queries. During this phase, an EVAL query whose endpoints lie strictly inside one grid interval reveals that interval and its density is less than $1/2$. This follows from the revealed-path invariant and the heavy-edge requirement for rich or critical leaves in Lemmas 4.5 and 4.7. [Farhadi–Hajiaghayi, Section 4](https://www.ijcai.org/proceedings/2018/0031.pdf)

After this phase, fix any consistent valuation and answer subsequent queries from it.

Independent copies of this adversary can be run on separate oracles. Interleaving queries does not change any copy’s local query count or invariant. Thus an interior EVAL query certifying grid-interval density at least $1/2$ requires more than $M(n)$ queries to that particular oracle.

This simultaneous adversary property is essential; a single-oracle worst-case lower bound alone would not justify summing lower bounds across adaptively selected types.

5. A lower bound for any subset of types

Fix a nonempty subset $H$ of type labels and write
$$ K=\sum_{t\in H}k_t, \qquad a=\max_{t\in H}k_t. $$
I prove
$$ Q^*(\mathbf{k})=\Omega\!\left(\frac Ka\log N\right). $$

It suffices to consider large $N$. Choose
$$ n=3^{\lfloor\log_3N\rfloor}, $$
so that $N/3<n\le N$ and $M(n)=\Omega(\log N)$.

For every $t\in H$, independently run the adversary of Section 4 on a valuation $w_t$. Let
$$ F_t(x)=w_t([0,x]), \qquad G_t=F_t^{-1}. $$
Full support and atomlessness make $F_t$ a continuous strictly increasing bijection.

Give the allocation protocol the valuation $u_t$ defined by
$$ u_t([x,y])=G_t(y)-G_t(x). $$
For $t\notin H$, give it the uniform valuation. These are all normalized, atomless, full-support measures. Repetitions are allowed by Section 3.

5.1 Simulating the allocation queries

An EVAL query to $u_t$ is answered using two CUT queries to $w_t$:
$$ u_t([x,y]) =\operatorname{CUT}_{w_t}(0,y) -\operatorname{CUT}_{w_t}(0,x). $$

For $\operatorname{CUT}_{u_t}(x,r)$, first obtain $z=G_t(x)$. If $z+r>1$, the query has no answer. Otherwise its answer is
$$ F_t(z+r)=\operatorname{EVAL}_{w_t}(0,z+r). $$
Indeed,
$$ u_t([x,F_t(z+r)]) =G_t(F_t(z+r))-G_t(x) =r. $$
Each allocation query therefore costs at most two underlying queries. Queries to uniform filler types require no underlying oracle calls.

Because $w_t([p,q])\le2(q-p)$,
$$ y-x =w_t([G_t(x),G_t(y)]) \le2\bigl(G_t(y)-G_t(x)\bigr). $$
Hence
$$ u_t([x,y])\ge\frac{y-x}{2}. $$
The same inequality holds for finite unions. Every permissible bundle belonging to a type in $H$ consequently has length at most $2/N$.

5.2 Many hard types receive a sufficiently long bundle

Uniform filler types collectively receive length at most
$$ \sum_{t\notin H}\frac{k_t}{N}=1-\frac KN. $$
Thus the $K$ bundles belonging to types in $H$ have total length at least $K/N$.

Let $\ell$ be the number of these bundles having length at least $1/(2N)$. Every hard bundle has length at most $2/N$, so
$$ \frac KN \le \frac{K-\ell}{2N}+\frac{2\ell}{N}. $$
Therefore $\ell\ge K/3$.

Each type has at most $a$ bundles. Consequently at least
$$ R\ge\frac{K}{3a} $$
different types in $H$ have a bundle of length at least $1/(2N)$. Select one such bundle for each of these types.

5.3 Extracting a dense grid interval

For a selected bundle $X$ owned by type $t$, map each interval $[p,q]$ of $X$ to
$$ [G_t(p),G_t(q)], $$
and call the resulting finite union $P$. Obtain its endpoints through CUT queries to $w_t$.

Strict monotonicity preserves disjointness of interval interiors, and
$$ |P|=u_t(X)\le\frac1N, \qquad w_t(P)=|X|\ge\frac1{2N}. $$
Thus $P$ has average density at least $1/2$. Some positive-length component $J$ of $P$ has density at least $1/2$.

These component densities are already known: if $J=[G_t(p),G_t(q)]$, then
$$ w_t(J)=q-p. $$

Since $|J|\le1/N\le1/n$, it intersects the interiors of at most two grid intervals. The density of $w_t$ is constant on each grid interval, so at least one intersected grid interval has density at least $1/2$. Query the middle third of each candidate grid interval. At least one answer certifies density at least $1/2$.

By Section 4, each of the $R$ selected underlying oracles has now received more than $M(n)$ queries.

5.4 Total query accounting

Suppose the allocation protocol uses $Q$ queries and obtains $r$ distinct interior CUT endpoints, with $r\le Q$. Its output can be represented, after discarding irrelevant isolated endpoints, by assigning each of the $r+1$ elementary open intervals to one bundle.

Therefore the total number $C$ of positive-length components across the selected bundles satisfies
$$ C\le r+1\le Q+1. $$
Also $R\le C$.

Simulating the allocation uses at most $2Q$ underlying queries. Mapping selected components costs at most $2C$ queries; testing candidate grid intervals costs at most $2R$. The total is at most
$$ 2Q+2C+2R\le6Q+4. $$
On the other hand, it is at least $R\,M(n)$. Hence
$$ 6Q+4 \ge R\,M(n) \ge\frac{K}{3a}M(n). $$
Since $M(n)=\Omega(\log N)$, this proves the claimed asymptotic lower bound.

Taking the maximum over $H$ and combining with the endpoint lower bound yields
$$ \boxed{ Q^*(\mathbf{k}) = \Omega\!\left(N+B(\mathbf{k})\log N\right). } $$
The finitely bounded range of smaller $N$ is covered by the endpoint bound, since $B(\mathbf{k})\le\tau\le N$ and $\log N$ is bounded in that range.

6. Consequences for unequal multiplicities

Taking $H$ to be all types gives
$$ B(\mathbf{k})\ge\frac{N}{k_{\max}}, \qquad k_{\max}=\max_t k_t. $$
Thus, whenever $k_{\max}\le C N/\tau$ for a fixed constant $C$,
$$ Q^*(\mathbf{k}) =\Omega(N+\tau\log N). $$
Together with the upper bound and $\log N\ge\log\tau$, this gives
$$ \boxed{ Q^*(\mathbf{k})=\Theta(N+\tau\log\tau). } $$
Equal multiplicities are included, but divisibility by $\tau$ is unnecessary.

There is also a stronger general lower bound than $\Omega(N)$. Put $A=N/\tau$. At least $\tau/2$ types satisfy $k_t\le2A$; otherwise their multiplicities alone would sum to more than $N$.

Partition these types into bins
$$ 2^j\le k_t<2^{j+1}. $$
There are at most
$$ d=1+\lfloor\log(2A)\rfloor $$
bins. One contains at least $\tau/(2d)$ types. Taking that bin as $H$ gives
$$ B(\mathbf{k})\ge\frac{\tau}{4d}. $$
Consequently,
$$ \boxed{ Q^*(\mathbf{k}) = \Omega\!\left( N+\frac{\tau\log N}{1+\log(N/\tau)} \right). } $$

In the previously unsettled regime $N<\tau\log\tau$, this implies, for sufficiently large $\tau$,
$$ Q^*(\mathbf{k}) = \Omega\!\left( N+\frac{\tau\log\tau}{1+\log\log\tau} \right). $$
Thus the remaining gap for arbitrary masses is at most a factor of order $1+\log\log\tau$.

7. Worst case over masses and the role of encoding

Without conditioning on exact $L$, balanced admissible masses establish the matching worst-case lower bound for every feasible pair $(N,\tau)$.

If arbitrary binary-encoded rational masses are allowed, choose positive integers $k_t$ differing by at most one and summing to $N$. Then
$$ k_{\max}=\left\lceil\frac N\tau\right\rceil \le\frac{2N}{\tau}, $$
so Section 6 applies.

For the next feasibility statement, interpret “binary-rational” as dyadic. Write
$$ N=2^a s, \qquad s\text{ odd}. $$
If $\mu_t$ is dyadic and $N\mu_t$ is integral, its reduced denominator divides $2^a$. Thus
$$ \ell_t=2^a\mu_t $$
is a positive integer, and $\sum_t\ell_t=2^a$. Feasibility therefore requires $\tau\le2^a$.

Conversely, whenever $\tau\le2^a$, choose positive integers $\ell_t$ differing by at most one and summing to $2^a$, and put
$$ \mu_t=\frac{\ell_t}{2^a}, \qquad k_t=s\ell_t. $$
These masses are admissible and satisfy
$$ k_{\max} =s\left\lceil\frac{2^a}{\tau}\right\rceil \le\frac{2N}{\tau}. $$
Thus under either interpretation,
$$ \boxed{ \text{worst case over admissible masses at fixed feasible }(N,\tau) = \Theta(N+\tau\log\tau). } $$

Under ordinary binary numerator/denominator encoding, these balanced descriptions have length $O(\tau\log N+\log N)$.

This does not establish the same lower bound for every prescribed exact value of $L$. The balanced descriptions need not belong to that exact-length input class. The fixed-vector bounds above remain valid for every admissible description, but matching lower bounds within every exact-length class have not been proved here.

8. What remains open

The uniform upper bound, the distinct-type repair, and the subset lower bound are proved. They settle every fixed mass vector with $N\ge\tau\log\tau$, every vector with bounded relative maximum multiplicity, and the worst case over masses at fixed feasible $(N,\tau)$.

Two questions remain:

⟨structured verdict parsed — rendered above⟩

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

The output establishes substantial bounds, but it does not resolve the requested optimal complexity as a function of $N$, $\tau$, and $L$. I found no false central step. The appropriate classification is partial: the proved bounds are credible and rigorous, while the exact-length input classes remain unsettled.

Step-by-step verification

1. Definitions and scope

The multiplicity assumptions
$$ k_t\in\mathbb Z_{>0}, \qquad \sum_t k_t=N $$
correctly imply $\tau\le N$.

The quantity $B(\mathbf{k})$ is well-defined because every denominator is positive. Its elementary range is
$$ 1\le B(\mathbf{k})\le\tau. $$

Defining $Q^*(\mathbf{k})$ initially using distinct supported measures is a restriction relative to a model that might permit separately labeled identical types. Section 3 addresses this restriction sufficiently for the lower-bound construction.

The output explicitly claims a partial solution. Its fixed-vector bounds and its worst case over masses without conditioning on $L$ must therefore be distinguished from the target complexity for a prescribed triple $(N,\tau,L)$.

2. Recursive allocation protocol

Verified.

The root invariant follows from normalization. At an internal node, the positive target
$$ \frac hn s_t $$
is strictly below $s_t$. Continuity gives existence of a CUT answer, and monotonicity ensures every valid answer lies strictly between $a$ and $b$, even when the cumulative valuation has flat portions.

The decreasing order of marks gives the stated inequalities:

The zero-value case is also covered: nonnegativity forces both subintervals to have zero value for that type.

The child invariants therefore hold. Recursion decreases the number of copies and terminates with exactly $N$ leaves, each meeting its owner’s bound. Atomlessness permits arbitrary endpoint ownership.

The endpoint restriction is respected. In particular, if the selected mark is the artificial mark $a$ of a zero-value type, it is an inherited permitted endpoint. Empty or degenerate leaf intervals cause no problem under the stated task.

3. Upper-bound query accounting

Verified.

Within a node, placing each type’s copies consecutively ensures that at most one type is represented in both children. Thus the incidence recurrence is valid, including levels at which some nodes have already terminated.

The maximum depth is $\lceil\log N\rceil$, and each internal incidence uses at most two queries. Consequently,
$$ Q=O(N+\tau\log N). $$

The subsequent conversion is valid:
$$ \tau\log(N/\tau)\le\frac N{\ln 2}, $$
using $\tau\le N$. Hence the claimed uniform bound
$$ Q=O(N+\tau\log\tau) $$
follows.

There is no additional oracle cost from processing the binary input. This does not assert polynomial time in its bit length; arithmetic and output time are explicitly uncharged.

4. Endpoint lower bound

Verified.

The proposed densities are positive, normalized, and pairwise distinct. Their uniform lower bound yields
$$ |X|\le\frac1{N-\frac12} $$
for every permissible bundle.

The permitted-endpoint rule prevents ownership from changing within an elementary open interval between consecutive CUT endpoints. Each such interval therefore satisfies the same length bound. Summing their lengths and using integrality gives
$$ r\ge N-1. $$

Since each distinct interior CUT endpoint requires a CUT query, the query lower bound follows.

The exact statement for $\tau=1$ is also valid. Cumulative cuts at distinct levels $j/N$ give an ordered partition even when individual CUT answers are nonunique.

5. Finite-transcript perturbation and repeated types

Verified.

The perturbation preserves the total value on the selected cell between consecutive points of $P$. Every interval whose endpoints belong to $P$ contains either that entire cell or none of its interior. Its value is therefore preserved.

The positive multipliers preserve atomlessness and full support. Distinct parameter choices produce distinct measures, so only finitely many choices are excluded by previously selected measures.

The transcript argument correctly uses:

The termination argument is sound: any finite transcript preceding an excessive query or nonterminating computation is realizable on an admissible distinct instance.

Output values are preserved because all output endpoints are available coordinates included in the finite set. Thus the extension to repeated full-support measures is justified.

6. Published adversary property

Verified against the cited source.

The precise property used here is stronger than merely a single-oracle worst-case lower bound, so checking the adversary itself is necessary.

The source’s balanced-value trees have positive constant density on each grid cell and density at most $2$. Its Lemma 4.5 supplies the heavy-edge requirement for rich or critical leaves. Lemma 4.7 describes the initial query phase and the revealed-path invariant. An EVAL query strictly inside a cell reveals its determining path; within the stated query budget, that cell cannot be rich or critical and consequently has density below $1/2$. The stated floor in $M(n)$ matches that budget. [Farhadi–Hajiaghayi, Section 4](https://www.ijcai.org/proceedings/2018/0031.pdf)

Independent copies can be interleaved: each copy responds according to its own local query history. Fixing a consistent completion after the initial phase preserves earlier answers. The simultaneous property required for summing query counts is therefore supported.

7. Dual valuations and query simulation

Verified.

Full support and atomlessness make each cumulative function a continuous strictly increasing bijection. Its inverse therefore defines the stated normalized, atomless, full-support valuation.

Both simulation formulas are correct. For CUT queries, the condition $z+r>1$ correctly detects insufficient remaining value for a nonnegative requested amount. Otherwise, the displayed identity verifies the answer. Each allocation query requires at most two underlying queries.

The density upper bound on $w_t$ correctly implies
$$ u_t([x,y])\ge\frac{y-x}{2}, $$
and additivity extends this to finite unions. Thus each hard-type bundle has length at most $2/N$.

8. Counting selected types

Verified.

Uniform filler types occupy total length at most $1-K/N$, so hard-type bundles occupy at least $K/N$.

The displayed length estimate gives $\ell\ge K/3$. Since a type has at most $a$ bundles, at least $K/(3a)$ distinct hard types have a qualifying bundle. This counting remains valid with unequal multiplicities and empty bundles.

9. Dense-cell extraction

Verified.

Strict monotonicity preserves disjoint component interiors. The endpoint transformation gives the stated identities
$$ |P|=u_t(X)\le\frac1N, \qquad w_t(P)=|X|\ge\frac1{2N}. $$

A finite weighted average then ensures a positive-length component with density at least $1/2$. Its density is available from its mapped endpoint lengths and its original interval length.

Since
$$ |J|\le\frac1N\le\frac1n, $$
it intersects at most two grid-cell interiors. Constant density within each cell justifies testing those candidates. At least one test certifies density at least $1/2$, invoking the verified local adversary obstruction.

10. Total lower-bound accounting

Verified.

After removing irrelevant isolated points and normalizing components, the permitted endpoints give at most $r+1$ elementary open intervals. Hence
$$ C\le Q+1, \qquad R\le C. $$

The accounting
$$ 2Q+2C+2R\le6Q+4 $$
includes simulation, endpoint mapping, and candidate tests. Summing the local adversary requirements over selected types is justified by Section 6 above.

The additive constant does not invalidate the asymptotic conclusion. The endpoint bound supplies the baseline needed to combine the bounds into
$$ Q^*(\mathbf{k}) =\Omega\!\left(N+B(\mathbf{k})\log N\right). $$

11. Consequences and encoding claims

Verified within their stated scope.

The bounded-maximum-multiplicity conclusion follows by taking all types as the subset. The dyadic-bin argument correctly establishes the universal lower bound claimed in Section 6. Its constants and bin count are valid, including bins containing boundary multiplicities.

For $N\ge\tau\log\tau$, the endpoint bound and uniform upper bound already match asymptotically.

The balanced integer construction works for ordinary binary-encoded rational masses. Under the dyadic interpretation, the denominator-divisibility argument, feasibility condition, and balanced construction are also correct.

However, these constructions do not establish membership in every prescribed exact-length input class. The output explicitly acknowledges this limitation.

Issue and minimum required follow-up

Major — incomplete resolution of the assigned target. Sections 7–8 leave the tight worst-case complexity for prescribed feasible $(N,\tau,L)$ unresolved. The unconditioned worst case over masses cannot be substituted for that target.

To complete the assignment, the prover must specify the rational encoding used to define $L$ and establish matching bounds within the resulting feasible exact-length classes, or precisely characterize any dependence on those classes. The unresolved fixed-vector question is an additional limitation of the stronger claims being investigated; resolving it is not automatically necessary if the requested worst-case classification can be established directly.

No additional mathematical error or substantive proof gap was detected in the bounds actually established.

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