Answer: —
Theorem 10 — class: algorithmic
Given \(\tau\) ordered run-types on \([0,1]\), each with rational party label \(p_j\in\{R,B\}\), support interval \(I_j\), and mass \(\mu_j\) with \(\sum_j\mu_j=1\), together with \(k,\varepsilon,\beta\), decide whether there is a consecutive partition \(\Pi\) into intervals of mass in \([(1-\varepsilon)/k,(1+\varepsilon)/k]\) such that no allowable interval \(D\) has unhappy mass \(u_p(D,\Pi)>\max\{|D|/2,\beta/k\}\) for either party \(p\), and construct \(\Pi\) when one exists.
A society is given by its support: a list of \(\tau\) types with positive binary rational masses; \(\tau\) is the support size, not the number of possible types. Here \(m=2\) parties, \(R\) and \(B\).
Type \(j\) has label \(p_j\in\{R,B\}\), mass \(\mu_j>0\), and interval \(I_j=[a_{j-1},a_j]\), where \(0=a_0<\cdots<a_\tau=1\) are rational, consecutive labels differ, and \(\sum_j\mu_j=1\). Its mass is uniformly distributed on \(I_j\); endpoints have zero mass.
For measurable \(A\), define \(M_p(A)=\sum_{j:p_j=p}\mu_j\lambda(A\cap I_j)/(a_j-a_{j-1})\), where \(\lambda\) is Lebesgue measure, and \(M(A)=M_R(A)+M_B(A)\).
Inputs also include a positive integer \(k\), encoded in unary, and binary rational parameters \(\varepsilon\in[0,1/2]\), \(\beta\in[1/2,1]\). Let \(L\) be the total input bit length; state running times in \(m,\tau,L,k\).
An interval \(D\subseteq[0,1]\) is allowable when \((1-\varepsilon)/k\le M(D)\le(1+\varepsilon)/k\). A balanced partition \(\Pi\) covers \([0,1]\) by consecutive allowable intervals with arbitrary real cut positions; its number of parts is unrestricted.
Each part elects its majority party by mass, with ties electing \(B\). Mass of party \(p\) in parts electing the other party is unhappy; let \(u_p(D,\Pi)\) be that unhappy mass within \(D\).
The partition is locally fair if \(u_p(D,\Pi)\le\max\{M(D)/2,\beta/k\}\) for every allowable interval \(D\) and both parties. Such \(D\) need not extend to a balanced partition.
Is deciding whether a locally fair balanced partition exists in \(\mathrm{P}\), or is it \(\mathrm{NP}\)-hard? In the polynomial-time case, can such a partition also be constructed in polynomial time?
For an explicit sequence of \(n\) voters and ideal population \(\sigma\in\{1,\ldots,n\}\), the discrete problem admits decision and construction in \(O(n\sigma^3)\) for \(\varepsilon\in[0,1/3)\), and \(O(n\sigma^4)\) for \(\varepsilon\in[1/3,1/2]\). [Verified discrete result](https://arxiv.org/pdf/2112.06899).
No result settling this exact continuous problem was located in the literature search.
The unrestricted question remains unresolved here: I do not establish either polynomial-time solvability or $\mathrm{NP}$-hardness.
The additional result proved below is that decision and construction are fixed-parameter tractable in the support size $\tau$. Specifically, for the stated model with $m=2$, both admit an exact algorithm with running time
$$
2^{O(\tau\log(\tau+1))}\operatorname{poly}(m,L,k).
$$
Thus, for every fixed support size, the problem is polynomial-time solvable even when unary $k$ is unrestricted.
The key reduction uses at most $\tau-1$ districts containing multiple types. All remaining districts can be represented by one integer count per type, without retaining their individual cut positions.
I also give a self-contained proof of polynomial-size rational witnesses and membership in $\mathrm{NP}$.
Let
$$
z_0=0,\qquad z_j=\sum_{r=1}^{j}\mu_r,
$$
and define the cumulative population map
$$
F(y)=M([0,y]).
$$
On the original type interval $[a_{j-1},a_j]$,
$$
F(y)=z_{j-1}
+\frac{\mu_j}{a_j-a_{j-1}}(y-a_{j-1}).
$$
Every slope is positive. Hence $F$ is a continuous, strictly increasing bijection from $[0,1]$ to itself.
An affine change of variables on each type interval shows that, in the coordinate $t=F(y)$:
Consequently, interval population, party population, district winners, unhappy mass, and local fairness are preserved.
Write
$$
A=\frac{1-\varepsilon}{k},\qquad
C=\frac{1+\varepsilon}{k},\qquad
b=\frac{\beta}{k}.
$$
An allowable interval now has length in $[A,C]$. In particular,
$$
A\ge\frac{1}{2k}>0.
$$
If a balanced partition has $q$ districts, then
$$
qA\le1\le qC,
$$
so
$$
q\le\left\lfloor\frac1A\right\rfloor\le2k.
$$
Once rational population-coordinate cuts have been obtained, their original coordinates are rational:
$$
F^{-1}(t)
=a_{j-1}
+\frac{a_j-a_{j-1}}{\mu_j}(t-z_{j-1}),
\qquad
t\in[z_{j-1},z_j].
$$
This conversion uses polynomial-time rational arithmetic.
Call a district mixed if it contains positive population from more than one type. Call it pure otherwise.
Because consecutive type labels differ and every type has positive mass, a district is mixed exactly when its interior contains at least one internal type boundary $z_j$. A pure district elects its sole party and creates no unhappy mass.
The interiors of distinct districts are disjoint. Choose an internal type boundary lying in the interior of each mixed district. Different mixed districts must receive different boundaries. There are only $\tau-1$ internal boundaries.
Therefore, if the mixed districts are
$$
[v_1,w_1],\ldots,[v_s,w_s],
$$
listed in increasing order, then
$$
s\le\tau-1,
\qquad
0\le v_1<w_1\le v_2<w_2\le\cdots\le v_s<w_s\le1.
$$
Also $s\le2k$, by the bound on the total number of districts. $\square$
Remove the mixed districts from a type interval
$$
T_j=[z_{j-1},z_j].
$$
Ignoring endpoints of zero population, the remaining set is a single interval, possibly empty.
Proof. Suppose instead that two positive residual portions within $T_j$ were separated by a removed portion. Choose residual points $u<v$ on opposite sides of that portion. Some mixed district meets $(u,v)$.
Since neither $u$ nor $v$ belongs to that district’s interior, the district must lie between them. It is therefore contained in $T_j$, and cannot be mixed. This is a contradiction. $\square$
Denote the residual interval in type $j$ by $J_j$, and its length by
$$
W_j
=\mu_j-\sum_{i=1}^{s}\lambda(T_j\cap[v_i,w_i]).
$$
Fix ordered, disjoint mixed intervals, each of length in $[A,C]$. They can be completed to a balanced partition by pure districts if and only if there exist integers
$$
n_j\in\{0,\ldots,2k\},\qquad j=1,\ldots,\tau,
$$
such that
$$
n_jA\le W_j\le n_jC.
$$
Proof.
For necessity, let $n_j$ be the number of pure districts remaining within type $j$. By Lemma 2, their lengths sum to $W_j$. Summing their individual balance inequalities gives
$$
n_jA\le W_j\le n_jC.
$$
The bound $n_j\le2k$ follows from the total district bound.
For sufficiency, if $n_j=0$, the inequalities force $W_j=0$. If $n_j>0$, divide $J_j$ into $n_j$ equal intervals. Their common length satisfies
$$
A\le\frac{W_j}{n_j}\le C.
$$
Together with the prescribed mixed districts, these intervals form a balanced partition. Each new interval is contained in one type, so it is pure. $\square$
The same proof establishes a useful invariance: the unhappy population depends only on the mixed intervals and their winners. Replacing the pure districts by any other balanced subdivision of the residual intervals leaves local fairness unchanged.
Fix mixed intervals, their actual winners, and a balanced pure completion. For party $p$, let
$$
H_p(t)=u_p([0,t],\Pi).
$$
Form the sorted union of the type boundaries and mixed endpoints:
$$
0=e_0<e_1<\cdots<e_r=1.
$$
Repeated coordinates are removed. The number of listed coordinates is at most
$$
\tau+1+2s\le3\tau-1.
$$
On every open interval between consecutive listed coordinates, either:
Thus $H_p$ is continuous and piecewise affine, with slope in $\{0,1\}$. In a pure residual interval its slope is zero. Individual pure-district cuts are unnecessary.
For any interval $[u,v]$,
$$
u_p([u,v],\Pi)=H_p(v)-H_p(u).
$$
Consider the pairs
$$
\mathcal V
=
\{(e_i,e_j):0\le i,j\le r\}
\cup
\{(e_i,e_i+c),(e_i-c,e_i):
0\le i\le r,\ c\in\{A,C,2b\}\}.
$$
Retain precisely those satisfying
$$
0\le u<v\le1,\qquad A\le v-u\le C.
$$
The partition is locally fair if and only if, for both parties and every retained pair,
$$
H_p(v)-H_p(u)
\le\max\left\{\frac{v-u}{2},b\right\}.
$$
Proof. Necessity follows because every retained pair defines an allowable interval.
For sufficiency, restrict the endpoint pair $(u,v)$ to a rectangle
$$
[e_i,e_{i+1}]\times[e_j,e_{j+1}].
$$
On this rectangle, $H_p(v)-H_p(u)$ is affine. Split its allowable portion into the two closed sets
$$
P^-_{ij}
=
\left\{
(u,v):
u\in[e_i,e_{i+1}],\
v\in[e_j,e_{j+1}],\
A\le v-u\le C,\
v-u\le2b
\right\}
$$
and
$$
P^+_{ij}
=
\left\{
(u,v):
u\in[e_i,e_{i+1}],\
v\in[e_j,e_{j+1}],\
A\le v-u\le C,\
v-u\ge2b
\right\}.
$$
On the first set, the fairness deficit is the affine function
$$
H_p(v)-H_p(u)-b.
$$
On the second, it is
$$
H_p(v)-H_p(u)-\frac{v-u}{2}.
$$
Each nonempty set is a compact polygon, segment, or point. An affine function attains its maximum at a vertex. Its boundary lines have the forms
$$
u=e_i,\qquad v=e_j,\qquad v-u=c,
\qquad c\in\{A,C,2b\}.
$$
The intersection of two nonparallel such lines is either a pair of breakpoints or a breakpoint paired with one of the listed shifts. Hence every vertex belongs to $\mathcal V$.
The assumed inequalities make each deficit nonpositive at every vertex, and therefore throughout both sets. These sets cover all allowable endpoint pairs. $\square$
This proof checks every allowable interval. It imposes no requirement that the interval extend to a balanced partition.
There are $O(\tau^2)$ candidates. Once the prefix functions have been computed, their values at all breakpoints and shifted breakpoints can be precomputed by merging a constant number of sorted lists. Each candidate then takes constant time per party.
For a supplied rational partition with total cut encoding length $S$, district winners and mixed intervals can first be identified by merging its cuts with the type boundaries. Consequently, verification takes
$$
O\!\left(m(\tau+k+\tau^2)\right)
$$
rational arithmetic operations, and polynomial bit time in $L+S$.
Fix
$$
s\in\{0,\ldots,\min(\tau-1,2k)\}.
$$
Use $2s$ real variables
$$
v_1,w_1,\ldots,v_s,w_s
$$
for the prospective mixed districts, and $\tau$ integer variables $n_j$ for their pure completions.
Let $E_1,\ldots,E_N$ be the symbolic list of the constant type boundaries and these endpoint variables. Consider all affine comparisons
$$
E_i-E_j-c,
\qquad
c\in\{0,\pm A,\pm C,\pm2b\}.
$$
There are $O(\tau^2)$ comparisons. Their zero sets form a rational hyperplane arrangement in dimension $2s$.
An arrangement cell records whether each comparison is negative, zero, or positive. Cells of every dimension are retained. Within one cell, the following information is fixed:
Each assertion is determined by signs of the listed comparisons.
Discard a cell unless every prospective mixed interval has at least one type boundary strictly in its interior. Impose the ordering and balance inequalities
$$
0\le v_1,\qquad
w_i\le v_{i+1},\qquad
w_s\le1,
$$
and
$$
A\le w_i-v_i\le C.
$$
For $s=0$, these conditions are absent.
Let $\ell_i$ and $r_i$ be the first and last types with positive intersection with mixed district $i$. They are fixed by the cell and satisfy $\ell_i<r_i$.
Its overlap with type $j$ is
$$
\lambda(T_j\cap[v_i,w_i])
=
\begin{cases}
0,&j<\ell_i\text{ or }j>r_i,\\
z_j-v_i,&j=\ell_i,\\
\mu_j,&\ell_i<j<r_i,\\
w_i-z_{j-1},&j=r_i.
\end{cases}
$$
Therefore every residual length $W_j$ is affine in the endpoint variables.
The completion constraints are the rational linear inequalities
$$
n_jA\le W_j\le n_jC,
\qquad
0\le n_j\le2k,
\qquad
n_j\in\mathbb Z.
$$
We may additionally impose
$$
s+\sum_{j=1}^{\tau}n_j\le2k.
$$
This holds for every balanced completion.
Let $P_R(t)$ be cumulative red population in population coordinates. It is continuous and affine on each type interval. The arrangement cell fixes the affine expression for $P_R$ at every endpoint variable.
For each prospective mixed district define
$$
G_i
=
2\bigl(P_R(w_i)-P_R(v_i)\bigr)-(w_i-v_i).
$$
Enumerate its winner as either $R$ or $B$. Impose
$$
G_i>0
\quad\text{for winner }R,
$$
and
$$
G_i\le0
\quad\text{for winner }B.
$$
These are exactly the prescribed majority conditions, including blue-winning ties.
The cell fixes the ordered breakpoints. The winner assignment fixes the unhappy-density slope $h_{p,\ell}\in\{0,1\}$ between each consecutive pair.
For $y\in[E_j,E_{j+1}]$,
$$
H_p(y)
=
\sum_{\ell<j}
h_{p,\ell}(E_{\ell+1}-E_\ell)
+h_{p,j}(y-E_j).
$$
A verification endpoint is a breakpoint or a breakpoint shifted by a fixed constant. Its containing segment is fixed by the cell. Thus its prefix value is affine in the endpoint variables.
The cell also fixes the applicable threshold branch. Every inequality from Lemma 4 is consequently linear.
We have obtained, for each cell and winner assignment, a mixed integer linear system with:
Its solutions are exactly the corresponding locally fair balanced completions, by Lemmas 3 and 4.
The strict inequalities must be handled exactly. Replacing them by weak inequalities without requiring positive slack would change the problem.
Write every strict inequality as
$$
f_h(x,n)>0,
$$
where $x$ denotes the real endpoints and $n$ the integer counts. Introduce a real variable $\delta$, replace these inequalities by
$$
f_h(x,n)\ge\delta,
$$
and add
$$
0\le\delta\le1.
$$
Also explicitly bound every endpoint between zero and one.
The augmented system can be cleared to integer coefficients using a common positive denominator. Let $U\ge1$ bound the absolute values of all resulting coefficients and right-hand sides, before fixing the counts.
Such a denominator and bound have bit length
$$
O\!\left(L+\log(\tau+k)\right).
$$
Indeed, the constants are sums of input masses and the parameters $A,C,b$, while the variable coefficients are bounded integer sums of the displayed affine expressions.
Fix any integer count vector with $0\le n_j\le2k$. After substitution, all coefficients and right-hand sides of the continuous system have absolute value at most
$$
T=U(1+2k\tau)+1.
$$
Let
$$
D=2s+1,\qquad
\eta=\frac{1}{D!\,T^D}.
$$
Claim. The original strict mixed integer system is feasible if and only if its augmented weak system is feasible with
$$
\delta\ge\eta.
$$
Proof. The reverse implication is immediate because $\eta>0$.
For the forward implication, fix the counts from a strict feasible solution. At that solution, the finitely many strict inequalities have a positive common slack. Thus the continuous augmented system admits a point with $\delta>0$.
Its feasible region is closed and bounded. Maximize $\delta$ and choose an optimal vertex. The optimum is positive.
At a vertex in $D$ variables, $D$ linearly independent active constraints determine the coordinates. Their integer coefficient matrix has entries bounded in absolute value by $T$. The determinant expansion gives
$$
|\det B|\le D!\,T^D.
$$
By Cramer’s rule, the positive coordinate $\delta$ has denominator at most $D!\,T^D$ after reduction. Its numerator is a positive integer. Therefore
$$
\delta\ge\frac{1}{D!\,T^D}=\eta.
$$
This proves the claim. $\square$
The bit length of $\eta$ is
$$
O\!\left(\tau\bigl(L+\log(\tau+k)\bigr)\right).
$$
Thus adding $\delta\ge\eta$ preserves polynomial encoding size.
Start with any feasible real partition. Choose its mixed intervals, counts, arrangement cell, and winners. Fix those counts and maximize $\delta$ in the augmented continuous system.
The preceding argument gives an optimal vertex with positive slack. Cramer’s rule, including the numerator determinant bound, gives endpoint encoding length
$$
O\!\left(\tau\bigl(L+\log(\tau+k)\bigr)\right)
$$
per endpoint.
Complete each residual type interval by equal subdivision into its fixed number of pure districts. Each additional cut is formed from rational endpoints and division by an integer at most $2k$. It has the same asymptotic encoding bound.
There are at most $2k$ districts. Hence a feasible instance has a rational partition whose total cut encoding length is
$$
O\!\left(
k\tau\bigl(L+\log(\tau+k)\bigr)
\right).
$$
The inverse population map preserves polynomial encoding length.
Since $k$ is unary and the input explicitly lists $\tau$ types, this is a polynomial-size certificate. Section 3 gives a polynomial-time exact verifier. Therefore the unrestricted decision problem belongs to $\mathrm{NP}$.
The algorithm uses two standard algorithmic theorems.
Rational linear programming. A rational linear system can be tested for feasibility in time polynomial in its binary encoding size. A rational linear objective can be optimized exactly in polynomial time. For a nonempty bounded feasible region, an optimal vertex can be obtained with polynomial encoding length, using further linear-programming calls if necessary.
Mixed integer linear feasibility. For a rational system of weak linear inequalities with $r$ designated integer variables, feasibility is decidable in
$$
(r+1)^{O(r)}\operatorname{poly}(S)
$$
time, where $S$ is its binary encoding size. The polynomial exponent is independent of $r$. This is the fixed-dimensional mixed integer programming theorem and its improved running-time bound; see [Lenstra, Section 5](https://people.csail.mit.edu/rrw/presentations/Lenstra81.pdf) and [Bredereck et al., Theorem 1](https://arxiv.org/pdf/1709.02850).
Our systems meet its hypotheses after Section 5 replaces every strict condition by the weak condition with $\delta\ge\eta$.
An arrangement of $H$ hyperplanes in dimension $d$ has at most
$$
\sum_{i=0}^{d}2^i\binom{H}{i}
$$
cells of all dimensions.
For completeness, adding a hyperplane splits some old cells. Each split replaces one cell by three and increases the count by two. The split cells give cells of the induced arrangement on the new hyperplane. Induction on $H$ and $d$ yields the displayed bound.
Cells intersecting the endpoint box can be enumerated incrementally. For every existing sign pattern, intersect it with the negative side, equality set, and positive side of the next hyperplane. Retain an intersection exactly when it meets the box.
These tests are rational linear feasibility tests with strict inequalities. They are performed by maximizing the common slack and accepting only when the optimum is strictly positive. The box and slack bounds make the programs bounded.
Here
$$
H=O(\tau^2),\qquad d=2s\le2(\tau-1).
$$
The number of cells, and the enumeration time apart from polynomial arithmetic costs, are therefore
$$
2^{O(\tau\log(\tau+1))}.
$$
For every
$$
s\in\{0,\ldots,\min(\tau-1,2k)\},
$$
perform the following steps:
Accept if any test succeeds.
Correctness. A genuine fair partition determines one enumerated value of $s$, one cell, one winner assignment, and one integer count vector. Section 5 shows that its corresponding weak system is feasible.
Conversely, a feasible tested system preserves its cell’s strict signs and all strict red-majority conditions because $\delta\ge\eta>0$. Lemma 3 constructs a balanced pure completion. The winner conditions give the actual mixed-district winners, and Lemma 4 proves local fairness of the completion.
A feasibility oracle suffices to recover the integer counts.
For each $n_j$, binary-search its bounded range $\{0,\ldots,2k\}$. At each step, query whether a feasible completion exists with an additional upper bound on $n_j$. Once the least feasible upper bound is found, fix $n_j$ to that value. This preserves feasibility and uses
$$
O(\tau\log(k+1))
$$
oracle calls.
With all counts fixed, maximize $\delta$ in the original continuous augmented system. Its optimum is positive because the recovered counts admit a solution with $\delta\ge\eta$. Extract an optimal vertex, subdivide each residual interval equally into its prescribed number of pure districts, and apply $F^{-1}$ to every cut.
This produces a rational locally fair balanced partition.
Each tested mixed integer system has:
The arrangement enumeration, winner enumeration, mixed integer calls, and construction therefore take
$$
\boxed{
2^{O(\tau\log(\tau+1))}
\operatorname{poly}(m,L,k),
\qquad m=2.
}
$$
This is fixed-parameter tractability in $\tau$, rather than merely a polynomial-time algorithm for fixed $k$.
When $\varepsilon=0$, every district has length $1/k$ in population coordinates. Hence there are exactly $k$ districts and their cuts are uniquely forced:
$$
x_i=\frac{i}{k},
\qquad i=0,\ldots,k.
$$
Verify this partition using Section 3. If it passes, convert its cuts to original coordinates; otherwise no fair balanced partition exists. Decision and construction take
$$
O\!\left(
m(\tau+k+\tau^2)\operatorname{poly}(L)
\right)
$$
bit time.
For unrestricted $\varepsilon$ and unrestricted support, the new algorithm still has an exponential dependence on $\tau$. Compression removes the individual pure-district cut variables, but leaves potentially $\tau-1$ mixed districts whose positions and winners must be coordinated.
Accordingly, the proved results do not settle the requested unrestricted classification. What remains is either an algorithm with polynomial dependence on $\tau,L,k$, including construction, or a valid hardness reduction.
⟨structured verdict parsed — rendered above⟩
Overall assessment: partial, with sound substantive progress. The output does not resolve the unrestricted decision problem posed in USER_TASK, and explicitly acknowledges this. Its support-parameter algorithm, rational-witness argument, membership in $\mathrm{NP}$, and polynomial-time case for $\varepsilon=0$ withstand the audit, subject to minor implementation clarifications.
I found no false central mathematical step.
This reduction is correct.
The assumptions $\mu_j>0$ and $a_j>a_{j-1}$ give strictly positive slopes for $F$. Its formulas agree at adjacent type boundaries, and its endpoint values are $0$ and $1$. Thus the claimed continuous, strictly increasing bijection exists.
The affine transformation on each type interval preserves total and party population measures. Consequently, it preserves majority outcomes, including ties, and all unhappy-mass inequalities.
The district-count bound is valid:
$$
qA\le 1,\qquad A\ge\frac{1}{2k}
\quad\Longrightarrow\quad
q\le 2k.
$$
The rational inverse formula is correct and has polynomial encoding cost.
All three lemmas are sound under the stated convention of ignoring endpoints of zero mass.
Lemma 1. A district contains positive mass from multiple types exactly when its interior contains an internal type boundary. Distinct district interiors cannot contain the same chosen boundary. Hence the bound of $\tau-1$ mixed districts follows.
Lemma 2. The contradiction argument is valid. A removed mixed district separating two residual points inside one type would have to lie between those points, and therefore inside that type. Such a district could not be mixed.
This reasoning applies to genuine mixed intervals, as required by Lemma 3. It would not apply to arbitrary removed intervals, but the output does not need that stronger assertion.
Lemma 3. The inequalities
$$
n_jA\le W_j\le n_jC
$$
are necessary by summing pure-district lengths. They are sufficient because each positive residual interval can be subdivided equally. The case $n_j=0$ is handled correctly: it forces $W_j=0$.
The unhappy-mass invariance is also correct. Pure districts always elect their sole party, so their subdivision cannot change either party’s unhappy population.
Lemma 4 is correct.
On each endpoint rectangle, the unhappy-mass difference is affine. Splitting at $v-u=2b$ makes the fairness threshold affine on each resulting region.
Every vertex of a nonempty region is determined by two nonparallel boundary lines drawn from:
$$
u=e_i,\qquad v=e_j,\qquad v-u=c,
\qquad c\in\{A,C,2b\}.
$$
Their intersections have exactly the forms included in $\mathcal V$. Parallel diagonal boundaries introduce no additional vertex form.
The argument also handles segments and points. Since $A>0$, retained candidates automatically have distinct, correctly ordered endpoints. Values such as $C>1$ cause no difficulty because the endpoint-domain restrictions remain in force.
The test covers every allowable interval, without imposing extendability to a balanced partition. This matches USER_TASK.
The claimed candidate count and rational-arithmetic verification cost are consistent with the construction.
Minor clarification needed: the certificate verifier should explicitly check coverage, increasing cuts, and district balance before invoking this fairness test. The bound of $2k$ districts applies to balanced partitions, not arbitrary supplied rational partitions. Early rejection of an excessive district count makes the stated verification bound applicable.
The encoding is substantively correct.
The listed comparisons determine:
For shifted candidates, the interval length is a fixed constant, so its threshold branch is determined directly from the input parameters.
The overlap formulas correctly handle positive intersections and endpoints coinciding with type boundaries. Consequently, each $W_j$ is affine.
The majority constraints correctly implement the asymmetric tie rule:
$$
G_i>0
$$
for an $R$ winner, and
$$
G_i\le 0
$$
for a $B$ winner.
Once the cell and winners are fixed, the unhappy-density slopes are fixed. Prefix evaluations and fairness constraints are therefore affine.
Minor clarification needed: not every listed comparison has a proper hyperplane as its zero set. For example, $E_i-E_i$ is identically zero; comparisons involving only constant boundaries may also be constant. The arrangement description should explicitly retain their fixed signs and enumerate only proper hyperplanes. This does not change the algorithm or its asymptotic bound.
Coincident breakpoints require removal or consistent relabeling before using the prefix formula. Section 3 already specifies removal, so this is an implementation convention rather than a substantive gap.
The positive-slack argument is valid.
For fixed integer counts, any strict feasible solution has a positive minimum slack over its finitely many strict constraints. The augmented continuous region is closed and bounded because the endpoints and $\delta$ are explicitly bounded.
A positive maximum of $\delta$ is attained at a vertex. Boundedness suffices here even when the feasible region is lower-dimensional.
After denominator clearing and count substitution, the stated bound $T$ covers the coefficients and right-hand sides. At a vertex, Cramer’s rule gives:
$$
|\det B|\le D!\,T^D.
$$
Since a positive rational $\delta$ has a positive integer numerator in reduced form, the lower bound
$$
\delta\ge\frac{1}{D!\,T^D}
$$
follows.
The denominator-size claim is compatible with the displayed constraints: their rational constants use sums of input masses and fixed rational shifts, and their variable coefficients are bounded integer sums. No multiplication of endpoint variables occurs.
The rational-witness size bounds also follow. Equal subdivisions introduce division only by bounded integer counts, and the inverse population map preserves polynomial encoding length. Unary encoding of $k$ makes the total certificate length polynomial.
Thus membership in $\mathrm{NP}$ is established, subject to making the routine certificate checks in Section 3 explicit.
The cited mixed integer programming theorem supports the claimed parameter dependence. Theorem 1 of [Bredereck et al.](https://arxiv.org/pdf/1709.02850) states a bound of $O(r^{2.5r+o(r)}|I|)$ parameterized by the number of integer variables. Its formulation permits rational continuous variables and denominator clearing. The prover’s weaker bound
$$
(r+1)^{O(r)}\operatorname{poly}(S)
$$
is therefore supported.
The systems satisfy the relevant hypotheses after strict inequalities are replaced by the positive-slack constraints. There are $\tau$ designated integer variables, and the remaining constraints are rational weak linear inequalities.
The arrangement-cell bound, including lower-dimensional cells, is valid. With
$$
H=O(\tau^2),\qquad d=O(\tau),
$$
it yields
$$
2^{O(\tau\log(\tau+1))}
$$
cells. Incremental enumeration using exact slack optimization preserves this bound up to polynomial factors.
The construction procedure is also correct. Feasibility under an additional upper bound on one count is monotone in that bound. Finding the least feasible integer upper bound allows that count to be fixed without losing feasibility. After all counts are fixed, the continuous optimization and pure subdivisions recover a valid partition.
Accordingly, the claimed decision and construction time
$$
2^{O(\tau\log(\tau+1))}\operatorname{poly}(m,L,k),
\qquad m=2,
$$
is supported.
For $\varepsilon=0$, the argument is correct. Every district has population length $1/k$, so exactly $k$ districts occur and all population-coordinate cuts are forced. Testing that unique partition settles decision and construction in the stated polynomial time.
However, neither this special case nor fixed-parameter tractability in $\tau$ settles the unrestricted classification. The input support size is unrestricted, so the exponential dependence on $\tau$ remains material. Membership in $\mathrm{NP}$ also does not establish either polynomial-time solvability or hardness.
This is the major outstanding issue relative to USER_TASK, not a contradiction in the prover’s acknowledged partial claim.
USER_TASK, supply either an algorithm polynomial in unrestricted $\tau,L,k$, with the requested construction result, or a valid hardness reduction.⟨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.