Answer: —
Lemma 6 — class: other
PDF text-layer excerpt — equations and symbol order may be approximateFor single resource allocations, the LCP mechanism allocates the resource in the form of the Shortest Job First (SJF) and the allocations are envy-free in expectation. The LCP allocations are envy-free in expectation when allocating multiple resources for two agents.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given a finite set of job types \(T\), rational masses \(\mu_t\geq 0\) with \(\sum_{t\in T}\mu_t=1\), and rational work requirements \(k_t>0\), choose a measurable service rate \(a_t(u,s)\geq 0\) for each \(u\in[0,\mu_t]\) and time \(s\geq 0\). Require \(\sum_{t\in T}\int_0^{\mu_t}a_t(u,s)\,du\leq 1\) at every time and \(\int_0^{T_t(u)}a_t(u,s)\,ds=k_t\), where \(T_t(u)\) is that job's completion time. Minimize \(\sum_{t\in T}\int_0^{\mu_t}\log T_t(u)\,du\).
A society is given by its support: the list of \(\tau\geq1\) 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 work requirement \(k_t>0\). There is one resource, so \(m=1\), with unit capacity; all jobs are available at time zero.
A schedule consists of jointly measurable rates \(a_t:[0,\mu_t]\times[0,\infty)\to[0,\infty)\), locally integrable in time for almost every job, satisfying \(\sum_t\int_0^{\mu_t}a_t(u,s)\,du\leq1\) at every time \(s\). There is no additional pointwise rate bound.
For almost every job, its completion time is the first time \(T_t(u)\in(0,\infty)\) at which \(\int_0^{T_t(u)}a_t(u,s)\,ds=k_t\); service stops thereafter. Integrals over jobs use Lebesgue measure, and schedules may distinguish jobs of the same type.
Define \(V=\inf_a\sum_t\int_0^{\mu_t}\log T_t(u)\,du\), using the natural logarithm and schedules with a well-defined objective. The input also includes a binary-rational threshold \(b\in\mathbb{Q}\); \(L\) is the total input bit length.
Is deciding whether \(V\leq b\) in \(\mathrm{P}\), with running time polynomial in \(m,\tau,L\), or is it \(\mathrm{NP}\)-hard?
For finitely many jobs on one resource, minimizing the product of completion times gives Shortest Job First and is envy-free in expectation under uniform random tie-breaking; with two jobs, product-minimizing allocations are also envy-free in expectation for multiple resources. [Narayana and Kash](https://ojs.aaai.org/index.php/AAAI/article/download/16706/16513)
No result settling this precise mass-based threshold problem was identified in the literature search.
The unrestricted classification remains unresolved here. The additional result proved below is:
For each fixed $\tau$, the threshold problem is in $\mathrm{P}$ for arbitrary rational thresholds $b$.
This extends the fixed-support, fixed-threshold result in the notes. The proof uses a quantitative bound for inhomogeneous linear forms in logarithms. Its running time is polynomial in $L$ when $\tau$ is fixed, but the bound does not give a polynomial running time jointly in $\tau$ and $L$.
I also prove the exact infimum formula and the comparison reductions needed to identify the remaining difficulty.
For the reverse reductions, I interpret “binary-rational” as a rational represented by a binary numerator and denominator.
The infimum formula, equality algorithm, approximation algorithm, and fixed-$\tau$ polynomial-time result also apply if “binary-rational” means a dyadic rational. The reverse reductions below need not preserve dyadic inputs; I explicitly delimit those conclusions.
All complexity statements use the ordinary bit model of computation.
Sort the supported types so that
$$
k_1\leq k_2\leq\cdots\leq k_\tau.
$$
Define
$$
P_0=C_0=0,\qquad
P_i=\sum_{j=1}^i\mu_j,\qquad
C_i=\sum_{j=1}^i\mu_jk_j.
$$
Represent the population by $(0,1)$, placing type $i$ on $(P_{i-1},P_i)$. Write $k(x)=k_i$ on that interval, and define
$$
W(q)=\int_0^q k(x)\,dx.
$$
Thus
$$
W(q)=C_{i-1}+k_i(q-P_{i-1})
\quad\text{for }P_{i-1}\leq q\leq P_i.
$$
Because every $k_i$ is positive, $W$ is continuous and strictly increasing.
If $E$ is a measurable set of jobs of mass $q$, then
$$
\int_E k(x)\,dx\geq W(q).
$$
For $0<q<1$, put $I=(0,q)$. Since $k$ is nondecreasing, there is a number $\kappa$ such that $k\leq\kappa$ almost everywhere on $I$ and $k\geq\kappa$ almost everywhere outside $I$. Consequently,
$$
(k-\kappa)(\mathbf 1_E-\mathbf 1_I)\geq0
$$
almost everywhere: on $I$ both factors are nonpositive, and outside $I$ both are nonnegative. Integrating and using $\lambda(E)=\lambda(I)$ gives
$$
\int_E k-\int_I k
=
\int_0^1(k-\kappa)(\mathbf 1_E-\mathbf 1_I)\,dx
\geq0.
$$
The cases $q=0,1$ follow directly.
For an admissible schedule, write
$$
A(x,s)=\int_0^s a(x,r)\,dr,\qquad
F(s)=\lambda\{x:T(x)\leq s\}.
$$
We disregard the null set on which the jobwise assumptions fail. Joint measurability makes $A$ measurable; its jobwise continuity and monotonicity make the completion time $T$ measurable.
Every job completed by time $s$ has received its required work. Tonelli’s theorem and the capacity constraint therefore give
$$
\begin{aligned}
\int_{\{T\leq s\}}k(x)\,dx
&\leq \int_0^1 A(x,s)\,dx\\
&=\int_0^s\int_0^1a(x,r)\,dx\,dr\\
&\leq s.
\end{aligned}
$$
The minimum-work inequality implies
$$
W(F(s))\leq s.
$$
Let
$$
Q(q)=\inf\{s\geq0:F(s)\geq q\},
\qquad 0<q<1.
$$
Whenever $F(s)\geq q$, we have
$$
s\geq W(F(s))\geq W(q).
$$
Taking the infimum yields
$$
Q(q)\geq W(q).
$$
The right continuity of $F$ gives
$$
\lambda\{q:Q(q)\leq s\}=F(s),
$$
so $Q$, evaluated at a uniform point of $(0,1)$, has the same distribution as $T$.
Put $k_{\min}=\min_i k_i$. Since
$$
Q(q)\geq W(q)\geq k_{\min}q,
$$
the negative parts of $\log Q$ and $\log W$ are integrable. Also, $W(q)\leq C_\tau$, so the positive part of $\log W$ is bounded. Thus, including schedules whose positive objective is infinite,
$$
\int_0^1\log T(x)\,dx
=
\int_0^1\log Q(q)\,dq
\geq
\int_0^1\log W(q)\,dq.
$$
In particular, no admissible schedule has objective $-\infty$.
Fix a positive integer $N$. Divide each type into $N$ batches of mass $\mu_i/N$. Process these batches consecutively in increasing type order.
A type-$i$ batch is processed for
$$
d_i=\frac{\mu_i k_i}{N}
$$
units of time. During its processing interval, every job in that batch receives rate $N/\mu_i$, and every other job receives rate zero. Its aggregate rate is exactly one, and each job receives
$$
\frac{N}{\mu_i}d_i=k_i.
$$
Half-open processing intervals ensure capacity feasibility at every time. These rates are jointly measurable, locally integrable, and stop after completion.
Batch $j$ of type $i$ completes at
$$
C_{i-1}+\frac{j\mu_i k_i}{N}.
$$
Its completion-time quantile $Q_N$ therefore satisfies, almost everywhere,
$$
W(q)\leq Q_N(q)\leq C_\tau,\qquad
Q_N(q)-W(q)\leq
\frac{\max_i\mu_i k_i}{N}.
$$
Hence $Q_N(q)\to W(q)$ for every $q>0$, apart from immaterial interval-endpoint conventions. Moreover,
$$
|\log Q_N(q)|
\leq |\log W(q)|+|\log C_\tau|.
$$
The right side is integrable. Dominated convergence proves
$$
\lim_{N\to\infty}\int_0^1\log Q_N(q)\,dq
=
\int_0^1\log W(q)\,dq.
$$
Combining the lower bound and this construction gives the exact infimum:
$$
\boxed{V=\int_0^1\log W(q)\,dq.}
$$
On the interval for type $i$, substitute $z=W(q)$, so $dz=k_i\,dq$. Using the continuous extension $z\log z=0$ at $z=0$,
$$
V=
\sum_{i=1}^{\tau}\frac{
C_i\log C_i-C_i-C_{i-1}\log C_{i-1}+C_{i-1}
}{k_i}.
$$
The nonlogarithmic terms sum to
$$
-\sum_{i=1}^{\tau}\frac{C_i-C_{i-1}}{k_i}
=-\sum_{i=1}^{\tau}\mu_i=-1.
$$
Define
$$
c_i=C_i\left(\frac1{k_i}-\frac1{k_{i+1}}\right)
\quad (i<\tau),
\qquad
c_\tau=\frac{C_\tau}{k_\tau}.
$$
Collecting the logarithmic terms gives
$$
\boxed{V=-1+\sum_{i=1}^{\tau}c_i\log C_i.}
$$
The sorted requirements imply $c_i\geq0$, and telescoping gives
$$
\sum_{i=1}^{\tau}c_i
=
\sum_{i=1}^{\tau}\frac{C_i-C_{i-1}}{k_i}
=1.
$$
Sorting and computing these rationals takes polynomial time in $L$. Their bit lengths are polynomially bounded: the denominators in each rational sum can be bounded by products of the participating denominators, whose bit lengths add. Subsequent products, differences, and reciprocals preserve polynomial bit length.
This computes an exact expression for $V$. Deciding its comparison with $b$ requires further work.
Choose a positive integer $D$ clearing the denominators of all $c_i$ and of $b+1$. If $V=b$, then
$$
\prod_i C_i^{Dc_i}=\exp(D(b+1)).
$$
The left side is rational. If $b+1\neq0$, then $D(b+1)$ is a nonzero integer.
The Hermite–Lindemann theorem states that $\exp(\alpha)$ is transcendental whenever $\alpha$ is a nonzero algebraic number. Its hypotheses apply to this integer, contradicting rationality of the left side. Thus
$$
V=b\quad\Longrightarrow\quad b=-1.
$$
This standard theorem follows from the Lindemann–Weierstrass theorem; a self-contained proof of the latter is given by [Popescu](https://arxiv.org/abs/2306.14352).
At $b=-1$, write $C_i=p_i/q_i$ in positive integers and choose $D$ clearing the coefficient denominators. Put $n_i=Dc_i$. Then
$$
V=-1
\quad\Longleftrightarrow\quad
\prod_i p_i^{n_i}=\prod_i q_i^{n_i}.
$$
The bases and exponents have polynomial-size binary encodings, although expanding the products could take exponential space.
Here is a polynomial-time equality algorithm that avoids expansion.
Represent the two products by lists of pairs $(a,e)$, with integer base $a>1$ and positive integer exponent $e$. Discard unit bases and zero exponents. Whenever a left pair $(a,e)$ and a right pair $(b,f)$ have
$$
g=\gcd(a,b)>1,
$$
replace their contribution using
$$
\frac{a^e}{b^f}
=
\frac{(a/g)^e}{(b/g)^f}\,g^{e-f}.
$$
Place $g^{e-f}$ on the appropriate side, and discard any new unit bases or zero exponents.
To bound the number of steps, let
$$
\Phi=\sum_{\text{both lists}}\log_2 a,
$$
counting every listed base separately. If $e\neq f$, a replacement decreases $\Phi$ by $\log_2 g\geq1$. If $e=f$, it decreases $\Phi$ by $2\log_2 g\geq2$. Therefore there are at most the initial $\Phi$ steps, which is bounded by the total input length of the bases.
Each step increases the number of pairs by at most one. No base exceeds the largest original base. If $E$ denotes the sum of all exponents in both lists, then a step replaces $e+f$ by at most
$$
e+f+|e-f|\leq2(e+f).
$$
Thus $E$ increases by at most a factor of two per step. Since there are polynomially many steps, all exponent bit lengths remain polynomial. Euclidean gcd computations and the other integer operations consequently take polynomial time.
At termination, every left base is coprime to every right base. The two products are then coprime integers, so they are equal precisely when both lists are empty.
This proves a polynomial-time equality test for every scheduling instance, with unrestricted $\tau$.
For completeness, the precision needed later can be computed efficiently.
For a positive rational $r$ of bit length $h$, write
$$
r=2^z y,\qquad 1\leq y<2,
$$
where $|z|=O(h)$. Put
$$
v=\frac{y-1}{y+1},
$$
so $0\leq v<1/3$. Integrating the geometric series for $2/(1-v^2)$ gives
$$
\log y=
2\sum_{\ell=0}^{M-1}\frac{v^{2\ell+1}}{2\ell+1}+E_M,
$$
with
$$
0\leq E_M\leq
\frac{2v^{2M+1}}{(2M+1)(1-v^2)}.
$$
The same formula computes $\log2$ using $v=1/3$.
Because
$$
\log r=z\log2+\log y,
$$
choosing
$$
M=O(p+\log(h+1))
$$
suffices to obtain error at most $2^{-p}$. The finite rational sums have polynomial bit length in $h$ and $M$, so their exact evaluation takes polynomial time.
Since $c_i\geq0$ and $\sum_i c_i=1$, approximating every $\log C_i$ to error $2^{-p}$ approximates $V$ to the same error. Hence:
An additive approximation to $V$ with error at most $2^{-p}$ is computable in time polynomial in $L$ and $p$.
This alone does not bound the precision needed for exact threshold decision.
For a rational $r=p/q$ in lowest terms, define its height as
$$
H(r)=\max\{|p|,q\}.
$$
Theorem 1 of [Cijsouw and Waldschmidt, *Linear forms and simultaneous approximations*](https://www.numdam.org/item/CM_1977__34_2_173_0.pdf) has the following rational specialization.
For each $n\geq1$, there is an effectively computable constant $K_n>0$. Let $\alpha_j>0$ and $\beta_0,\ldots,\beta_n$ be rational. Choose $A_j\geq6$ bounding both $H(\alpha_j)$ and $\exp(|\log\alpha_j|)$, and $B\geq6$ bounding all $H(\beta_j)$. Put
$$
\Lambda=\beta_0+\sum_{j=1}^n\beta_j\log\alpha_j,
\qquad
\Omega=\prod_{j=1}^n\log A_j.
$$
If $\Lambda\neq0$, then
$$
|\Lambda|>
\exp\!\left(
-K_n\Omega(\log\Omega)(\log B+\log\Omega)
\right).
$$
Here the algebraic-degree parameter in their theorem is $1$.
Apply the theorem with
$$
n=\tau,\qquad
\alpha_i=C_i,\qquad
\beta_i=c_i,\qquad
\beta_0=-(b+1).
$$
Then
$$
\Lambda=V-b.
$$
All $\alpha_i$ are positive rationals, and all coefficients are rational, so the degree and positivity hypotheses hold. Zero coefficients and bases equal to one are allowed in the stated theorem.
Let $h\geq3$ be an integer bounding the numerator and denominator bit lengths of every $C_i$, $c_i$, and $b+1$. Section 3 proves that $h$ is polynomially bounded in $L$. In particular,
$$
H(C_i),H(c_i),H(b+1)\leq2^h
$$
and
$$
\exp(|\log C_i|)=\max\{C_i,C_i^{-1}\}\leq2^h.
$$
We may therefore take
$$
A_i=B=2^{h+3}.
$$
Set $u=(h+3)\log2$. Then $1<u<h+3$, and
$$
\Omega=u^\tau,\qquad
\log\Omega=\tau\log u.
$$
Using $\log u<h+3$ gives
$$
\Omega(\log\Omega)(\log B+\log\Omega)
<
\tau(\tau+1)(h+3)^{\tau+2}.
$$
Choose an effectively computable integer $M_\tau\geq K_\tau$, and define
$$
R=M_\tau\tau(\tau+1)(h+3)^{\tau+2}.
$$
Whenever $V\neq b$, the theorem yields
$$
|V-b|>\exp(-R).
$$
Since $\log2>1/2$, the integer
$$
p=2R+3
$$
satisfies
$$
2^{-p}<\exp(-R)<|V-b|.
$$
First use Section 4 to test whether $V=b$. If equality holds, answer yes.
Otherwise compute $\widehat V$ with
$$
|\widehat V-V|\leq2^{-(p+2)}.
$$
The proved separation implies that $\widehat V-b$ has the same sign as $V-b$. Its rational sign therefore decides the instance.
For fixed $\tau$, $M_\tau$ is a constant and $p$ is polynomial in $h$, hence polynomial in $L$. Section 5 computes the required approximation in polynomial time. This proves
$$
\boxed{\text{For every fixed }\tau,\text{ arbitrary rational thresholds are decidable in }\mathrm{P}.}
$$
More explicitly, the proof gives a uniform running-time bound of the form
$$
f(\tau)L^{O(\tau)}
$$
for an effectively computable function $f$. This is not a polynomial bound jointly in $\tau$ and $L$.
There is also a polynomial-time subclass with unrestricted $\tau$: suppose every cumulative work value is a power of two,
$$
C_i=2^{z_i},\qquad z_i\in\mathbb Z.
$$
This property and the exponents $z_i$ can be computed from the rational encodings in polynomial time. Then
$$
V=-1+\gamma\log2,\qquad
\gamma=\sum_i c_i z_i\in\mathbb Q.
$$
The rational $\gamma$ has polynomial bit length. If $\gamma=0$, comparison is rational. Otherwise, applying the preceding quantitative theorem with only one logarithm gives polynomial-time decision, regardless of the number of supported types.
This section assumes general binary numerator-and-denominator rational inputs.
Define rational logarithmic comparison to be the following decision problem: given rational coefficients $\alpha_j$, positive rational bases $r_j$, and a rational $d$, decide whether
$$
\sum_j\alpha_j\log r_j\leq d.
$$
The value formula gives a polynomial-time reduction from scheduling threshold decision to this problem:
$$
V\leq b
\quad\Longleftrightarrow\quad
\sum_i c_i\log C_i\leq b+1.
$$
The converse follows from an exact realization.
Let
$$
0<R_1<\cdots<R_n
$$
be positive rationals, and let positive rational weights $w_i$ sum to one. Define
$$
R_0=0,\qquad
h_i=\sum_{j=i}^n\frac{w_j}{R_j},\qquad
k_i=\frac1{h_i},\qquad
\mu_i=(R_i-R_{i-1})h_i.
$$
All masses and requirements are positive. Also,
$$
h_i-h_{i+1}=\frac{w_i}{R_i}>0,
$$
so $k_1<\cdots<k_n$.
The total mass is
$$
\begin{aligned}
\sum_i\mu_i
&=\sum_i(R_i-R_{i-1})\sum_{j=i}^n\frac{w_j}{R_j}\\
&=\sum_j\frac{w_j}{R_j}\sum_{i=1}^j(R_i-R_{i-1})\\
&=\sum_j w_j=1.
\end{aligned}
$$
Its cumulative work satisfies
$$
C_i=\sum_{\ell=1}^i\mu_\ell k_\ell
=\sum_{\ell=1}^i(R_\ell-R_{\ell-1})
=R_i.
$$
Therefore its value coefficients are
$$
c_i=R_i(h_i-h_{i+1})=w_i\quad(i<n),
\qquad
c_n=R_nh_n=w_n.
$$
Its infimum is exactly
$$
V=-1+\sum_iw_i\log R_i.
$$
The construction has polynomial output bit length: each $h_i$ is a sum of at most $n$ explicitly represented rationals, and the subsequent reciprocals and products have polynomial-size numerator and denominator representations.
For a general expression
$$
S=\sum_j\alpha_j\log r_j,
$$
discard zero terms. Replace each term with negative coefficient by
$$
\alpha_j\log r_j=|\alpha_j|\log(1/r_j).
$$
Combine equal bases, discard bases equal to one, and sort. All remaining coefficients are positive.
If their sum is $H>0$, normalize them by $H$ and apply the realization construction. It produces
$$
V=-1+\frac{S}{H}.
$$
Choosing
$$
b=-1+\frac dH
$$
gives
$$
V\leq b\quad\Longleftrightarrow\quad S\leq d.
$$
If no terms remain, $S=0$ and rational comparison decides the source instance; it can be mapped to a fixed yes-instance or no-instance.
Thus
$$
\boxed{
\text{Scheduling threshold decision is polynomial-time equivalent to rational logarithmic comparison.}
}
$$
For positive integers and binary-encoded nonnegative integer exponents,
$$
X=\prod_i A_i^{e_i},\qquad
Y=\prod_j B_j^{f_j},
$$
we have
$$
X\leq Y
\quad\Longleftrightarrow\quad
\sum_i e_i\log A_i-\sum_j f_j\log B_j\leq0.
$$
The preceding reduction produces a scheduling instance with $b=-1$.
Conversely, at $b=-1$, clearing coefficient denominators gives
$$
V\leq-1
\quad\Longleftrightarrow\quad
\prod_i p_i^{Dc_i}\leq\prod_i q_i^{Dc_i},
$$
where $C_i=p_i/q_i$. All bases and exponents have polynomial-size binary encodings.
Therefore the scheduling problem restricted to $b=-1$ is polynomial-time equivalent to comparison of products of powers.
The realization does not always produce dyadic requirements. For example,
$$
R_1=1,\quad R_2=2,\quad w_1=w_2=\frac12
$$
gives
$$
h_1=\frac34,\qquad k_1=\frac43.
$$
Consequently, the reverse-equivalence conclusions above have not been proved for dyadic-only inputs. The earlier analytic and algorithmic results do apply to those inputs.
The exact optimization value and polynomial-time equality test are established. The new quantitative argument settles arbitrary rational thresholds for every fixed support size.
For growing $\tau$, however, the proved precision bound contains both the parameter-dependent constant $M_\tau$ and a power of $h$ whose exponent grows with $\tau$. It does not establish the requested uniform polynomial-time bound.
The reductions identify an exact arithmetic comparison problem; they do not establish $\mathrm{NP}$-hardness. Accordingly, neither alternative in the unrestricted target question is proved here.
⟨structured verdict parsed — rendered above⟩
Assessment: correct partial progress; the unrestricted task remains unresolved. The infimum formula, equality test, approximation algorithm, fixed-support decision result, and qualified comparison reductions withstand verification. No central false step was found. The output explicitly acknowledges that it proves neither a running time polynomial jointly in $\tau,L$ nor $\mathrm{NP}$-hardness.
There is one minor indexing omission in the realization construction. The principal obstacle is incompleteness relative to USER_TASK, rather than an error in the established results.
The prover distinguishes general rationals encoded by binary numerators and denominators from dyadic rationals. This distinction is relevant: the reverse realization construction involves reciprocals that need not be dyadic.
The restriction is stated explicitly and maintained through the conclusions. Consequently:
The output uses the number of supported types throughout. It does not substitute the number of possible types or introduce unsupported types with zero mass.
Representing the population by $(0,1)$ preserves its measure and type requirements. Discarding interval endpoints is legitimate because they form a null set.
The function $W$ is continuous and strictly increasing because every supported requirement is positive. Its piecewise formula is correct, including at type boundaries.
The minimum-work argument is valid. A separating value $\kappa$ exists because $k$ is nondecreasing. The signs of both factors in
$$
(k-\kappa)(\mathbf 1_E-\mathbf 1_I)
$$
are correctly identified on $I$ and its complement. Equal measures cancel the constant term upon integration. The cases of mass zero and mass one are immediate and are explicitly covered.
The measurability assertions are justified by the stated assumptions. Joint measurability gives measurable accumulated service; jobwise continuity and monotonicity make the completion-time level sets measurable after disregarding the exceptional null set.
The capacity calculation is correct. Nonnegativity permits Tonelli’s theorem, and each completed job contributes its required work. Hence
$$
W(F(s))\leq s.
$$
This uses only aggregate capacity and does not assume a pointwise rate bound.
The quantile argument is also valid. Monotonicity of $W$ gives
$$
Q(q)\geq W(q).
$$
Right continuity of the completion-time distribution gives the stated equality of distributions. Almost-everywhere finite completion ensures that the quantile is finite for $0<q<1$.
The logarithmic integrability argument handles the singularity near zero correctly. The bound
$$
Q(q)\geq W(q)\geq k_{\min}q
$$
controls the negative parts by an integrable logarithmic function. The positive part of $\log W$ is bounded. Thus the objective comparison is meaningful even when a schedule has infinite positive objective, and the exclusion of objective $-\infty$ follows.
The batch construction is feasible under the task’s absence of a pointwise rate bound. Its aggregate rate, processing duration, and total service per job are calculated correctly.
Half-open processing intervals ensure capacity feasibility at every time, including transitions. The first batch completes at a strictly positive time. Every job completes after finite time, and service stops thereafter.
The quantile error bound is correct:
$$
0\leq Q_N(q)-W(q)\leq \frac{\max_i\mu_i k_i}{N}.
$$
The displayed dominating function is integrable and bounds $|\log Q_N|$. Dominated convergence therefore applies.
Conclusion: the exact infimum formula
$$
V=\int_0^1\log W(q)\,dq
$$
is established. The prover correctly proves an infimum through a sequence of feasible schedules without claiming attainment.
The substitution on each type interval is correct. The convention at zero properly handles the initial endpoint.
The nonlogarithmic terms sum to $-1$, and collecting adjacent logarithmic terms yields the stated coefficients:
$$
V=-1+\sum_i c_i\log C_i.
$$
Sorting gives $c_i\geq0$, including zero coefficients for equal adjacent requirements. The identity
$$
\sum_i c_i=1
$$
is correctly obtained by telescoping.
The polynomial bit-length justification is sufficient. Rational sums can use denominator products whose bit lengths add, and the polynomial number of subsequent arithmetic operations preserves polynomial-size encodings. This establishes an efficiently computable symbolic expression, not an exact threshold decision by itself.
Clearing coefficient and threshold denominators is legitimate. If $V=b$, the resulting product is rational, whereas the exponential argument is a nonzero integer when $b\neq-1$.
The stated Hermite–Lindemann theorem applies exactly to that argument. Its hypotheses and the contradiction are correct. The cited [Popescu paper](https://arxiv.org/abs/2306.14352) states the underlying Lindemann–Weierstrass theorem.
Thus the implication
$$
V=b\Longrightarrow b=-1
$$
is established.
The gcd replacement preserves the quotient of the two encoded products.
The potential-function calculation is correct: a replacement decreases the sum of base logarithms by at least one. Consequently, only polynomially many replacements occur, regardless of the numerical magnitudes of the exponents.
The bounds on list length, base sizes, and exponent bit lengths are sufficient. Scanning the polynomial-size lists for eligible pairs also takes polynomial time.
At termination, the two products are coprime. They can be equal only if both equal one, which is equivalent to both lists being empty after the stated preprocessing.
Conclusion: unrestricted-support equality testing is established. This does not establish unrestricted-support order comparison.
The logarithmic series and remainder estimate are correct on the stated range, including the endpoint used to approximate $\log2$.
The factor multiplying the approximation to $\log2$ is accounted for by the extra logarithmic dependence on the input height. The finite rational sums have bit lengths polynomial in the input size and number of terms.
Because the coefficients are nonnegative and sum to one, the error in the value is bounded by the maximum individual logarithm error.
Conclusion: additive approximation in time polynomial in $L,p$ is established. The prover correctly distinguishes this from determining how much precision exact comparison requires.
I checked the original theorem page in [Cijsouw and Waldschmidt, *Linear forms and simultaneous approximations*](https://www.numdam.org/item/CM_1977__34_2_173_0.pdf). The rational specialization in the output matches its inhomogeneous lower bound. The theorem permits degree one and does not require nonzero logarithms or nonzero coefficients.
The application satisfies its hypotheses: positive rational bases supply real logarithms, rational coefficients have degree at most one, and the selected height bounds also bound the exponential magnitudes of the logarithms.
The subsequent estimates are correct:
$$
\Omega=u^\tau,\qquad \log\Omega=\tau\log u,
$$
and the proposed polynomial expression in $h$ bounds the exponent for fixed $\tau$.
The choice of precision ensures an approximation error strictly smaller than the separation from the threshold. Testing equality first handles the zero case, so the rational approximation determines the correct sign.
Conclusion: polynomial-time threshold decision for every fixed $\tau$ is established. The effective constants also justify the stated parameter-dependent uniform bound. That bound is not polynomial jointly in $\tau,L$.
The unrestricted-support subclass with all cumulative works powers of two is also correctly handled: its value expression reduces to one logarithm with polynomial-size rational coefficients.
The masses and requirements are positive. The mass normalization and cumulative-work calculations are correct. The recovered value coefficients equal the prescribed weights.
The output-size argument is sufficient, so this is a polynomial-time realization for general rational inputs.
Minor issue: the statement
$$
h_i-h_{i+1}=\frac{w_i}{R_i}>0
$$
does not specify $i<n$, although $h_{n+1}$ has not been defined. Its intended range is evident from the adjacent-ordering conclusion and the later separate treatment of the last coefficient.
Minimum clarification: specify $1\leq i<n$ in that statement.
Replacing negative coefficients by positive coefficients on reciprocal bases preserves the expression. Combining equal bases, removing unit bases, normalizing by the positive coefficient sum, and transforming the threshold all preserve the decision.
The empty-expression case is explicitly handled. No unsupported zero-mass types are introduced.
The resulting polynomial-time equivalence with rational logarithmic comparison is established under the declared general-rational encoding.
Both reductions at threshold $b=-1$ preserve polynomial-size binary encodings of bases and exponents. The equivalence with comparison of products of powers is established for general rational scheduling inputs.
The dyadic counterexample is calculated correctly. It demonstrates why the particular reverse construction does not preserve dyadic inputs; the prover appropriately avoids claiming that it does.
Major issue relative to the assigned target: neither requested unrestricted complexity alternative is established.
The fixed-support theorem cannot supply the requested joint polynomial bound because its precision bound has an exponent depending on $\tau$. The comparison reductions identify equivalent arithmetic problems but establish no hardness result. Under dyadic-only encoding, the reverse equivalences are additionally unavailable.
This is an acknowledged limitation, not a concealed logical leap. No expositional clarification can turn the current partial results into a resolution of USER_TASK; further mathematics is required.
The minimum repair to the existing write-up is the indexing clarification above. Completing the assignment requires an unrestricted polynomial-time decision argument or an appropriate hardness proof for the intended input encoding.
⟨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.