Answer: The guarantee \(\mathrm{OPT}_{\pi}\ge\tfrac12\mathrm{OPT}\) holds for every admissible instance and every supplied order \(\pi\).
Theorem 1 — class: algorithmic
PDF text-layer excerpt — equations and symbol order may be approximateWhen λk = 1 for every k, we have r = SW(θ∗ ≺ads) SW(θ∗) ≥1 2 for every ≺ads.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given a finite type set \(T\), rational type masses \(\mu_t\ge 0\) summing to \(1\), per-unit values \(\bar v_t\), fatigue rates \(\delta_t\ge 0\), and feed mass \(\rho\in(0,1]\), choose a measurable schedule \(z:[0,\rho]\to T\) with \(|\{x:z(x)=t\}|\le\mu_t\) to maximize \(W(z)=\int_0^\rho \bar v_{z(x)}\exp(-\int_0^x\delta_{z(y)}\,dy)\,dx\). For every supplied total order \(\pi\) on \(T\), does the best schedule whose nonempty type blocks follow \(\pi\) achieve at least half the unrestricted optimum?
A society is given by its support \(T\): the list of its \(\tau=|T|\ge1\) types with positive binary rational masses \(\mu_t\), where \(\sum_t\mu_t=1\); \(\tau\) counts supported types, not possible types. Each type has binary rational per-unit value \(\bar v_t\ge0\) and finite fatigue rate \(\delta_t\ge0\). The input also includes binary rational capacity \(\rho\in(0,1]\) and a strict total order \(\pi\) on \(T\).
A feasible schedule chooses a length \(\ell\in[0,\rho]\) and a measurable map \(z:[0,\ell]\to T\), with \(\operatorname{Leb}\{x:z(x)=t\}\le\mu_t\) for every type; unused capacity is a vacant suffix.
Its welfare is \(W(z)=\int_0^\ell \bar v_{z(x)}\exp\bigl(-\int_0^x\delta_{z(y)}\,dy\bigr)\,dx\). There is no position-dependent attenuation.
A schedule respects \(\pi\) if, up to null sets, each used type occupies one contiguous interval and these intervals follow \(\pi\); types may be omitted and their masses partially used. Unrestricted schedules may split and revisit types.
Let \(\mathrm{OPT}\) and \(\mathrm{OPT}_\pi\) be the supremal welfare over unrestricted and order-respecting feasible schedules, respectively. Any running times are measured in \(\tau\) and total input bit length \(L\); this model has no separate ambient parameter \(m\).
Does \(\mathrm{OPT}_\pi\ge\tfrac12\mathrm{OPT}\) hold for every admissible instance and every supplied order \(\pi\), or can this guarantee fail?
For finite ads with nonnegative values and continuation probabilities in \([0,1]\), the best subsequence of any prescribed order attains at least half the unrestricted welfare when position-dependent attenuation is absent; the guarantee also holds for constant position factors. [Farina–Gatti](https://arxiv.org/pdf/1511.07397).
The [later full version](https://www.mit.edu/~gfarina/2017/adopting-cascade-model-truthful-jair17/adopting-cascade-model-truthful-jair17.pdf) retains this guarantee and explicitly permits vacant suffixes. No result settling the exact continuous model above was located.
1. Result
The guarantee holds for every admissible instance and every supplied order:
\[ \mathrm{OPT}_{\pi}\ge \tfrac12\mathrm{OPT}. \]
We prove this directly for measurable schedules, including schedules that split and revisit types. The argument gives a continuous analogue of [Farina–Gatti’s Theorem 1](https://www.mit.edu/~gfarina/2017/adopting-cascade-model-truthful-jair17/adopting-cascade-model-truthful-jair17.pdf).
2. Freeze the amounts used by an arbitrary schedule
Fix a feasible schedule \(z:[0,\ell]\to T\). For each type define its cumulative usage and total usage by
\[ a_t(x)=\int_0^x\mathbf 1_{\{z(y)=t\}}\,dy, \qquad a_t=a_t(\ell). \]
Thus \(0\le a_t\le\mu_t\) and \(\sum_ta_t=\ell\le\rho\).
Define
\[ \Phi_t(u)=\int_0^u e^{-\delta_t s}\,ds = \begin{cases} (1-e^{-\delta_t u})/\delta_t,&\delta_t>0,\\ u,&\delta_t=0, \end{cases} \]
and let
\[ R_t=\bar v_t\Phi_t(a_t), \qquad C_t=e^{-\delta_t a_t}. \]
Here \(R_t\) is the welfare of a contiguous block of type \(t\), of length \(a_t\), when its incoming attenuation equals one. Its continuation factor is \(C_t\). Finiteness of the fatigue rates implies \(0<C_t\le1\), and
\[ 1-C_t=\delta_t\Phi_t(a_t). \]
For a subsequence \(t_1,\ldots,t_k\) of the supplied order \(\pi\), define
\[ V(t_1,\ldots,t_k) = \sum_{i=1}^k R_{t_i}\prod_{j<i}C_{t_j}. \]
Concatenating these blocks gives exactly this welfare. Such a schedule is feasible: its total length is at most \(\ell\), and each type uses at most its original amount \(a_t\). Zero-length blocks can simply be omitted.
Let \(B\) be the maximum of \(V\) over all subsequences of \(\pi\), including the empty subsequence. This maximum exists because there are finitely many subsequences. Consequently,
\[ 0\le B\le\mathrm{OPT}_{\pi}. \]
3. A finite telescoping inequality
We claim that
\[ \sum_{t\in T}\bigl(R_t-B(1-C_t)\bigr)_+\le B, \qquad u_+=\max\{u,0\}. \]
To prove this, put \(g_t=R_t-B(1-C_t)\), and list the types for which \(g_t>0\) in their supplied order as \(t_1,\ldots,t_k\). Set
\[ Q_i=\prod_{j<i}C_{t_j}, \qquad P=\prod_{j=1}^k C_{t_j}>0. \]
Empty products equal one. Since every continuation factor is at most one, \(Q_i\ge P\). The definition of \(B\), followed by telescoping, gives
\[ \begin{aligned} B &\ge V(t_1,\ldots,t_k)\\ &=\sum_{i=1}^k Q_i\bigl(B(1-C_{t_i})+g_{t_i}\bigr)\\ &=B(1-P)+\sum_{i=1}^k Q_i g_{t_i}\\ &\ge B(1-P)+P\sum_{i=1}^k g_{t_i}. \end{aligned} \]
Subtracting \(B(1-P)\) and dividing by the strictly positive \(P\) proves the claim. The same calculation covers the empty subsequence.
4. Bound the original measurable schedule
Write
\[ A(x)=\sum_{t\in T}\delta_t a_t(x), \qquad S(x)=e^{-A(x)}. \]
The functions \(a_t\), \(A\), and \(S\) are absolutely continuous. Almost everywhere,
\[ S'(x)=-\delta_{z(x)}S(x). \]
Therefore,
\[ \begin{aligned} W(z) &=\int_0^\ell \bar v_{z(x)}S(x)\,dx\\ &=B\bigl(1-S(\ell)\bigr) +\sum_{t\in T}(\bar v_t-B\delta_t) \int_{\{x:z(x)=t\}}S(x)\,dx. \end{aligned} \]
We now bound each integral without making any assumption about how often a type is revisited. Nonnegative fatigue rates imply
\[ A(x)\ge\delta_t a_t(x), \qquad S(x)\le e^{-\delta_t a_t(x)}. \]
Moreover, the chain rule for absolutely continuous functions gives
\[ \begin{aligned} \int_{\{x:z(x)=t\}}e^{-\delta_t a_t(x)}\,dx &=\int_0^\ell e^{-\delta_t a_t(x)}a_t'(x)\,dx\\ &=\Phi_t(a_t). \end{aligned} \]
Dropping terms with negative coefficients in the welfare identity, and applying these bounds to the remaining terms, yields
\[ \begin{aligned} W(z) &\le B\bigl(1-S(\ell)\bigr) +\sum_{t\in T}(\bar v_t-B\delta_t)_+\Phi_t(a_t)\\ &=B\bigl(1-S(\ell)\bigr) +\sum_{t\in T}\bigl(R_t-B(1-C_t)\bigr)_+\\ &\le B\bigl(2-S(\ell)\bigr)\\ &\le 2B\\ &\le 2\mathrm{OPT}_{\pi}. \end{aligned} \]
The second equality uses \(\Phi_t(a_t)\ge0\) and \(1-C_t=\delta_t\Phi_t(a_t)\). The next inequality is precisely the telescoping inequality proved above.
Since \(z\) was an arbitrary feasible measurable schedule, taking the supremum proves
\[ \mathrm{OPT}\le2\mathrm{OPT}_{\pi}. \]
No existence assumption for an unrestricted maximizing schedule is needed. The argument uses at most one block per supported type, hence at most \(\tau\) blocks.
⟨structured verdict parsed — rendered above⟩
The proof is correct and resolves the assigned question: \(\mathrm{OPT}_{\pi}\ge \tfrac12\mathrm{OPT}\) holds for every admissible instance and every supplied order. No major or minor mathematical issues were found.
For a measurable schedule, each indicator \(\mathbf 1_{\{z(x)=t\}}\) is measurable and bounded. Consequently, the cumulative usage \(a_t(x)\) is absolutely continuous, with derivative \(\mathbf 1_{\{z(x)=t\}}\) almost everywhere.
The bounds \(0\le a_t\le\mu_t\) follow from feasibility. Since the type sets partition the schedule domain, \(\sum_t a_t=\ell\le\rho\). These statements remain valid for schedules with arbitrarily many revisits.
The formulas for \(\Phi_t\), \(R_t\), and \(C_t\) are correct, including when \(\delta_t=0\). In particular, \(1-C_t=\delta_t\Phi_t(a_t)\) holds in both cases. Finite fatigue rates and finite usage amounts ensure \(0<C_t\le1\).
Assessment: Correct.
A block of type \(t\) with incoming attenuation \(s\) contributes \(sR_t\) and multiplies attenuation by \(C_t\). Thus the displayed expression for \(V(t_1,\ldots,t_k)\) is exactly the welfare of the concatenated blocks.
Every such subsequence respects \(\pi\), uses each type at most once, and uses at most its original amount. Its total length is at most \(\ell\le\rho\); any remaining capacity is a vacant suffix.
There are finitely many subsequences, and all their welfare values are finite. Therefore \(B\) exists and satisfies \(0\le B\le\mathrm{OPT}_{\pi}\).
Assessment: Correct. No assumption about rationality of the frozen amounts is needed for these feasible schedules.
For the selected types, \(g_{t_i}>0\). Since all continuation factors lie in \((0,1]\), the prefix product satisfies \(Q_i\ge P>0\). Multiplying this comparison by the positive \(g_{t_i}\) preserves its direction.
The telescoping identity \(\sum_i Q_i(1-C_{t_i})=1-P\) is correct. Hence the displayed calculation yields \(BP\ge P\sum_i g_{t_i}\), and division by \(P>0\) establishes the claimed positive-part bound.
For the empty selected subsequence, \(P=1\), both sums vanish, and the same calculation is valid. No division by \(B\) occurs, so \(B=0\) poses no problem.
Assessment: Correct. The positivity needed for division follows explicitly from the task’s finite-fatigue assumption.
The finite sum \(A(x)\) is absolutely continuous, with derivative \(\delta_{z(x)}\) almost everywhere. Its range is bounded because there are finitely many finite fatigue rates and \(\ell\le\rho\).
The exponential is continuously differentiable with bounded derivative on this range. The absolute-continuity chain rule therefore applies to \(S(x)=e^{-A(x)}\), giving the stated derivative.
Since \(S(0)=1\), integrating that derivative gives \(\int_0^\ell\delta_{z(x)}S(x)\,dx=1-S(\ell)\). Subtracting and adding the corresponding term with coefficient \(B\) gives exactly the displayed welfare identity. All integrals are finite.
Assessment: Correct; the calculus hypotheses are satisfied.
Nonnegative fatigue implies \(A(x)\ge\delta_t a_t(x)\), hence \(S(x)\le e^{-\delta_t a_t(x)}\).
The integral substitution is justified by \(a_t'(x)=\mathbf 1_{\{z(x)=t\}}\) almost everywhere and by the chain rule applied to \(\Phi_t(a_t(x))\). Here \(\Phi_t\) is continuously differentiable and \(a_t(0)=0\). Its integrated derivative is exactly \(\Phi_t(a_t)\).
Thus this bound does not require the type’s usage set to be an interval or a finite union of intervals.
Assessment: Correct.
Each integral of \(S\) over a type’s usage set is nonnegative. Consequently, discarding terms whose coefficients \(\bar v_t-B\delta_t\) are negative produces an upper bound. Applying the integral bound to the remaining coefficients is therefore legitimate.
The positive-part equality follows from \(R_t-B(1-C_t)=(\bar v_t-B\delta_t)\Phi_t(a_t)\) and \(\Phi_t(a_t)\ge0\). It also holds when \(a_t=0\).
Applying the proved telescoping inequality gives \(W(z)\le B(2-S(\ell))\le2B\le2\mathrm{OPT}_{\pi}\).
Assessment: Correct; all inequality directions and constants check out.
The argument applies separately to every feasible unrestricted schedule. Although \(B\) depends on that schedule, its upper bound \(\mathrm{OPT}_{\pi}\) is uniform, so taking the supremum is valid.
The proof also covers:
The final observation about at most \(\tau\) blocks correctly describes the constructed ordered schedules. It does not assert a running-time bound.
Assessment: Correct.
The cited [Farina–Gatti Theorem 1](https://www.mit.edu/~gfarina/2017/adopting-cascade-model-truthful-jair17/adopting-cascade-model-truthful-jair17.pdf) states the analogous finite-model half guarantee when all position factors equal one. The prover’s continuous argument is self-contained and does not apply that theorem to measurable schedules.
The output establishes the requested welfare guarantee. It does not classify computational complexity, which the assigned question does not require.
None required. The write-up establishes its claimed conclusion without missing lemmas or additional assumptions.
⟨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.