Answer: Polynomial-time solvable in m, τ, and L. Every promised instance has finite dimension, and attaining rational rules can be output in polynomial time.
Theorem 1 — class: other
PDF text-layer excerpt — equations and symbol order may be approximateLet Γ(N, LM) be a simple game and let C ⊂2N be a collection of coalitions such that ∀x ∈LM∃c ∈C : d(x, c) ≤1. The dimension of Γ(N, LM) is bounded from above by |C|.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given rational masses \(\mu_t\) for \(\tau\) membership types and an explicitly encoded monotone, closed rational polyhedral winning region \(W\subseteq\prod_t[0,\mu_t]\), find the least \(d\) for which rational vectors \(w^1,\ldots,w^d\ge 0\) and positive rational quotas \(q_1,\ldots,q_d\) satisfy \(x\in W\) exactly when \(w^j\cdot x\ge q_j\) for every \(j\); output the rules or report that no finite representation exists.
A society is given by its support: a list of \(\tau\ge 1\) membership types with positive masses \(\mu_t\in\mathbb{Q}_{>0}\), encoded in binary. Here \(\tau\) is the support size, not the number of possible types; total mass need not equal one.
A coalition is any real vector \(x\in B:=\prod_{t=1}^{\tau}[0,\mu_t]\). Its winning region is supplied as \(W=\{x\in B:Ax\ge b\}\), with \(m\) explicitly listed rational inequalities. Promise that \(0\notin W\), \(\mu\in W\), and \(x\in W,\ x\le y\in B\) imply \(y\in W\); lower-dimensional regions are allowed.
Define the dimension as the least positive integer \(d\) admitting \(w^j\in\mathbb{Q}_{\ge0}^{\tau}\) and \(q_j\in\mathbb{Q}_{>0}\) such that, for every \(x\in B\), \(x\in W\iff w^j\cdot x\ge q_j\) for all \(j\in\{1,\ldots,d\}\). Equality meets the quota. Set the dimension to \(\infty\) if no finite representation exists.
The computational problem is to find this minimum and output attaining rules, or report that no finite representation exists. Let \(L\) be the total binary input length; state running times in \(m,\tau,L\).
Is this minimum-dimension problem solvable in polynomial time in \(m,\tau,L\), or is it \(\mathrm{NP}\)-hard?
For finite simple games, dimension is at most \(|C|\) whenever every maximal losing coalition is within Hamming distance one of some member of \(C\). [Olsen](https://arxiv.org/abs/1609.04960)
Given \(k\) weighted majority games, deciding whether their intersection has dimension exactly \(k\) is \(\mathrm{NP}\)-hard. [Deineko–Woeginger](https://research.tue.nl/en/publications/on-the-dimension-of-simple-monotonic-games/)
No result settling the exact continuous problem specified above was located.
Result. The minimum-dimension problem is polynomial-time solvable in $m,\tau,L$. Every instance satisfying the promises has finite dimension, and attaining rational rules can be produced in polynomial time.
The lower-dimensional case contributes one extra rule, regardless of how many coordinates are forced to their maximum values. The proof below establishes both the construction and its optimality.
1. Removing forced coordinates.
Define
$$
F=\{t:x_t=\mu_t\text{ for every }x\in W\},
\qquad
U=\{1,\ldots,\tau\}\setminus F.
$$
For each coordinate, solve the rational linear program
$$
\ell_t=\min\{x_t:x\in B,\ Ax\ge b\}.
$$
These programs are feasible because $\mu\in W$, and their feasible regions are compact. Since $x_t\le\mu_t$ throughout $B$,
$$
t\in F\iff \ell_t=\mu_t.
$$
Thus $F$ is computable using $\tau$ exact linear programs.
Let
$$
B_U=\prod_{t\in U}[0,\mu_t],
\qquad
P=\{u\in B_U:(\mu_F,u)\in W\}.
$$
Here $(\mu_F,u)$ denotes the vector with coordinates $\mu_t$ on $F$ and $u_t$ on $U$. By the definition of $F$,
$$
W=\{(\mu_F,u):u\in P\}.
$$
Substituting the forced coordinates into each input row gives
$$
a_i=(A_{it})_{t\in U},
\qquad
\beta_i=b_i-\sum_{t\in F}A_{it}\mu_t,
$$
and hence
$$
P=\{u\in B_U:a_i\cdot u\ge\beta_i\text{ for }i=1,\ldots,m\}.
$$
If $U$ is nonempty, then $P$ has nonempty interior in $\mathbb R^U$. To prove this, for each $t\in U$ choose $x^{(t)}\in W$ with $x^{(t)}_t<\mu_t$. Such a point exists because $t\notin F$. The average
$$
z=\frac1{|U|}\sum_{t\in U}x^{(t)}
$$
belongs to $W$ by convexity. For every $t\in U$, all summands have their $t$th coordinate at most $\mu_t$, and one has it strictly smaller. Therefore $z_t<\mu_t$.
Upward closure implies
$$
\prod_{t\in U}[z_t,\mu_t]\subseteq P.
$$
The point
$$
u^\circ=\frac{z_U+\mu_U}{2}
$$
lies strictly between the endpoints of every interval in this product and satisfies $0<u^\circ_t<\mu_t$. Consequently, an open ball around $u^\circ$ lies in $P\cap\operatorname{int}(B_U)$.
If $U$ is empty, then $W=\{\mu\}$; we handle this case using the empty reduced system below.
2. Removing redundant inequalities relative to the box.
Start with $J=\{1,\ldots,m\}$ and process its rows in any fixed order. For a current row $i\in J$, solve
$$
v_i=\min\left\{
a_i\cdot u:
u\in B_U,\
a_j\cdot u\ge\beta_j\text{ for }j\in J\setminus\{i\}
\right\}.
$$
Delete $i$ precisely when $v_i\ge\beta_i$.
Each feasible region contains $P$ and is compact, so every such minimum exists. A deletion preserves the represented set. Moreover, a row found nonredundant remains nonredundant after subsequent deletions: its violating witness continues to satisfy the remaining rows.
Thus, after at most $m$ linear programs, the final set $J$ satisfies
$$
P=\{u\in B_U:a_i\cdot u\ge\beta_i\text{ for }i\in J\},
$$
and every retained row is nonredundant relative to $B_U$. Write
$$
r=|J|.
$$
When $U$ is empty, every reduced row is a true constant inequality because $\mu\in W$, so all rows are deleted and $r=0$.
We next prove the crucial properties of the retained rows.
3. Every retained row is an admissible weighted rule.
Suppose $U$ is nonempty. For every $i\in J$, we claim that
$$
a_i\ne0,\qquad a_i\in\mathbb Q_{\ge0}^U,\qquad \beta_i>0.
$$
A retained row cannot have $a_i=0$: because $P$ is nonempty, its constant inequality would hold everywhere and would be redundant.
The interior point $u^\circ$ from Section 1 satisfies every retained row strictly. Indeed, if a nonzero valid linear inequality were tight at an interior point of $P$, a sufficiently small displacement against its normal would remain in $P$ and violate it.
Fix $i\in J$. Nonredundancy provides a point $v\in B_U$ satisfying
$$
a_i\cdot v<\beta_i,
\qquad
a_j\cdot v\ge\beta_j\quad(j\in J\setminus\{i\}).
$$
For sufficiently small $\varepsilon>0$, the point
$$
y=(1-\varepsilon)v+\varepsilon u^\circ
$$
still violates row $i$, lies in $\operatorname{int}(B_U)$, and satisfies all other retained rows strictly. The segment from $y$ to $u^\circ$ therefore contains a point $p_i$ such that
$$
a_i\cdot p_i=\beta_i,
\qquad
a_j\cdot p_i>\beta_j\quad(j\ne i),
\qquad
p_i\in\operatorname{int}(B_U).
$$
In particular, $p_i\in P$.
For any $t\in U$, a sufficiently small positive displacement $p_i+\delta e_t$ remains in $B_U$. Upward closure gives $p_i+\delta e_t\in P$, so
$$
\beta_i+\delta a_{it}
=a_i\cdot(p_i+\delta e_t)
\ge\beta_i.
$$
Hence $a_{it}\ge0$.
Finally, if $\beta_i\le0$, then nonnegativity of $a_i$ would imply
$$
a_i\cdot u\ge0\ge\beta_i
\qquad\text{for every }u\in B_U.
$$
The row would be redundant. Therefore $\beta_i>0$, proving the claim.
We will also use the local geometry at $p_i$: because all other rows and all box bounds are strict there, some neighborhood $N_i$ of $p_i$ satisfies
$$
P\cap N_i
=
\{u\in N_i:a_i\cdot u\ge\beta_i\}.
$$
4. Constructing an attaining representation.
For each $i\in J$, output the rule
$$
w^i_t=
\begin{cases}
a_{it},&t\in U,\\
0,&t\in F,
\end{cases}
\qquad
q_i=\beta_i.
$$
These weights are rational and nonnegative, and their quotas are positive.
If $F$ is nonempty, also output
$$
\sum_{t\in F}x_t\ge\sum_{t\in F}\mu_t.
$$
Its quota is positive. Within $B$, every summand satisfies $x_t\le\mu_t$, so this rule holds exactly when
$$
x_t=\mu_t\quad\text{for every }t\in F.
$$
Together with the retained reduced rows, it therefore represents $W$ exactly.
Consequently,
$$
\dim(W)\le r+\mathbf1_{\{F\ne\varnothing\}}.
$$
The right-hand side is positive: if $F$ were empty and $r=0$, we would have $W=B$, contrary to $0\notin W$.
5. Lower bound for arbitrary representations.
Consider any representation of $W$ by $d$ admissible rules,
$$
w^k\cdot x\ge q_k,\qquad k=1,\ldots,d.
$$
On the face $x_F=\mu_F$, these become
$$
c_k\cdot u\ge s_k,
\qquad
c_k=w^k_U,
\qquad
s_k=q_k-w^k_F\cdot\mu_F.
$$
Their intersection inside $B_U$ is exactly $P$.
First suppose $U$ is nonempty. Fix a retained row $i$ and its point $p_i$ from Section 3. At least one restricted rule with $c_k\ne0$ must be tight at $p_i$. Otherwise, all nonconstant restricted rules would be strict in a neighborhood of $p_i$. The constant restricted rules hold everywhere because they hold on the nonempty set $P$. Thus the represented set would contain a neighborhood of $p_i$, contradicting the local halfspace description in Section 3.
Choose such a tight rule. For any vector $v$ satisfying $a_i\cdot v=0$, both $p_i+\delta v$ and $p_i-\delta v$ lie in $P$ for sufficiently small $\delta>0$. Validity and tightness of the chosen rule give
$$
c_k\cdot v=0.
$$
Therefore $c_k$ is proportional to $a_i$. Both vectors are nonzero and nonnegative, so the proportionality factor is positive. Tightness at $p_i$ then yields
$$
(c_k,s_k)=\lambda(a_i,\beta_i)
\quad\text{for some }\lambda>0.
$$
Different retained rows require different rules. Indeed, if the same rule served two rows, their equality hyperplanes would coincide. This is impossible because $p_i$ is tight for row $i$ and strict for every other retained row.
It follows that every representation has at least $r$ rules whose restrictions have nonzero normals:
$$
d\ge r.
$$
Now suppose $F$ is nonempty, allowing $U$ to be empty. Choose an interior point $u^\circ$ of $P$ when $U$ is nonempty, or its unique point when $U$ is empty, and set
$$
x^\circ=(\mu_F,u^\circ).
$$
Every rule with $c_k\ne0$ is strict at $u^\circ$. This follows from the same interior-point argument used in Section 3.
There must be a tight rule at $x^\circ$ with $c_k=0$. If no such rule existed, every rule would be strict at $x^\circ$. Since there are finitely many rules, decreasing any one coordinate in $F$ by a sufficiently small positive amount would preserve them all and remain inside $B$. The resulting point would be declared winning, contradicting the definition of $F$.
This tight rule with zero restricted normal is additional to the $r$ distinct rules required above. Hence
$$
d\ge r+1\qquad\text{when }F\ne\varnothing.
$$
Combining construction and lower bound proves the exact formula
$$
\boxed{\dim(W)=r+\mathbf1_{\{F\ne\varnothing\}}.}
$$
In particular, $W=\{\mu\}$ has dimension one, enforced by the single rule
$$
\sum_{t=1}^{\tau}x_t\ge\sum_{t=1}^{\tau}\mu_t.
$$
6. Running time and output size.
The algorithm uses at most $\tau+m$ exact rational linear programs. Each has at most $\tau$ variables and $m+2\tau$ constraints.
We use the standard rational linear-programming theorem: feasibility and finite optimal values can be computed exactly in time polynomial in the binary encoding length. This theorem permits lower-dimensional feasible regions; rational LP polynomial-time solvability is discussed, for example, by [Adler and Beling](https://adler.ieor.berkeley.edu/ilans_pubs/lp_algebraic_stoc_1992.pdf). Here every program is feasible and bounded, as verified above.
Substitution, exact comparisons, and output construction require polynomial-time rational arithmetic. A conservative bound on the encoding length of each constructed LP is
$$
S=O((m+\tau+1)^2L).
$$
If $T_{\mathrm{LP}}(n,h,S)$ denotes the polynomial bit-time bound of an exact rational LP solver, the total running time is
$$
O\!\left(
(m+\tau)\,
T_{\mathrm{LP}}\!\left(\tau,m+2\tau,O((m+\tau+1)^2L)\right)
\right)
+\operatorname{poly}(m,\tau,L).
$$
Thus the total time is polynomial in $m,\tau,L$. At most $m+1$ rules are output, with polynomial total binary length.
The cited [Deineko–Woeginger hardness result](https://research.tue.nl/en/publications/on-the-dimension-of-simple-monotonic-games/) concerns finite simple games. The proof here uses equality of the winning regions throughout the real box: the local boundary near each $p_i$ forces a distinct rule. This establishes polynomial-time solvability for the specified continuous problem.
⟨structured verdict parsed — rendered above⟩
The prover resolves the specified continuous problem correctly. The construction produces admissible rational rules, the lower bound proves their optimality, and the algorithm runs in polynomial time in $m,\tau,L$.
I found no major or minor gaps. In particular, the treatment of lower-dimensional winning regions is valid: all forced coordinates can be enforced by one additional rule, and the proof establishes that this additional rule is necessary.
Each coordinate-minimization program is feasible because $\mu\in W$. Its feasible region is closed and contained in the compact box $B$, so its minimum is attained.
Since every feasible point satisfies $x_t\le\mu_t$, the equivalence
$$
t\in F\iff \ell_t=\mu_t
$$
is correct. It identifies exactly the coordinates fixed at their upper bounds throughout $W$.
The identity
$$
W=\{(\mu_F,u):u\in P\}
$$
then follows directly from the definitions. Substituting the forced coordinates gives the stated rational coefficients $a_i$ and $\beta_i$ without changing the represented set.
The full-dimensionality argument for $P$ is sound. For each $t\in U$, the chosen point $x^{(t)}$ exists by the definition of $U$. Convexity of $W$ follows from its description as an intersection of a box and linear halfspaces, so the average $z$ belongs to $W$. Its coordinates satisfy
$$
z_t<\mu_t\qquad(t\in U).
$$
Upward closure consequently supplies the entire stated product of intervals inside $P$. Because $\mu_t>0$ and $z_t\ge0$, the midpoint $u^\circ$ lies strictly inside both this product and $B_U$. Thus $P$ has nonempty ambient interior whenever $U\ne\varnothing$.
When $U=\varnothing$, the promises and the definition of $F$ indeed give $W=\{\mu\}$.
The redundancy test is exact: row $i$ follows from the remaining rows and the box precisely when
$$
v_i\ge\beta_i.
$$
Every tested feasible region contains $P$, so it is nonempty; compactness ensures that the minimum exists.
Deleting a redundant row preserves $P$. A witness to nonredundancy continues to satisfy all surviving rows after later deletions, so a row retained earlier cannot become redundant through this procedure. Therefore one pass yields an irredundant description relative to $B_U$.
For $U=\varnothing$, every row is a constant inequality satisfied at $\mu$. All rows are therefore deleted, as claimed.
The proof correctly establishes all three required properties:
$$
a_i\ne0,\qquad a_i\ge0,\qquad \beta_i>0.
$$
A zero-normal row valid on nonempty $P$ would hold throughout the reduced box and hence be redundant.
Every nonzero retained inequality is strict at the interior point $u^\circ$: equality there would allow a small displacement against its normal inside $P$, contradicting validity.
Nonredundancy provides a violating point $v$ satisfying every other retained row. Mixing it with $u^\circ$ by a sufficiently small positive coefficient simultaneously preserves the strict violation, moves into the interior of the box, and makes every other row strict. The segment to $u^\circ$ therefore crosses row $i$ at the claimed point $p_i$, with all other inequalities and box bounds strict.
For each coordinate $t\in U$, a small upward displacement from $p_i$ remains in the box and is winning by upward closure. Since row $i$ is tight at $p_i$, this implies $a_{it}\ge0$.
Finally, $\beta_i\le0$ would make the row automatically true throughout $B_U$, contradicting nonredundancy. Thus the retained rows have positive quotas.
The local halfspace description at $p_i$ also follows: finitely many strict inequalities and strict box bounds remain strict in a sufficiently small neighborhood.
Extending each retained normal by zero weights on $F$ produces rational, nonnegative weights with positive quotas.
When $F\ne\varnothing$, the additional rule
$$
\sum_{t\in F}x_t\ge\sum_{t\in F}\mu_t
$$
has positive quota. Within $B$, it is satisfied exactly when every coordinate in $F$ equals its upper bound. This follows because the nonnegative deficits $\mu_t-x_t$ must have sum zero.
Consequently, the constructed rules represent $W$ exactly and establish
$$
\dim(W)\le r+\mathbf1_{\{F\ne\varnothing\}}.
$$
The prover also correctly checks the positive-dimension requirement: $F=\varnothing$ and $r=0$ would imply $W=B$, contradicting $0\notin W$.
Thus every promised instance has a finite admissible representation.
Restricting any admissible representation to the face $x_F=\mu_F$ gives exactly the stated representation of $P$. The restricted quotas $s_k$ need not be positive, and the argument correctly does not assume that they are.
At each $p_i$, some restricted rule with nonzero normal must be tight. Otherwise, all nonconstant rules would hold strictly in a neighborhood, while constant rules would hold everywhere because $P$ is nonempty. This would contradict the established local boundary of $P$.
For a tight nonconstant rule, both sufficiently small displacements tangent to row $i$ remain in $P$. Validity in both directions forces
$$
c_k\cdot v=0
\qquad\text{whenever }a_i\cdot v=0.
$$
The resulting proportionality of the nonzero normals is valid. Their nonnegativity makes the proportionality factor positive, and tightness identifies the corresponding quota:
$$
(c_k,s_k)=\lambda(a_i,\beta_i),\qquad \lambda>0.
$$
A single restricted rule cannot serve two retained rows. Positive proportionality would make their equality hyperplanes coincide, contradicting the fact that $p_i$ is tight only for its own retained row. Therefore at least $r$ distinct rules have nonzero restricted normals.
When $F\ne\varnothing$, every rule with nonzero restricted normal is strict at the interior reduced point $u^\circ$. If there were no tight rule with zero restricted normal, all original rules would be strict at $x^\circ$. Finiteness of the representation would then permit a sufficiently small decrease in a forced coordinate while preserving all rules. Positive masses ensure that this decrease stays in $B$. The resulting winning point would contradict the definition of $F$.
Hence a further rule is necessary:
$$
d\ge r+1\qquad(F\ne\varnothing).
$$
This argument also covers $U=\varnothing$, when every restricted normal is zero.
The construction and lower bound therefore establish exactly
$$
\dim(W)=r+\mathbf1_{\{F\ne\varnothing\}}.
$$
The algorithm performs at most $\tau+m$ rational linear programs, each with at most $\tau$ variables and $m+2\tau$ constraints. All are feasible and bounded, including those with lower-dimensional feasible regions.
The invoked standard theorem—exact polynomial-time solvability of rational linear programming in the binary encoding model—is applicable. The cited paper explicitly discusses polynomial-time solvability for rational input and polynomial bounds on intermediate encoding lengths. [Adler–Beling](https://adler.ieor.berkeley.edu/ilans_pubs/lp_algebraic_stoc_1992.pdf)
Substitution uses rational products and finite sums, so the resulting encoding lengths remain polynomial. The displayed bound
$$
S=O((m+\tau+1)^2L)
$$
is conservative and sufficient. Exact comparisons and construction of at most $m+1$ rules likewise require polynomial time and produce polynomial total output length.
The stated running-time expression therefore establishes the required polynomial dependence on $m,\tau,L$.
No corrections or additional clarification are required. The proof establishes both the minimum value and attaining rational rules for every promised instance.
⟨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.