Answer: Polynomial-time solvable in \(m,\tau,L\), by exact rational linear programming.
Theorem 3.1(i) — class: hardness
Given a finite support \(T\) of equal-sized district patterns with rational masses \(\mu_t\) summing to \(1\), true and reported vote-share vectors \(q_t,\tilde q_t\in\Delta_m\), a recount budget \(\beta\), target \(a\), tie-breaking order, and reported-profile winner \(b\ne a\), decide whether there are masses \(x_t\in[0,\mu_t]\) with \(\sum_t x_t\le\beta\) such that \(S_c(x)=\sum_t((\mu_t-x_t)\tilde q_{tc}+x_tq_{tc})\) makes \(a\) the winner under that order.
A society is given by its support: a nonempty list \(T\) of \(\tau\) district types with positive binary-rational masses \(\mu_t\), summing to \(1\). Here \(\tau=|T|\) is the support size, not the number of possible types.
Let \(C\) be the candidate set, \(|C|=m\ge3\). Each type represents districts of the same positive size and specifies true and reported vote-share vectors \(q_t,\tilde q_t\in\mathbb Q_{\ge0}^m\), each with coordinate sum \(1\).
The input also specifies a binary-rational recount budget \(\beta\in[0,1]\), a strict linear tie-breaking order \(\succ\) on \(C\), and a target \(a\in C\). The reported-profile Plurality winner is \(b\ne a\); there is no promise that \(a\) wins the true profile.
A recount chooses real masses \(0\le x_t\le\mu_t\) with \(\sum_{t\in T}x_t\le\beta\), restoring the true shares on that mass of districts. The resulting score is \(S_c(x)=\sum_{t\in T}((\mu_t-x_t)\tilde q_{tc}+x_tq_{tc})\).
Candidate \(a\) wins precisely when \(S_a(x)>S_c(x)\) for every \(c\succ a\), and \(S_a(x)\ge S_c(x)\) for every other \(c\ne a\). Let \(L\) be the total binary input bit length; state running times in \(m,\tau,L\).
Is deciding whether such a recount makes \(a\) win solvable in polynomial time in \(m,\tau,L\), or is it NP-hard?
Discrete Plurality recounting with indivisible districts and binary vote counts is NP-complete even for \(m=3\), without an equal-district-size restriction. [Source](https://www.ijcai.org/proceedings/2019/0037.pdf)
No published result settling exactly the continuous problem defined here was identified in the search.
The problem is solvable in polynomial time in \(m,\tau,L\). The proof uses a rational linear program with \(\tau+1\) variables. Strict tie-breaking inequalities are handled by maximizing a common positive margin.
For each candidate \(c\ne a\), define the reported score difference
\(r_c=\sum_{t\in T}\mu_t(\tilde q_{ta}-\tilde q_{tc})\)
and the change in that difference per unit of recounted mass
\(d_{tc}=(q_{ta}-\tilde q_{ta})-(q_{tc}-\tilde q_{tc}).\)
Expanding the given score formula yields
\(S_a(x)-S_c(x)=r_c+\sum_{t\in T}d_{tc}x_t.\)
Thus every score comparison is an affine inequality in the \(\tau\) recount variables.
Let \(H=\{c\in C\setminus\{a\}:c\succ a\}\) and \(K=C\setminus(H\cup\{a\})\). A feasible recount makes \(a\) win exactly when these differences are positive for candidates in \(H\) and nonnegative for candidates in \(K\).
Introduce a variable \(\varepsilon\). Maximize \(\varepsilon\) subject to:
All constraints are non-strict linear inequalities with rational coefficients.
This program has \(\tau+1\) variables and \(2\tau+m+2\) inequalities. Its feasible region is closed and contained in the bounded box
\(\left(\prod_{t\in T}[0,\mu_t]\right)\times[0,1].\)
Consequently, if the program is feasible, its maximum is attained. Denote the maximum by \(\varepsilon^\star\).
Claim. A recount making \(a\) win exists if and only if the linear program is feasible and \(\varepsilon^\star>0\).
Forward direction. Suppose \(x\) is a feasible recount making \(a\) win.
If \(H\ne\varnothing\), define
\(\varepsilon=\min\left(\{1\}\cup\{S_a(x)-S_c(x):c\in H\}\right).\)
Every difference appearing in this finite minimum is strictly positive, so \(0<\varepsilon\le1\). The score constraints for \(H\) hold by the definition of the minimum. Those for \(K\) hold because \(a\) wins. The remaining constraints hold because \(x\) is a feasible recount. Hence \((x,\varepsilon)\) is feasible, and \(\varepsilon^\star\ge\varepsilon>0\).
If \(H=\varnothing\), choose \(\varepsilon=1\). There are no score constraints involving \(\varepsilon\), and every required comparison is nonnegative. Thus \((x,1)\) is feasible, again giving \(\varepsilon^\star>0\).
Reverse direction. Suppose the program is feasible and \(\varepsilon^\star>0\). Let \((x^\star,\varepsilon^\star)\) attain its maximum.
The bounds and budget constraint make \(x^\star\) a feasible recount. For each \(c\in H\),
\(S_a(x^\star)-S_c(x^\star)\ge\varepsilon^\star>0.\)
For each \(c\in K\),
\(S_a(x^\star)-S_c(x^\star)\ge0.\)
These are precisely the stated winning conditions for \(a\). This proves the claim.
In particular, merely testing the feasibility of all comparisons after replacing strict inequalities by non-strict ones would be insufficient. Testing whether the optimal margin is positive preserves the tie-breaking rule exactly.
We use the standard rational linear programming theorem: a linear program with binary-encoded rational coefficients can be solved in deterministic time polynomial in its number of variables, number of constraints, and total encoding length. The algorithm detects infeasibility and, when a finite optimum is attained, can return an exact rational optimum and an optimal rational solution. Polynomial-time rational linear programming follows from the ellipsoid method. [Khachiyan, *Polynomial algorithms in linear programming*](https://www.mathnet.ru/php/archive.phtml?jrnid=zvmmf&option_lang=eng&paperid=5239&wshow=paper).
Here its hypotheses hold: all coefficients are rational, the constraints and objective are linear, and every feasible instance of the constructed program has an attained finite optimum.
We must also check that constructing the program does not cause excessive coefficient growth. Each \(d_{tc}\) is a signed sum of four input rationals. Each \(r_c\) is a sum of products of input rationals. For a fixed \(c\), a common denominator can be obtained by multiplying the denominators of the masses and the two relevant reported coordinates for every type. The sum of their binary lengths is \(O(L)\), so this denominator has \(O(L)\) bits.
Moreover, \(|r_c|\le1\): it is a weighted sum, with weights summing to \(1\), of differences in \([-1,1]\). Thus the corresponding numerator also has \(O(L)\) bits. The same polynomial bound holds for every coefficient of the program. These coefficients can be computed by exact rational arithmetic in polynomial time.
A dense encoding of the resulting program therefore has length
\(B=O((m+\tau)(\tau+1)L).\)
The decision algorithm constructs the program, solves it exactly, rejects if it is infeasible, and otherwise accepts exactly when its rational optimum satisfies \(\varepsilon^\star>0\). The final comparison is an exact sign test on a rational number; no numerical tolerance is needed.
Its running time is
\(\operatorname{poly}\!\left(\tau+1,\;2\tau+m+2,\;(m+\tau)(\tau+1)L\right),\)
which is polynomial in \(m,\tau,L\). It uses one variable per listed support type and never enumerates unlisted possible types.
The [cited discrete hardness result](https://www.ijcai.org/proceedings/2019/0037.pdf) concerns indivisible districts. Here the permitted masses form intervals \(x_t\in[0,\mu_t]\), and all budget and winning conditions admit the linear formulation proved above.
The argument applies to every instance specified in the question, including instances where \(a\) does not win the true profile. No additional promise is required.
⟨structured verdict parsed — rendered above⟩
The prover resolves the stated continuous problem. The LP formulation, treatment of strict inequalities, and polynomial bit-complexity argument are correct. No major or minor mathematical issues were found.
The definitions of \(r_c\) and \(d_{tc}\) correctly give
\[
S_a(x)-S_c(x)=r_c+\sum_{t\in T}d_{tc}x_t.
\]
This follows directly by subtracting the two given score formulas and collecting constant and variable terms.
The sets \(H\) and \(K\) partition all opponents according to the specified strict tie-breaking order. The required positive comparisons for \(H\) and nonnegative comparisons for \(K\) therefore match the task exactly.
The bounds on \(x_t\) and the budget constraint reproduce the permitted recounts without imposing integrality or restricting the variables to rational values.
The common margin \(\varepsilon\) is imposed only on the comparisons that must be strict. Its upper bound does not exclude any winning recount: the forward implication explicitly caps the chosen positive margin at \(1\).
The stated dimensions are correct. There are \(\tau+1\) variables and
\[
2\tau+1+2+(m-1)=2\tau+m+2
\]
inequalities.
All constraints are non-strict affine inequalities, so the feasible region is closed. The variable bounds place it inside the stated bounded box. Thus, whenever it is nonempty, it is compact, and the continuous objective attains a finite maximum.
This justifies the use of an attaining pair \((x^\star,\varepsilon^\star)\) in the reverse implication. No full-dimensionality assumption is needed.
In the forward direction, when \(H\) is nonempty, every member of the finite set used to define \(\varepsilon\) is positive. Its minimum is therefore positive, and every LP constraint follows as stated.
The separate treatment of \(H=\varnothing\) is necessary and correct: choosing \(\varepsilon=1\) is feasible whenever the recount satisfies all weak comparisons.
In the reverse direction, an attained optimum with \(\varepsilon^\star>0\) supplies all required strict and weak comparisons. Hence the equivalence is proved in both directions.
The proof also correctly rejects the weaker approach of merely checking feasibility after replacing strict comparisons by weak ones.
Each \(d_{tc}\) uses only four input rationals and consequently has polynomial encoding length.
For each fixed \(c\), the denominator product described for \(r_c\) is a valid common denominator. Its binary length is bounded by the sum of the lengths of the relevant input denominators, which is \(O(L)\). The bound \(|r_c|\le1\) is correct because the masses are positive and sum to \(1\), while every reported-share difference lies in \([-1,1]\). Thus the numerator also has \(O(L)\) bits.
These bounds justify computing the coefficients by exact rational arithmetic in polynomial time. The dense LP encoding bound
\[
B=O((m+\tau)(\tau+1)L)
\]
safely accounts for the constraint matrix, right-hand sides, and objective.
The prover states the relevant standard theorem sufficiently precisely for this application: binary-encoded rational LPs admit deterministic polynomial-time solution, including infeasibility detection and exact rational optimization when an attained finite optimum exists. The cited [Khachiyan reference](https://www.mathnet.ru/php/archive.phtml?jrnid=zvmmf&option_lang=eng&paperid=5239&wshow=paper) is correctly identified.
Every required hypothesis is verified in the write-up: rational coefficients, linear constraints and objective, polynomial encoding length, and an attained finite optimum whenever feasible. Exact comparison of the returned rational optimum with zero therefore decides the problem without numerical tolerance.
The stated running time is polynomial in \(m,\tau,L\). It depends on the listed support size and does not enumerate possible unlisted types.
The argument covers both endpoint budgets, a single support type, zero vote shares, infeasible LPs, and feasible LPs with optimal margin zero. It also explicitly handles a target ranked first in the tie-breaking order.
Neither the reported winner assumption nor a promise about the true winner is needed by the algorithm; proving the result for this broader collection of profiles is valid.
The distinction from indivisible-district recounting is accurate and consistent with the [cited discrete paper](https://www.ijcai.org/proceedings/2019/0037.pdf). That contextual comparison is not used to establish the continuous result.
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.