Answer: —
Theorem 9 — class: algorithmic
Given a succinct feasible set \(S\), a finite type set \(T\) with rational masses \(\mu_t\) summing to \(1\), and nonnegative utilities \(u_t:S\to\mathbb{Q}_{\ge 0}\), define \(Q_x(q)=\inf\{v:\sum_{t:u_t(x)\le v}\mu_t\ge q\}\) for \(0<q\le1\). For \(\alpha\in(0,1]\) and \(\varepsilon\ge0\), seek a feasible \(x\) for which there are no feasible \(y\) and \(q\in(0,1]\) with \(Q_y(r)\ge Q_x(r)\) for every \(0<r<q\) and \(Q_y(q)>(Q_x(q)+\varepsilon)/\alpha\). Can a weighted ordered-tail adaptation of Algorithm 1, using lower-tail integrals \(\int_0^q Q_x(r)\,dr\), return such a solution with the guarantee \((\alpha^2/(1-\alpha+\alpha^2),\,\varepsilon/(1-\alpha+\alpha^2))\) in time polynomial in the decision description, \(\tau=|T|\), and the mass bit length \(L\), given approximate solvers for its ordered-tail subproblems?
A society is given by its support: \(T\) lists the \(\tau\ge1\) types with positive binary-rational masses \(\mu_t\), with \(\sum_t\mu_t=1\); \(\tau\) is the support size, not the number of possible types.
Let \(S\subseteq\mathbb Q^m\) be a nonempty succinctly represented feasible set, with feasible decisions encoded in at most \(B\) bits and polynomial-time evaluable utilities \(u_t:S\to\mathbb Q_{\ge0}\). Let \(N\) be the decision and utility description length and \(L\) the total mass bit length.
Define \(Q_x(q)=\inf\{v\in\mathbb R:\sum_{t:u_t(x)\le v}\mu_t\ge q\}\) for \(0<q\le1\), and \(A_x(q)=\int_0^q Q_x(r)\,dr\), with \(A_x(0)=0\). Equal utilities are pooled; quantiles use this endpoint convention without interpolation.
A feasible \(x\) is \((a,e)\)-approximately leximin-optimal if no \(y\in S\) and \(q\in(0,1]\) satisfy both \(Q_y(r)\ge Q_x(r)\) for every \(0<r<q\) and \(Q_y(q)>(Q_x(q)+e)/a\).
Fix binary-rational \(\alpha\in(0,1]\) and \(\varepsilon\ge0\). An ordered-tail oracle receives rational \(0=q_0<q_1<\cdots<q_k<q\le1\) and bounds \(b_0=0,b_1,\ldots,b_k\in\mathbb Q\), and maximizes \(F(x)=(A_x(q)-b_k)/(q-q_k)\) subject to \(x\in S\) and \(A_x(q_j)\ge b_j\) for \(1\le j\le k\).
On nonempty subproblems with nonnegative optimal value, the oracle returns a feasible \(x\) satisfying \(F(x)\ge\alpha\max F-\varepsilon\), in polynomial time in its encoded input length; feasibility is exact and the returned objective is the actual \(F(x)\).
Can an iterative adaptation using these ordered-tail oracles return an \(\left(\alpha^2/(1-\alpha+\alpha^2),\varepsilon/(1-\alpha+\alpha^2)\right)\)-approximately leximin-optimal decision in time polynomial in \(m,\tau,N,L,B\) and the bit lengths of \(\alpha,\varepsilon\), uniformly over all admissible oracle outputs?
For a finite list of equally weighted agents, the ordered-outcomes iteration obtains exactly these approximation parameters from approximate residual ordered-sum solvers. [Hartman et al.](https://arxiv.org/html/2303.12506v4)
No result settling this positive-rational-mass oracle problem was identified in the literature search.
The requested uniform polynomial-time guarantee remains unresolved. The following result extends the exact-oracle case from the notes to approximate oracles.
Theorem. For every admissible $\alpha>0$ and $\varepsilon\ge0$, the supplied ordered-tail oracle suffices to compute an exactly leximin-optimal decision, uniformly over all admissible oracle outputs, in time polynomial in
$$
m,\tau,N,L,B,\operatorname{bits}(\alpha),\operatorname{bits}(\varepsilon),\frac1\alpha.
$$
Consequently, the requested approximation guarantee is obtainable in polynomial time whenever $1/\alpha$ is polynomially bounded in the input length. In particular, it is obtainable for $\alpha=1$ and arbitrary $\varepsilon$, and for every fixed positive $\alpha$.
The dependence on the numerical value $1/\alpha$ prevents this theorem from settling the general question. The proof below establishes that dependence explicitly.
We use the natural interpretation that each decision encoding determines one decision. Since encodings have length at most $B$, the feasible set is finite. Every nonempty optimization problem considered below therefore attains its optimum.
Write the masses in reduced form as $\mu_t=a_t/d_t$, and define
$$
D=\operatorname{lcm}_{t\in T}d_t,
\qquad
\delta=\frac1D.
$$
Every mass and every sum of masses is an integer multiple of $\delta$. Moreover,
$$
\log_2D\le\sum_{t\in T}\log_2d_t\le L.
$$
Thus $D$ has polynomial encoding length, although its numerical value may be exponential.
Pooling equal utilities, every quantile breakpoint is a cumulative mass of types. The stipulated endpoint convention consequently makes $Q_x$ constant on every cell
$$
((i-1)\delta,i\delta],
\qquad 1\le i\le D.
$$
In particular,
$$
A_x(i\delta)-A_x((i-1)\delta)
=
\delta Q_x(i\delta).
$$
Let $P$ be a polynomial upper bound on the bit lengths of utility numerators and denominators. Such a bound follows from the assumed polynomial-time utility evaluation on decision encodings of length at most $B$. Increase $P$ if necessary so that
$$
0\le u_t(x)\le U:=2^P
$$
for every feasible $x$ and every type $t$. Hence, for $0\le r\le q\le1$,
$$
0\le A_x(q)-A_x(r)\le U(q-r).
$$
We also need a uniform separation bound. Fix a rational $p=a/d\in(0,1]$ in reduced form. If the utility denominators at $x$ are $e_1,\ldots,e_\tau$, the denominator of $A_x(p)$ divides
$$
Dd\prod_{t=1}^{\tau}e_t.
$$
Indeed, its full utility-group contributions have masses with denominator dividing $D$, and its final partial contribution has mass $p-c$, where $c$ has denominator dividing $D$.
Since $e_t\le2^P$, every reduced denominator of $A_x(p)$ is at most
$$
W(p):=Dd\,2^{\tau P}.
$$
Two distinct attainable values of $A_x(p)$ therefore differ by at least
$$
g(p):=\frac1{W(p)^2}.
$$
To justify this, distinct reduced fractions with denominators $v_1,v_2\le W(p)$ differ by a nonzero integer divided by $v_1v_2$.
Both $g(p)$ and all integrals used below have polynomial bit length when $p$ does.
The key new step is to place the objective quantile very close to a retained checkpoint.
Lemma. Let $X$ be a nonempty feasible set defined by ordered-tail constraints whose last checkpoint is $s$, taking $s=0$ when there are no constraints. Suppose a decision $x_0\in X$ is known. For rational $s<r<1$ and $0<\eta\le U$, one can obtain $x\in X$ satisfying
$$
A_x(r)\ge\max_{y\in X}A_y(r)-\eta
$$
using
$$
n=
\left\lceil\frac1\alpha\right\rceil
\left\lceil\log_2\frac{2U}{\eta}\right\rceil
$$
oracle calls. All calls satisfy the oracle promise.
Proof. Put
$$
M=\max_{y\in X}A_y(r),
\qquad
b_0=A_{x_0}(r).
$$
Choose the positive rational
$$
h=
\min\left\{
\frac{1-r}{2},
\frac{\alpha\eta}{2(U+\varepsilon)}
\right\}.
$$
At iteration $j$, retain the original constraints defining $X$, append the checkpoint $r$ with bound $b_j$, and query at $q=r+h$. Let the returned decision be $x_{j+1}$, and set
$$
b_{j+1}=A_{x_{j+1}}(r).
$$
The checkpoint at $r$ is replaced at the next iteration; duplicate checkpoints are never introduced.
The subproblem is nonempty because the preceding decision satisfies its constraints. Its objective is nonnegative for every feasible decision:
$$
A_x(r+h)\ge A_x(r)\ge b_j.
$$
Thus the oracle promise applies.
A maximizer $y$ of $A_y(r)$ over the original set $X$ remains feasible, since $b_j\le M$. Its residual objective is at least $(M-b_j)/h$. Therefore the oracle guarantee gives
$$
A_{x_{j+1}}(r+h)-b_j
\ge
\alpha(M-b_j)-\varepsilon h.
$$
Using the utility upper bound,
$$
b_{j+1}
\ge
b_j+\alpha(M-b_j)-h(U+\varepsilon).
$$
Exact feasibility also gives $b_{j+1}\ge b_j$.
For $G_j=M-b_j$, we obtain
$$
0\le G_{j+1}
\le
(1-\alpha)G_j+h(U+\varepsilon)
\le
(1-\alpha)G_j+\frac{\alpha\eta}{2}.
$$
Since $G_0\le U$, induction yields
$$
G_n\le(1-\alpha)^nU+\frac{\eta}{2}.
$$
For $0<\alpha<1$,
$$
(1-\alpha)^{\lceil1/\alpha\rceil}
\le e^{-1}<\frac12.
$$
For $\alpha=1$, the left side is zero. With the stated choice of $n$,
$$
(1-\alpha)^nU
\le
2^{-\lceil\log_2(2U/\eta)\rceil}U
\le\frac{\eta}{2}.
$$
Hence $G_n\le\eta$, proving the lemma.
The checkpoints $r,r+h$ have polynomial encoding length. Each bound $b_j$ is an actual integral of a returned decision at the fixed rational $r$, so its bit length does not grow with the number of iterations. ∎
Proposition. Suppose $X$ is defined by retained constraints, its last checkpoint is $s<p\le1$, and a decision in $X$ is known. An exact maximizer of $A_x(p)$ over $X$ can be computed with a number of oracle calls polynomial in the encoding lengths and $1/\alpha$.
Apply the lemma with
$$
r=p,
\qquad
\eta=\frac{g(p)}2.
$$
Its output satisfies
$$
0\le\max_{y\in X}A_y(p)-A_x(p)\le\frac{g(p)}2.
$$
If this difference were positive, rational separation would make it at least $g(p)$, a contradiction. Thus $x$ is an exact maximizer.
The oracle cannot put its objective quantile beyond $1$. Instead, perturb the integral being optimized slightly to the left.
Write $g=g(1)$, and choose
$$
\zeta=
\min\left\{
\frac{1-s}{2},
\frac{g}{4U}
\right\},
\qquad
r=1-\zeta.
$$
Then $s<r<1$. Apply the lemma at $r$ with $\eta=g/4$, obtaining $x$ such that
$$
A_x(r)\ge\max_{y\in X}A_y(r)-\frac g4.
$$
Let $y$ maximize $A_y(1)$ over $X$. Since
$$
A_y(r)\ge A_y(1)-U\zeta
$$
and $A_x(1)\ge A_x(r)$, we get
$$
A_x(1)
\ge
A_y(1)-U\zeta-\frac g4
\ge
A_y(1)-\frac g2.
$$
Rational separation at $1$ forces equality. Thus $x$ exactly maximizes $A_x(1)$.
In both cases, the logarithm of the required inverse accuracy is polynomial in $\tau,P,L$ and the checkpoint encoding lengths. The lemma therefore supplies the claimed call bound. ∎
This proposition uses only nonempty subproblems with nonnegative objective. It neither queries an unknown feasibility condition nor relies on oracle behavior outside its promise.
For completeness, the exact-prefix construction from the notes is proved here, with explicit terminal returns.
First obtain a known feasible decision by an unconstrained oracle call at $q=1$. Its objective is nonnegative. Thereafter, use the proposition whenever an exact integral maximizer is required.
Exactly maximize $A_x(\delta)$ over $S$. Since every positive mass is at least $\delta$,
$$
\frac{A_x(\delta)}{\delta}
=
\min_{t\in T}u_t(x).
$$
Let its optimal value be $\delta v$. Retain
$$
A_x(\delta)\ge\delta v,
$$
and put
$$
s=\delta,
\qquad
b=\delta v.
$$
Every retained decision has minimum utility exactly $v$: the constraint gives a minimum at least $v$, and maximality of $v$ gives the reverse inequality.
If $s=1$, return the maximizing decision.
Let $X$ be the set defined by the retained constraints. Maintain:
Initialization establishes these properties.
For $x\in X$, define
$$
c_x=\sum_{t:u_t(x)\le v}\mu_t,
\qquad
c=\min_{x\in X}c_x.
$$
The minimum exists because $X$ is finite and nonempty. Also, $c_x\ge s$, and every $c_x$ is a grid point.
Monotonicity and the endpoint convention give
$$
Q_x(r)=v
\quad\text{for }s<r\le c_x,
$$
and
$$
Q_x(r)>v
\quad\text{for }c_x<r\le1.
$$
For a grid point $q>s$, define
$$
M(q)=\max_{x\in X}A_x(q),
\qquad
H(q)=b+v(q-s).
$$
The proposition computes $M(q)$ exactly. We have
$$
M(q)>H(q)
\quad\Longleftrightarrow\quad
q>c.
$$
Indeed, if $q\le c$, every retained decision has quantile $v$ throughout $(s,q]$, so its integral is $H(q)$. If $q>c$, a decision attaining $c_x=c$ has quantile strictly larger than $v$ on the positive-length interval $(c,q]$, making its integral strictly larger than $H(q)$.
Compute $M(1)$. If $M(1)=H(1)$, then $c=1$ and every decision in $X$ has the same complete quantile function. Return the maximizer obtained in this query.
Otherwise, binary search over grid indices finds the smallest $j$ for which
$$
M(j\delta)>H(j\delta).
$$
The predicate is monotone, and
$$
c=(j-1)\delta.
$$
The search requires $O(1+\log D)$ exact-maximization requests.
Put
$$
s'=j\delta=c+\delta,
\qquad
b'=M(s').
$$
For every $x\in X$, grid constancy gives
$$
A_x(s')
=
b+v(c-s)+\delta Q_x(s').
$$
Consequently, maximizing $A_x(s')$ exactly maximizes $Q_x(s')$ over $X$.
Define
$$
w=\frac{b'-b-v(c-s)}{\delta}.
$$
Since $b'>H(s')$, we have $w>v$.
Append the constraint
$$
A_x(s')\ge b'.
$$
The new feasible set $X'$ contains the returned maximizer. Because $b'$ is the maximum over $X$, every decision in $X'$ has integral exactly $b'$ and hence endpoint utility exactly $w$.
Thus all decisions in $X'$ share the extended prefix: the previous prefix, followed by $v$ through $c$, followed by $w$ on $(c,s']$. Replace the state by
$$
(X,s,b,v)\leftarrow(X',s',b',w).
$$
If $s'=1$, return the retained maximizer immediately. Otherwise begin another phase.
Each successful extension introduces a new, strictly larger utility value on a cell of positive mass. The fixed prefix belongs to every retained decision, and each decision has at most $\tau$ distinct utilities. There can therefore be at most $\tau-1$ successful extensions after initialization.
The total number of exact-maximization requests is
$$
O\bigl(\tau(1+\log D)\bigr).
$$
Let $x^\star$ be the returned decision. Suppose there were $y\in S$ and $q\in(0,1]$ with
$$
Q_y(r)\ge Q_{x^\star}(r)
\quad\text{for every }0<r<q,
$$
and
$$
Q_y(q)>Q_{x^\star}(q).
$$
By common-grid constancy, the first grid cell on which the two quantile functions differ must favor $y$.
Such a first favorable difference is impossible:
These cases cover the entire quantile domain. Thus the alleged first favorable difference cannot exist, and $x^\star$ is exactly leximin-optimal.
The official retained checkpoints are grid points and number at most $\tau$. Their encoding lengths are polynomial in $L$. Their bounds are actual integrals, whose encoding lengths are polynomial in $\tau,P,L$.
Every exact-maximization request uses a polynomial number of approximate-oracle calls times $1/\alpha$, by Sections 2 and 3. Its temporary checkpoints and bounds also have polynomial encoding length. The complete construction therefore has the running time stated in the theorem, uniformly over all admissible oracle outputs.
Set
$$
d_\alpha=1-\alpha+\alpha^2,
\qquad
a=\frac{\alpha^2}{d_\alpha},
\qquad
e=\frac{\varepsilon}{d_\alpha}.
$$
Since $0<a\le1$ and $e\ge0$,
$$
\frac{Q_{x^\star}(q)+e}{a}\ge Q_{x^\star}(q).
$$
Any forbidden witness for the requested parameters would therefore also be a forbidden witness for exact leximin optimality. The constructed decision satisfies the requested guarantee.
The unresolved issue is exclusively the running time when $1/\alpha$ is exponentially large relative to its encoding length.
The dependence on $1/\alpha$ cannot simply be removed from the preceding tightening analysis.
Consider one type of mass $1$, feasible decisions
$$
S=\{0,1,\ldots,M\},
$$
utility $u(j)=j$, and parameters
$$
\alpha=\frac1M,
\qquad
\varepsilon=0.
$$
At a tightening checkpoint $r=1/2$, suppose the current decision is $c<M$ and the bound is $b=rc$. For any permitted $h>0$, the residual objective is
$$
F(j)=\frac rh(j-c)+j.
$$
It is maximized at $j=M$. Nevertheless, returning only $c+1$ is admissible, because
$$
\alpha F(M)
=
\frac rh\left(1-\frac cM\right)+1
\le
\frac rh+1
\le
F(c+1).
$$
It also satisfies the retained constraint exactly as required.
Thus, even arbitrarily small choices of $h$ allow an admissible sequence that advances the decision by only one unit per call. Starting from $c=1$, exact recovery can require $M-1$ such calls, while $\alpha=1/M$ has encoding length logarithmic in $M$.
This example concerns the exact-recovery subroutine, not a lower bound for the task’s weaker approximation target. In fact, the one-type approximation problem is handled by a single unconstrained oracle call. A general solution may therefore need to avoid exact recovery rather than accelerate it.
⟨structured verdict parsed — rendered above⟩
The output establishes a substantive partial result: exact leximin optimization using the supplied approximate oracle in time polynomial in the input lengths and the numerical reciprocal $1/\alpha$. It does not settle the requested running time polynomial in $\operatorname{bits}(\alpha)$. The prover accurately acknowledges this limitation.
The partial theorem is sound in substance. I found one minor domain omission in the tightening lemma and no false central step.
The explicit interpretation that each decision encoding determines one decision makes $S$ finite, since encoding lengths are bounded by $B$. Consequently, every nonempty subproblem attains its optimum. This is consistent with the intended encoding model.
Writing $\mu_t=a_t/d_t$ and taking the least common multiple $D$ correctly makes every cumulative mass a multiple of $\delta=1/D$. The bound
$$
\log_2 D\le \sum_t\log_2 d_t\le L
$$
is valid.
Pooling equal utilities and using the specified endpoint convention correctly gives constancy on
$$
((i-1)\delta,i\delta].
$$
Thus the integral increment identity is valid, including cells whose right endpoint is a quantile breakpoint.
Polynomial-time utility evaluation supplies a polynomial bound on output bit lengths. Enlarging that bound to obtain $u_t(x)\le U=2^P$ is legitimate, and nonnegative utilities give
$$
0\le A_x(q)-A_x(r)\le U(q-r).
$$
For rational $p=a/d$, the proposed denominator bound
$$
Dd\prod_t e_t
$$
is valid for both full-group and partial-group integral contributions. Consequently, distinct attainable values of $A_x(p)$ differ by at least $g(p)=1/W(p)^2$. The separation argument correctly allows different decisions to have different utility denominators.
The claimed polynomial bit lengths follow from the bounds on $D$, $d$, and the utility encodings.
Finding: Correct.
The augmented subproblem remains nonempty because the preceding decision satisfies the new checkpoint bound. Every feasible decision has nonnegative residual objective, so the oracle promise applies.
A maximizer of $A_y(r)$ over the original $X$ remains feasible: every updated bound is an attained value over $X$, hence is at most $M$. The oracle inequality therefore yields the stated bound
$$
A_{x_{j+1}}(r+h)-b_j
\ge \alpha(M-b_j)-\varepsilon h.
$$
Subtracting the tail contribution, bounded by $Uh$, correctly gives
$$
b_{j+1}\ge b_j+\alpha(M-b_j)-h(U+\varepsilon).
$$
Exact checkpoint feasibility also establishes $b_{j+1}\ge b_j$.
The resulting recurrence and its iteration are valid:
$$
G_n\le (1-\alpha)^nU+\frac{\eta}{2}.
$$
For $0<\alpha<1$, the bound
$$
(1-\alpha)^{\lceil1/\alpha\rceil}\le e^{-1}<\frac12
$$
justifies the stated call count. The separate treatment of $\alpha=1$ is correct.
Replacing the temporary checkpoint prevents duplicate checkpoints, and computing each new bound from an actual returned decision prevents iterative growth of its encoding length.
Minor issue: The lemma does not explicitly require $\eta$ to be rational. As stated for arbitrary real $\eta$, its prescribed $h$ need not be rational, although oracle inputs must be rational. Every subsequent application uses rational $\eta$, so this omission does not affect the partial theorem.
Minimum clarification: State that $\eta\in\mathbb Q$.
For $p<1$, the chosen accuracy $g(p)/2$ is strictly below the minimum positive separation between attainable integral values. Hence the returned decision must attain the exact maximum.
For $p=1$, the perturbation satisfies $s<r<1$, and the displayed comparison correctly gives
$$
A_x(1)\ge A_y(1)-\frac g2.
$$
Since both values are attainable at $1$, rational separation forces equality.
The lemma’s accuracy restriction is satisfied in both cases: $W(p)\ge1$, so the chosen accuracies are at most $1$, while $U\ge1$.
The inverse accuracies have polynomial logarithmic size. Thus the claimed dependence on $1/\alpha$, rather than on an exponentially small separation value itself, is justified.
Finding: Correct.
Every positive mass is at least $\delta$, so
$$
A_x(\delta)=\delta\min_t u_t(x).
$$
Exact maximization therefore fixes the largest possible minimum utility. Every retained decision has minimum exactly $v$, establishing the initial invariant.
For later phases, the common prefix and its endpoint value imply $c_x\ge s$. Monotonicity and the endpoint convention justify the claimed plateau through $c_x$ and strict increase after it.
All retained checkpoints remain strictly ordered: the next checkpoint is $c+\delta>s$.
Finding: Correct, including the immediate return when $\delta=1$.
The equivalence
$$
M(q)>H(q)\quad\Longleftrightarrow\quad q>c
$$
is valid. For $q\le c$, every retained decision has the stated plateau. For $q>c$, a decision attaining the minimum $c_x=c$ has strictly larger utility on a positive-length interval.
The predicate is monotone on grid indices. Since $c$ is itself a grid point, the first successful index satisfies $c=(j-1)\delta$. Binary search therefore uses only logarithmically many exact-maximization requests.
At $s'=c+\delta$, every decision shares the prefix through $c$, and grid constancy gives
$$
A_x(s')=b+v(c-s)+\delta Q_x(s').
$$
Thus maximizing the integral maximizes the endpoint utility. Retaining the attained maximum fixes the new endpoint value and the entire next cell.
Finding: Correct.
Each successful extension fixes a strictly larger utility value on a cell of positive mass. Every retained decision realizes all previously fixed levels and has at most $\tau$ distinct utility values. Therefore there are at most $\tau-1$ extensions after initialization.
The first-differing-cell argument matches the task’s definition. A forbidden witness must have a first differing grid cell favoring $y$. Agreement on earlier fixed prefixes places $y$ in the corresponding retained set. The initial maximum, forced plateau, next-cell maximum, or identical terminal suffix rules out that favorable difference.
Both terminal-return cases are covered.
Finding: Correct.
The number of retained checkpoints, their bit lengths, and the integral-bound bit lengths are polynomially bounded. Combining the exact-maximization call count with the phase count proves the stated running time polynomial in the encoded inputs and $1/\alpha$.
The conversion from exact leximin optimality to the requested approximation guarantee is valid because
$$
0<a\le1,\qquad e\ge0,\qquad Q_{x^\star}(q)\ge0,
$$
which imply
$$
\frac{Q_{x^\star}(q)+e}{a}\ge Q_{x^\star}(q).
$$
Major target limitation: Polynomial dependence on $1/\alpha$ does not establish polynomial dependence on $\operatorname{bits}(\alpha)$. The result resolves the stated restricted regimes, including fixed positive $\alpha$, but leaves the general task unresolved.
Minimum additional requirement: Establish the requested encoding-length running time or establish an impossibility result for that target. The present proof supplies neither.
The one-type objective calculation is correct:
$$
F(j)=\frac rh(j-c)+j.
$$
It increases with $j$, so its maximum occurs at $M$. Returning $c+1$ satisfies the retained constraint, and the displayed inequalities correctly verify its admissibility for $\alpha=1/M$ and $\varepsilon=0$.
Thus an admissible sequence can require $M-1$ tightening calls from the stated starting decision. This demonstrates a limitation of the exact-recovery procedure, not a lower bound for the requested weaker approximation guarantee. The prover explicitly makes that distinction.
Finding: Correct and appropriately limited.
⟨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.