← back to the atlas

d4-conf-ecai-2025-0261 (d4-conf-ecai-2025-0261)

Answer: $\rho^*(b,B)=\min\left\{\frac{b+\sqrt{b^2+4bB}}{2B},\frac{3b}{B}\right\}$.

The anchor (named result in the paper)

Theorem 6 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateThe AMC-$h$ policy has a competitive ratio of $\min\left\{\frac{1}{2}, \frac{3\mathsf{min}}{\mathsf{max}}\right\}$ for maximizing social welfare when the characteristic function belonging to the class $V_{\delta}$ with $\delta \geq 3$, when $h = \begin{cases} \mathsf{min} & \mathsf{max} < 4\mathsf{min} \text{ (i.e., }v\in V_3 \text{)}; \\ 2\mathsf{min} & \mathsf{max} \geq 4\mathsf{min} \text{ (i.e., }v\in V_{\geq 4} \text{)}.

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

The continuous mirror question, as graded

Given a finite type set \(T\), masses \(\mu\), and a monotone bounded type-symmetric game \(v(A)\) on finite multisets \(A\), what is the best worst-case welfare ratio achievable by a causal, irrevocable, non-wasteful sharing policy when type mass arrives over time and follows the paper’s greedy choice rule, compared with \(\operatorname{OPT}(\mu,v)=\max_{\lambda_A\ge0}\sum_{1\le |A|\le\delta}\lambda_Av(A)\) subject to \(\sum_A a_t(A)\lambda_A=\mu_t\) for every \(t\in T\)?

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

Fix positive binary rationals \(b,B\) and an integer \(\delta\geq3\) with \(\delta b\leq B<(\delta+1)b\). A society is given by its support \(T\): the list of its \(\tau\) types with positive binary-rational masses \(\mu_t\), normalized by \(\sum_t\mu_t=1\); \(\tau\) counts supported types, not possible types.
The type-symmetric value function depends only on a finite multiset \(A\), with \(v(\varnothing)=0\) and \(b\leq v(A)\leq v(D)\leq B\) whenever \(\varnothing\neq A\subseteq D\). Input values are binary rationals tabulated for \(1\leq|A|\leq\delta\); set \(v(A)=B\) for larger multisets. Let \(m\) be the table size and \(L\) the total input bit length; express running times in \(m,\tau,L,\delta\), and the packet parameter \(k\) when applicable.
Define continuous arrivals by vanishing equal-mass packets: for every integer \(k\) with \(k\mu_t\in\mathbb Z\), there are \(k\mu_t\) packets of type \(t\), each of mass \(1/k\), arriving in an arbitrary order \(\pi\). A coalition with multiset \(A\) has welfare \(v(A)/k\).
A deterministic policy family \(\Phi=(\varphi^{(k)})_k\) is announced before arrivals. For each ordered coalition history \(w\), it specifies nonnegative per-unit shares summing to \(v(A(w))\); appending a type cannot decrease any incumbent's share. Shares depend only on \(w\), values on its submultisets, and the known parameters \(T,b,B,k\), never on final masses or future arrivals or unrevealed values.
Each arriving packet immediately and permanently joins an existing coalition or starts a singleton, maximizing its offered immediate share as if it were the last arrival. Use a fixed lexicographic tie rule, with the singleton option first and existing coalitions ordered by their founding arrival. Incumbents may receive additional shares; coalitions cannot merge and members cannot move.
Write \(a_t(A)\) for the multiplicity of type \(t\), and define \(\operatorname{OPT}(\mu,v)=\max_{\lambda_A\geq0}\{\sum_{1\leq|A|\leq\delta}\lambda_Av(A):\sum_Aa_t(A)\lambda_A=\mu_t\text{ for every }t\in T\}\). Let \(\operatorname{SW}_{\varphi^{(k)}}(v,\pi)\) denote terminal packet welfare.

What is the optimal worst-case welfare ratio \(\rho^*(b,B)=\sup_\Phi\inf_{T,\mu,v}\liminf_{\substack{k\to\infty\\k\mu\in\mathbb Z^T}}\inf_\pi\frac{\operatorname{SW}_{\varphi^{(k)}}(v,\pi)}{\operatorname{OPT}(\mu,v)}\) for this continuous model?

For discrete players, allocating the newcomer's marginal contribution minus a threshold to the newcomer, and the remainder to the preceding coalition member, guarantees \(\min\{1/2,3b/B\}\), using threshold \(b\) when \(B<4b\) and \(2b\) otherwise; the founder receives its singleton value. [Verified discrete guarantee](https://arxiv.org/html/2507.11883v1#Thmtheorem6).
Every discrete irrevocable policy has worst-case ratio at most \(3b/B\). [Verified discrete upper bound](https://arxiv.org/html/2507.11883v1#Thmtheorem2). No result settling this specified continuous model was located.

Modeling choices made when packaging the task

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

Exact optimal ratio

The optimal worst-case welfare ratio is
$$ \boxed{ \rho^*(b,B)= \min\left\{ \frac{b+\sqrt{b^2+4bB}}{2B}, \frac{3b}{B} \right\}. } $$
Equivalently,
$$ \rho^*(b,B)= \begin{cases} \dfrac{b+\sqrt{b^2+4bB}}{2B},&3b\leq B\leq6b,\\[6pt] \dfrac{3b}{B},&B\geq6b. \end{cases} $$

The new step closing the gap in the notes is a three-type upper bound. It uses three different positive dyadic mass profiles with the same support and value table. Thus their relevant offers coincide even for policies depending arbitrarily on the packet parameter.

1. Preliminaries

Write
$$ q=\frac{B}{b}, \qquad f(q)=\frac{1+\sqrt{1+4q}}{2q}. $$
The hypotheses imply $q\geq3$.

For every admissible policy, a packet of type $t$ receives at least its singleton value $v(\{t\})$ upon entry: starting a singleton offers exactly that value. Irrevocability preserves this lower bound. Consequently, every actual coalition $C$ satisfies
$$ v(C)\geq |C|b. $$
Since $v(C)\leq B<(\delta+1)b$, every actual coalition has at most $\delta$ members.

The benchmark program is feasible: take $\lambda_{\{t\}}=\mu_t$ and all other variables zero. Moreover, every feasible solution satisfies
$$ \sum_A |A|\lambda_A = \sum_t\mu_t = 1. $$
Its feasible region is therefore bounded and closed, so its maximum exists.

2. An admissible policy attaining the claimed lower bound

2.1. Threshold allocation

Fix a threshold $h\geq0$. A founder receives its singleton value. When a type $t$ is appended to a nonempty coalition with multiset $A$, let
$$ \Delta=v(A+\{t\})-v(A). $$
Give the newcomer
$$ \max\{0,\Delta-h\}, $$
and increase the preceding coalition member’s share by
$$ \min\{\Delta,h\}. $$
Leave all other shares unchanged.

Monotonicity gives $\Delta\geq0$. The two allocations sum to $\Delta$, so this defines nonnegative, budget-balanced, irrevocable shares recursively for every ordered history. It uses only permitted history values and the parameters $b,B$. This is the threshold allocation discussed in the [supplied discrete result](https://arxiv.org/html/2507.11883v1#Thmtheorem6); its continuous guarantee is proved below directly.

Label the packets by $i$, and put
$$ s_i=v(\{t(i)\}). $$
Because the singleton option wins ties, an actual join requires
$$ \Delta-h>s_i. $$
Summing along a terminal coalition’s formation gives
$$ v(C)\geq \sum_{i\in C}s_i+(|C|-1)h. $$

Define analytical weights, rather than policy shares, by
$$ u_i = s_i+ \frac{v(C)-\sum_{j\in C}s_j}{|C|} \qquad(i\in C). $$
They satisfy
$$ \sum_{i\in C}u_i=v(C), \qquad u_i\geq s_i. $$
For a nonsingleton terminal coalition,
$$ u_i \geq s_i+\frac{|C|-1}{|C|}h \geq s_i+\frac h2. $$

2.2. Inequalities for subsets of labeled packets

Set
$$ \alpha(h)= \min\left\{ \frac{2b}{2b+h}, \frac{4b+h}{2B}, \frac{3b}{B} \right\}. $$
We prove that every nonempty subset $S$ of labeled packets with $|S|\leq\delta$ satisfies
$$ \sum_{i\in S}u_i\geq \alpha(h)v(S). $$
Here $v(S)$ denotes the value of its type multiset, including repeated types.

There are four exhaustive cases.

$$ u_i\geq s_i=v(\{i\})\geq\alpha(h)v(\{i\}). $$

$$ \max\{0,v(\{i,j\})-s_i-h\}\leq s_j. $$
Therefore
$$ v(\{i,j\})\leq s_i+s_j+h. $$
With $x=s_i+s_j\geq2b$,
$$ u_i+u_j=x \geq \frac{2b}{2b+h}(x+h) \geq \frac{2b}{2b+h}v(\{i,j\}). $$
The first inequality follows from
$$ \frac{x}{x+h}\geq\frac{2b}{2b+h}. $$

$$ u_i+u_j \geq \frac{4b+h}{2B}v(\{i,j\}), $$
because $v(\{i,j\})\leq B$.

$$ \sum_{i\in S}u_i\geq3b \geq\frac{3b}{B}v(S). $$

This proves the asserted subset inequality.

2.3. Transfer to the fractional benchmark

Fix an instance and an admissible packet parameter $k$. Write
$$ n_t=k\mu_t. $$
For all sufficiently large admissible $k$, every supported type satisfies $n_t\geq\delta$, because its mass is positive.

Define its average analytical weight by
$$ \overline u_t = \frac1{n_t}\sum_{i:t(i)=t}u_i. $$
For a table multiset $A$, choose uniformly a labeled subset containing exactly $a_t(A)$ packets of each type $t$. These choices exist because $n_t\geq\delta$. Every selected subset has value $v(A)$.

A packet of type $t$ is included with probability $a_t(A)/n_t$. Averaging the subset inequality therefore yields
$$ \sum_t a_t(A)\overline u_t\geq\alpha(h)v(A). $$
For any feasible benchmark allocation $(\lambda_A)_A$, multiply by $\lambda_A$ and sum:
$$ \begin{aligned} \alpha(h)\sum_A\lambda_Av(A) &\leq \sum_t\overline u_t\sum_Aa_t(A)\lambda_A\\ &= \sum_t\mu_t\overline u_t\\ &= \frac1k\sum_i u_i\\ &= \operatorname{SW}_{\varphi^{(k)}}(v,\pi). \end{aligned} $$
Taking the maximum over feasible allocations proves
$$ \operatorname{SW}_{\varphi^{(k)}}(v,\pi) \geq \alpha(h)\operatorname{OPT}(\mu,v) $$
for every arrival order and all sufficiently large admissible $k$.

The weights and the mass averages are used only in this proof. The policy itself uses neither final masses nor future arrivals.

2.4. Choosing the threshold

The first threshold-dependent term in $\alpha(h)$ decreases with $h$, and the second increases. They coincide when
$$ (2b+h)(4b+h)=4bB, $$
whose nonnegative solution is
$$ h_*=\sqrt{b^2+4bB}-3b. $$
It is positive because $B\geq3b$. At this threshold, both terms equal
$$ \frac{b+\sqrt{b^2+4bB}}{2B}=f(q). $$
Hence
$$ \rho^*(b,B)\geq \min\left\{f(q),\frac3q\right\}. $$
For $q\geq6$, the rational threshold $h=2b$ also attains $3/q$, since
$$ \alpha(2b)= \min\left\{\frac12,\frac{3b}{B},\frac{3b}{B}\right\} = \frac{3b}{B}. $$

3. A universal upper bound

Use one supported type of mass $1$, with
$$ v(A)= \begin{cases} b,&1\leq|A|\leq2,\\ B,&|A|\geq3. \end{cases} $$
This is an admissible monotone table and extension.

A singleton incumbent receives $b$. A pair also has value $b$, so budget balance and irrevocability force its newcomer’s offer to be zero. By induction, every packet starts a singleton under every policy. Terminal packet welfare is therefore $b$.

For the one-type fractional benchmark,
$$ \operatorname{OPT} = \max_{1\leq r\leq\delta}\frac{v(r)}r = \frac B3. $$
Indeed, the size-three column exists, $B/3\geq b$, and no other column has greater value per packet. Consequently,
$$ \rho^*(b,B)\leq\frac{3b}{B}. $$

4. The three-type upper bound

We now prove, for every binary rational $P$ satisfying
$$ 2b<P<B, $$
the bound
$$ \rho^*(b,B) \leq \max\left\{ \frac{2b}{P}, \frac{P+2b}{2B}, \frac{B+3b}{3B} \right\}. $$

4.1. A common support and value table

Take the support
$$ T=\{x,y,z\}. $$
For multisets of size at most $\delta$, define:

For larger multisets, use the prescribed extension $v(A)=B$.

This table is monotone: a pure multiset’s value can increase only from $b$ to $P$ or $B$, and a mixed multiset already has value $B$.

Fix an arbitrary admissible policy family $\Phi$. For each $k$, let
$$ \xi_k = \text{the newcomer’s offer for history }(x,x), $$
and
$$ \eta_k = \text{the newcomer’s offer for history }(x,x,y). $$
These offers are identical across the mass profiles below. Their ordered histories, local values, support, and parameters coincide, and final masses are prohibited policy inputs.

Whenever all $x$ packets arrive first:

For the second statement, a singleton offers $\xi_k>b$, whereas an existing $x$-pair offers a further $x$ packet zero: its size-three value is still $P$, so no additional value is available after preserving the incumbents’ total shares.

4.2. Profile A: refusing the third packet

Fix a positive dyadic $\varepsilon<1/4$ and take
$$ \mu_x=\mu_y=\frac{1-\varepsilon}{2}, \qquad \mu_z=\varepsilon. $$
Use the arrival order consisting of all $x$ packets, then all $y$ packets, then all $z$ packets.

Consider admissible $k$ for which the number of $x$ packets is even and
$$ \xi_k>b, \qquad \eta_k\leq b. $$
After the first phase, there are exactly
$$ \frac{(1-\varepsilon)k}{4} $$
$x$-pairs. Every $y$ packet starts a singleton: joining an $x$-pair offers at most $b$, and joining a pure $y$ singleton offers zero.

Welfare before the $z$ phase is
$$ (1-\varepsilon)\left(\frac P4+\frac b2\right). $$
Each later arrival increases welfare by at most $B$: it either starts a singleton or increases one existing coalition’s value by at most $B$. Thus
$$ \operatorname{SW} \leq (1-\varepsilon)\left(\frac P4+\frac b2\right)+\varepsilon B. $$

A feasible benchmark allocation uses mixed $xy$ pairs and $z$ singletons, giving
$$ \operatorname{OPT} \geq \frac{1-\varepsilon}{2}B+\varepsilon b. $$
The ratio is consequently at most
$$ H_\varepsilon(P)= \frac{ (1-\varepsilon)(P/4+b/2)+\varepsilon B }{ (1-\varepsilon)B/2+\varepsilon b }, $$
and
$$ \lim_{\varepsilon\to0}H_\varepsilon(P) = \frac{P+2b}{2B}. $$

4.3. Profile B: refusing the initial pair

With the same $\varepsilon$, take
$$ \mu_x=1-2\varepsilon, \qquad \mu_y=\mu_z=\varepsilon. $$
Again, all $x$ packets arrive first, then all $y$, then all $z$.

If $\xi_k\leq b$, the first phase consists entirely of singletons, with welfare $(1-2\varepsilon)b$. There are $2\varepsilon k$ later arrivals, each increasing welfare by at most $B$. Hence
$$ \operatorname{SW} \leq (1-2\varepsilon)b+2\varepsilon B. $$

The benchmark can use pure $x$-pairs and singleton $y$ and $z$ coalitions:
$$ \operatorname{OPT} \geq \frac{1-2\varepsilon}{2}P+2\varepsilon b. $$
Therefore the ratio is at most
$$ R_\varepsilon(P)= \frac{ (1-2\varepsilon)b+2\varepsilon B }{ (1-2\varepsilon)P/2+2\varepsilon b }, $$
with
$$ \lim_{\varepsilon\to0}R_\varepsilon(P)=\frac{2b}{P}. $$

4.4. Profile C: accepting both joins

Take a positive dyadic $a<1/6$ and set
$$ \mu_x=2a, \qquad \mu_y=a, \qquad \mu_z=1-3a. $$
All masses are positive dyadic numbers. Use the same type-block arrival order.

Suppose
$$ \xi_k>b, \qquad \eta_k>b. $$
For admissible $k$, the $2ak$ initial $x$ packets form exactly $ak$ pairs. Every subsequent $y$ packet joins an unfilled $x$-pair:

There are exactly $ak$ arriving $y$ packets. Thus every $x$-pair becomes an $xxy$ triple of value $B$.

Every later $z$ packet starts a singleton. Existing triples already have value $B$, and pure $z$ pairs have value $b$, so neither option offers a positive newcomer share. Terminal welfare is exactly
$$ \operatorname{SW}=aB+(1-3a)b. $$

A feasible benchmark allocation is
$$ \lambda_{\{x,z\}}=2a, \qquad \lambda_{\{y,z\}}=a, \qquad \lambda_{\{z\}}=1-6a. $$
These nonnegative coefficients use precisely the specified masses. They give
$$ \operatorname{OPT}\geq3aB+(1-6a)b. $$
Consequently the ratio is at most
$$ G_a= \frac{aB+(1-3a)b}{3aB+(1-6a)b}. $$
Taking dyadic $a$ approaching $1/6$ from below,
$$ \lim_{a\to(1/6)^-}G_a = \frac{B+3b}{3B}. $$

4.5. The quantifiers and dependence on the packet parameter

For fixed $\varepsilon$ and $a$, choose an infinite arithmetic progression of packet parameters admissible for all three profiles, additionally ensuring an even number of $x$ packets in Profile A. Such a progression exists because all masses are dyadic.

Every $k$ in this progression belongs to exactly one of the following classes:
$$ \begin{aligned} &\xi_k\leq b,\\ &\xi_k>b,\quad \eta_k\leq b,\\ &\xi_k>b,\quad \eta_k>b. \end{aligned} $$
At least one class is infinite.

If the first class is infinite, the fixed Profile B has limiting inferior ratio at most $R_\varepsilon(P)$. If the second is infinite, Profile A has limiting inferior ratio at most $H_\varepsilon(P)$. If the third is infinite, Profile C has limiting inferior ratio at most $G_a$.

Each conclusion follows because an infinite admissible subsequence bounds the limiting inferior over all admissible packet parameters, and the infimum over arrival orders is at most the ratio for the displayed order.

Thus, for every policy family, its worst-instance limiting inferior ratio is at most
$$ \max\{R_\varepsilon(P),H_\varepsilon(P),G_a\}. $$
Letting $\varepsilon$ tend to zero through positive dyadics and $a$ approach $1/6$ through dyadics from below gives
$$ \inf_{T,\mu,v} \liminf_{\substack{k\to\infty\\k\mu\in\mathbb Z^T}} \inf_\pi \frac{\operatorname{SW}_{\varphi^{(k)}}(v,\pi)} {\operatorname{OPT}(\mu,v)} \leq \max\left\{ \frac{2b}{P}, \frac{P+2b}{2B}, \frac{B+3b}{3B} \right\}. $$
This bound is uniform over policy families, so it also bounds $\rho^*(b,B)$.

5. Matching the lower bound

Put
$$ p=\sqrt{b^2+4bB}-b. $$
For $q\geq3$, one has $2b<p<B$. Indeed,
$$ \frac pb=\sqrt{1+4q}-1>2, $$
and
$$ \sqrt{1+4q}<q+1 $$
because squaring reduces the latter inequality to $q(q-2)>0$.

Also,
$$ p^2+2bp=4bB, $$
so
$$ \frac{2b}{p} = \frac{p+2b}{2B} = f(q). $$
Choose binary rationals $P$ approaching $p$ within $(2b,B)$. The three-type upper bound and continuity imply
$$ \rho^*(b,B) \leq \max\left\{ f(q),\frac{q+3}{3q} \right\}. $$

For $q\geq3$,
$$ f(q)\geq\frac{q+3}{3q} \quad\Longleftrightarrow\quad 3\sqrt{1+4q}\geq2q+3. $$
Both sides of the last inequality are positive. Squaring therefore preserves equivalence and gives
$$ 9+36q\geq4q^2+12q+9 \quad\Longleftrightarrow\quad q\leq6. $$
Hence, when $3\leq q\leq6$,
$$ \rho^*(b,B)\leq f(q). $$
When $q\geq6$, Section 3 gives
$$ \rho^*(b,B)\leq\frac3q. $$

Finally,
$$ f(q)\leq\frac3q \quad\Longleftrightarrow\quad \sqrt{1+4q}\leq5 \quad\Longleftrightarrow\quad q\leq6. $$
These upper bounds match Section 2 in every permitted parameter range, proving the stated formula. The exhibited threshold policy family attains the optimum.

6. Running times and exact arithmetic

Benchmark computation

The benchmark is a rational linear program with $m$ variables and $\tau$ equality constraints. Every incidence coefficient belongs to $\{0,\ldots,\delta\}$. Its encoding length is bounded by
$$ O\!\left(L+m\tau\log(\delta+1)\right). $$
The polynomial-time theorem for rational linear programming computes an exact optimum in time polynomial in this encoding length. Its hypotheses hold here: all coefficients are rational, the feasible region is nonempty, and the objective has a finite attained maximum by Section 1. Thus the benchmark is computable in
$$ \operatorname{poly}\!\left(L+m\tau\log(\delta+1)\right) $$
bit operations.

Policy implementation

At each arrival, evaluate at most $k$ existing coalitions and the singleton option. Actual coalition histories have length at most $\delta$; an augmented multiset beyond that size has the prescribed value $B$.

Using linear searches through table keys, a conservative implementation takes
$$ O(k^2m\tau\delta) $$
arithmetic operations and comparisons. Its bit-operation bound is
$$ O\!\left( k^2m\tau\delta\, \operatorname{poly}\!\left( L+\log k+\log(\delta+1) \right) \right). $$
Only the requested history values enter the allocation decisions.

For $B\leq6b$, the threshold $h_*$ lies in a quadratic extension of the rationals. Store shares as rational expressions in $\sqrt{b^2+4bB}$. Exact sign comparisons reduce, after checking signs, to rational comparisons by squaring; they have polynomial bit complexity. Rational coefficient lengths remain polynomial in the displayed parameters because the input denominators have total bit length bounded by $L$, and accumulated multiplicities are bounded by $k$. The model permits these algebraic shares.

For $B\geq6b$, use the rational threshold $2b$. The optimal ratio itself has a rational or quadratic-radical representation computable in time polynomial in $L$.

⟨structured verdict parsed — rendered above⟩

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

The claimed formula is proved for the specified continuous model. The lower bound, the three-profile upper bound, and their limiting quantifiers are valid. I found no major or minor issues requiring repair.

1. Preliminaries

Every arriving packet can obtain its singleton value by starting a coalition. Its chosen immediate share is therefore at least that value, and irrevocability preserves this lower bound thereafter. Budget balance consequently implies
$$ v(C)\geq\sum_{i\in C}v(\{t(i)\})\geq |C|b. $$
Together with $v(C)\leq B<(\delta+1)b$, this correctly bounds every actual coalition’s size by $\delta$.

The benchmark is feasible through singleton columns. Summing its type constraints gives
$$ \sum_A |A|\lambda_A=1. $$
Because there are finitely many columns and every column is nonempty, its nonnegative feasible region is bounded and closed. The asserted existence of an optimum follows.

2. Threshold policy and lower bound

Policy admissibility

The prescribed newcomer payment and incumbent increment are nonnegative and sum to the marginal increase:
$$ \max\{0,\Delta-h\}+\min\{\Delta,h\}=\Delta $$
for $\Delta\geq0$. The recursive allocation is therefore budget-balanced and irrevocable on every history, including histories that do not occur during play.

Its decisions use only the permitted history values and known parameters. The analytical weights introduced later are separate from the policy and do not create prohibited dependence on final masses.

The attribution to the [supplied discrete result](https://arxiv.org/html/2507.11883v1#Thmtheorem6) is background; the continuous guarantee is established independently in the output.

Formation inequality and analytical weights

Because the singleton option wins ties, an actual join requires
$$ \Delta-h>s_i. $$
Summing these inequalities along a coalition’s formation justifies the stated weaker inequality
$$ v(C)\geq\sum_{i\in C}s_i+(|C|-1)h. $$

The analytical weights sum to coalition value. Their claimed bounds follow directly from this formation inequality. In particular, for a nonsingleton coalition,
$$ u_i\geq s_i+\frac{|C|-1}{|C|}h\geq s_i+\frac h2. $$

Subset inequalities

The four cases are exhaustive and valid:

Repeated types do not invalidate any case: the subsets consist of distinct labeled packets, and values are evaluated on their type multisets.

Transfer to the fractional benchmark

For each fixed positive mass profile, every supported type eventually has at least $\delta$ packets along the admissible packet parameters. Thus every table multiset can be represented by the sampled labeled subsets.

The inclusion probabilities and averaging calculation are correct. Multiplication by the nonnegative benchmark coefficients preserves the inequalities, and the type constraints yield
$$ \sum_t\mu_t\overline u_t =\frac1k\sum_i u_i =\operatorname{SW}_{\varphi^{(k)}}(v,\pi). $$
This correctly proves the lower bound for every arrival order and all sufficiently large admissible $k$.

The required cutoff may depend on the instance. That is compatible with the instance-by-instance limiting inferior in the task.

Threshold optimization

The intersection equation, its nonnegative solution, and the resulting common value are correct:
$$ h_*=\sqrt{b^2+4bB}-3b, \qquad \alpha(h_*)=\min\{f(q),3/q\}. $$
The threshold is positive throughout the permitted range $q\geq3$. For $q\geq6$, the alternative threshold $h=2b$ correctly attains $3/q$.

3. One-type upper bound

The constructed value table is admissible, including its prescribed extension beyond $\delta$.

A pair has no additional value over its singleton incumbent. Irrevocability and budget balance therefore force the newcomer’s offer to be zero. Every packet starts a singleton, giving welfare $b$.

The benchmark calculation is correct. The size-three column exists because $\delta\geq3$, and
$$ \max_{1\leq r\leq\delta}\frac{v(r)}r=\frac B3 $$
because $B/3\geq b$. This establishes the universal upper bound $3b/B$.

4. Three-type upper bound

Common table and offers

The table is monotone and satisfies all value restrictions. Its larger-multiset extension also preserves monotonicity.

The offers $\xi_k$ and $\eta_k$ coincide across the three mass profiles: their histories, local values, support, and permitted parameters coincide. The task expressly excludes final masses from policy inputs.

The description of the initial $x$ phase is correct. If $\xi_k\leq b$, ties favor singletons. If $\xi_k>b$, packets form pairs; a third $x$ packet receives zero because the coalition value remains $P$ and the incumbents already receive total shares $P$.

Profile A

The parity restriction ensures that the initial phase consists entirely of $x$-pairs. Under $\eta_k\leq b$, every $y$ packet starts a singleton.

Both the welfare calculation before the $z$ phase and the bound on subsequent welfare increments are correctly scaled by packet mass. The displayed benchmark allocation satisfies all type constraints, and the expression and limit for $H_\varepsilon(P)$ are correct.

Profile B

Under $\xi_k\leq b$, the initial singleton welfare is correctly calculated. The bound on later welfare increments is valid.

The proposed pure-$x$ pairs and remaining singletons form a feasible benchmark allocation. The expression and limit for $R_\varepsilon(P)$ are correct.

Profile C

Admissibility makes $ak$ integral, so the initial $2ak$ packets form exactly $ak$ pairs. Under $\eta_k>b$, each subsequent $y$ packet joins an unfilled pair. Completed triples have value $B$ and cannot offer a positive newcomer share.

All later $z$ packets consequently start singletons, giving the stated terminal welfare.

The benchmark coefficients are nonnegative because $a<1/6$. They consume exactly the specified masses. The expression for $G_a$ and its limit as $a$ approaches $1/6$ from below are correct.

Quantifier audit

This is the critical continuous-model step, and it is sound.

For each fixed choice of $\varepsilon$ and $a$, a common infinite arithmetic progression of admissible packet parameters exists, including the parity requirement. Partitioning it into the three offer classes guarantees an infinite class.

Each class supplies a bound for one fixed mass profile along an infinite admissible subsequence. That bounds the limiting inferior over all admissible packet parameters. The infimum over arrival orders can only decrease the displayed-order ratio.

The resulting bound by the maximum of the three profile bounds holds for every fixed $\varepsilon$ and $a$. Taking their indicated limits is legitimate after establishing that bound on the worst-instance infimum. No interchange of an instance-dependent limit with the packet limit is assumed.

5. Matching bounds and boundary cases

The proposed limiting value $p$ lies strictly inside $(2b,B)$ throughout $q\geq3$. Its defining identity and the two resulting equal ratios are correct. Approximating it by binary rationals preserves admissibility and justifies the continuity argument.

Both comparison calculations are correct:
$$ f(q)\geq\frac{q+3}{3q} \quad\Longleftrightarrow\quad q\leq6, $$
and
$$ f(q)\leq\frac3q \quad\Longleftrightarrow\quad q\leq6. $$
The squaring step uses positive quantities, as explicitly checked.

The upper and lower bounds match, including at $q=3$ and $q=6$. The exhibited policy attains the optimum rather than merely approaching it.

6. Running times and arithmetic

The benchmark has the stated number of variables and constraints. Its incidence coefficients and rational data satisfy the hypotheses of the invoked polynomial-time rational linear-programming result. The encoding-length estimate is a valid conservative bound.

The packet-policy implementation bound is also conservative: it scans at most $k$ coalitions per arrival and uses histories of actual size at most $\delta$. Exact quadratic arithmetic suffices for the threshold and shares. The claimed polynomial coefficient lengths are consistent with the finite rational input and accumulated multiplicities.

The simulation bound is polynomial in $k$, as requested; it is not claimed to be polynomial in $\log k$. The optimal continuous ratio itself has the stated polynomial-time exact representation.

No additional clarification or repair is needed.

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