Answer: \(\mathrm{NP}\)-hard already for fixed \(m=4\) and \(\tau=1\).
Theorem 4.10 — class: algorithmic
PDF text-layer excerpt — equations and symbol order may be approximateLet M = (S, A, R, P) be a social choice MDP, let R be an anonymous reward function, let bΘ be the partition of the agents into types, let Θ be a refinement of bΘ, and let Ψ ⊆S × A be symmetric with respect to EΘ. Fur- thermore, assume that |A| = O(1) and |Θ| = O(1). Then an optimal deterministic Ψ-consistent policy for M (which will be symmetric with respect to EΘ) can be computed in polynomial time in the number of agents n.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given fixed finite \(A\) and \hat{Θ}, rational type masses \(ρ_θ\), rational kernels \(P_θ(≻'∣≻,a)\), rational discount factor γ, initial mass state \(μ_0\), rational piecewise-linear anonymous reward ̅\(R(μ,a)\), and an anonymous polyhedral local restriction Ψ(μ), where μ ranges over ∏_θΔ\(L(A)\) and \(F_a\) is the induced affine update, compute a finite rational polyhedral stationary policy π with π(μ)∈Ψ(μ) that is ε-optimal for Σ_{k≥0}γ^k̅\(R(μ_k,π(μ_k))\), with μ_{k+1}=F_{π(μ_k)}μ_k.
Let \(A\) be a nonempty alternative set, \(m=|A|\), and \(L(A)\) the strict rankings. A society is given by its support: the list of \(\tau\) transition types with positive binary rational masses \(\rho_\theta\), normalized by \(\sum_\theta\rho_\theta=1\); \(\tau\) counts supported types, not possible rankings. Fix \(m\) and \(\tau\) as constants.
The state space is \(X=\prod_\theta\Delta(L(A))\), with conditional ranking distributions \(\mu_\theta\). Input stochastic kernels have nonnegative rational entries, and the deterministic update is \((F_a\mu)_\theta(r')=\sum_{r\in L(A)}P_\theta(r'\mid r,a)\mu_\theta(r)\).
Write \(q_r(\mu)=\sum_\theta\rho_\theta\mu_\theta(r)\). Anonymity means that rewards and allowed actions depend only on \(q(\mu)\): \(\bar R(\mu,a)=g_a(q(\mu))\) and \(\Psi(\mu)=\{a:q(\mu)\in D_a\}\).
Each signed reward \(g_a\) is given explicitly by rational affine formulas on a finite rational polyhedral partition of the ranking simplex; discontinuities are permitted. Each \(D_a\) is an explicitly listed finite union of rational polyhedral cells, and \(\Psi(\mu)\ne\varnothing\) for every \(\mu\in X\). Cells may use strict or weak inequalities, with boundaries explicitly assigned.
Input also includes rational \(\mu_0\in X\), \(0\le\gamma<1\), and \(\varepsilon>0\). A finite rational polyhedral stationary policy explicitly partitions \(X\) into such cells and assigns one action to each, satisfying \(\pi(\mu)\in\Psi(\mu)\) everywhere.
Define \(V^*(\mu_0)\) as the supremum of \(\sum_{k\ge0}\gamma^k\bar R(\mu_k,a_k)\) over admissible action sequences with \(\mu_{k+1}=F_{a_k}\mu_k\). The synthesis problem asks for a policy with \(V^\pi(\mu_0)\ge V^*(\mu_0)-\varepsilon\). Let \(L\) be the total binary input length, including all listed cells, \(\gamma\), and \(\varepsilon\).
Is this policy synthesis problem solvable in polynomial time, or is it NP-hard, for fixed \(m\) and \(\tau\)? State running times in \(m\), \(\tau\), and \(L\), making any additional dependence on \(\varepsilon\) and \(\gamma\) explicit.
For finite societies, optimal deterministic policies under type-symmetric local restrictions and anonymous rewards are computable in polynomial time in the agent count when the alternative count and the refining type partition size are constant ([Parkes–Procaccia](https://procaccia.info/wp-content/uploads/2020/03/dynamic.pdf)).
Related continuous-state work gives exact symbolic dynamic programming for finite-horizon models with finitely many actions ([Sanner–Delgado–de Barros](https://ssanner.github.io/papers/anu/cont_mdp.pdf)); no result settling this exact infinite-horizon synthesis problem was located.
1. Result
The problem is \(\mathrm{NP}\)-hard already for the fixed constants \(m=4\) and \(\tau=1\). Thus fixing the alternative count and the number of supported types does not give a polynomial-time synthesis algorithm unless \(\mathrm{P}=\mathrm{NP}\).
The hardness holds with rewards in \(\{0,1\}\), fixed tolerance \(\varepsilon=1/4\), and \((1-\gamma)^{-1}\) polynomially bounded in the input length. It also holds with both \(\gamma=1/2\) and \(\varepsilon=1/4\) fixed if binary-encoded reward magnitudes are unrestricted.
There is nevertheless an effective synthesis algorithm. Write \(d=\tau(m!-1)\), and let \(M\) be a computable bound on all absolute rewards. For \(M>0\), choose an integer \(H\ge1\) satisfying
\(\displaystyle \frac{2M\gamma^H}{1-\gamma}\le\varepsilon.\)
A conservative running-time bound is
\(\displaystyle (L+\tau m!)^{O(d+1)}\,m^{O(H)}\,\operatorname{poly}(H).\)
The algorithm outputs an admissible finite rational polyhedral stationary policy. Both assertions are proved below.
For \(m=1\), the sole action is admissible everywhere, so synthesis is trivial. The hardness statement concerns the general fixed-constant regime; it does not assert hardness for every smaller fixed alternative count.
2. A stochastic encoding of integer arithmetic
We first construct four fixed stochastic kernels. Set \(m=4\), so there are \(24\) rankings, and set \(\tau=1\) and \(\rho_1=1\). Consequently \(q=\mu_1\), and every function of the state is anonymous.
Choose five ranking coordinates, denoted \(s,t,v,u,z\). The first four will encode a scale, a clock, a current integer, and an accumulated sum. The coordinate \(z\) receives unused probability mass. All remaining coordinates start at zero.
Label the four actions \(a_0,a_1,a_+,a_{\mathrm{skip}}\). Define nonnegative linear maps on the first four coordinates by
\(\displaystyle B_0(s,t,v,u)=(s,t+s,2v,u),\)
\(\displaystyle B_1(s,t,v,u)=(s,t+s,2v+s,u),\)
\(\displaystyle B_+(s,t,v,u)=(s,t+s,0,u+v),\)
\(\displaystyle B_{\mathrm{skip}}(s,t,v,u)=(s,t+s,0,u).\)
Every column sum of every \(B_a\) is at most \(3\). To obtain a stochastic kernel \(P_a\), put \(B_a/3\) in the rows and columns corresponding to \(s,t,v,u\). For each of those four columns, send the remaining mass to \(z\). Send all mass from every other ranking column to \(z\).
All entries are nonnegative rationals, and every column sums to one. These are therefore valid kernels under the convention \(P_a(r'\mid r)\).
Their updates satisfy
\(\displaystyle (s',t',v',u')=\frac13 B_a(s,t,v,u).\)
Whenever \(s>0\), define the decoded quantities
\(\displaystyle c=\frac ts,\qquad x=\frac vs,\qquad y=\frac us.\)
Since \(s'=s/3>0\), the decoded updates are exactly:
| Action | Decoded update |
|---|---|
| \(a_0\) | \((c,x,y)\mapsto(c+1,2x,y)\) |
| \(a_1\) | \((c,x,y)\mapsto(c+1,2x+1,y)\) |
| \(a_+\) | \((c,x,y)\mapsto(c+1,0,y+x)\) |
| \(a_{\mathrm{skip}}\) | \((c,x,y)\mapsto(c+1,0,y)\) |
Thus stochastic linear dynamics can perform the required arithmetic on ratios of coordinates. Every test used below is still a rational linear test on the original coordinates: for example, \(c=k\) means \(t=ks\).
3. Reduction from binary SUBSET SUM
Use the standard \(\mathrm{NP}\)-hard SUBSET SUM problem: given positive binary integers \(w_1,\ldots,w_n,T\), determine whether some subset sums to \(T\). The hardness of SUBSET SUM is a standard established result; see, for example, [Polak–Rohwedder–Węgrzycki](https://arxiv.org/abs/2105.04035).
Let \(\ell_i\) be the binary length of \(w_i\), and define
\(\displaystyle N=\sum_{i=1}^n(\ell_i+1).\)
Construct a schedule of \(N\) instructions. For each \(w_i\), in order:
Let
\(\displaystyle G_k=\{q:s>0,\ t=ks\},\qquad 0\le k<N.\)
On \(G_k\), allow exactly the action or actions specified by instruction \(k\). Outside their union, allow only \(a_0\).
These restrictions have the required explicit polyhedral representation. Indeed, within the ranking simplex, the complement of the scheduled slices is the disjoint union of
\(\displaystyle \{s=0\},\)
\(\displaystyle \{s>0,\ t>(N-1)s\},\)
and
\(\displaystyle \{s>0,\ ks<t<(k+1)s\},\qquad 0\le k<N-1.\)
Here \(t\ge0\) follows from being a simplex coordinate. Thus every state has at least one admissible action, and all strict inequalities and boundaries are explicitly assigned.
Take the initial distribution concentrated on coordinate \(s\):
\(\displaystyle s=1,\qquad t=v=u=z=0.\)
The decoded initial state is \((c,x,y)=(0,0,0)\). Inductively, at time \(k\),
\(\displaystyle s_k=3^{-k}>0,\qquad c_k=k.\)
Hence the trajectory follows the schedule exactly.
Reading the digits of \(w_i\) from an initial \(x=0\) produces \(x=w_i\), because each digit updates \(x\) to twice its previous value plus that digit. The following choice either adds \(w_i\) to \(y\) or leaves \(y\) unchanged, and resets \(x\) to zero. Therefore, at time \(N\),
\(\displaystyle x_N=0,\qquad y_N=\sum_{i\in I}w_i,\)
where \(I\) is precisely the subset selected by the choice actions.
For every action, define the same reward:
\(\displaystyle g_a(q)= \begin{cases} 1,&s>0,\ t=Ns,\ u=Ts,\\ 0,&\text{otherwise}. \end{cases}\)
This is a permitted piecewise constant reward. An explicit finite rational polyhedral partition is obtained by distinguishing \(s=0\) from \(s>0\), and the three possible signs of each of \(t-Ns\) and \(u-Ts\). There are only constantly many cells.
The clock increases at every step, including after the schedule. Consequently a trajectory can receive a nonzero reward only at time \(N\), and receives it exactly when its selected subset sums to \(T\). Thus every admissible trajectory has value either \(0\) or \(\gamma^N\), and
\(\displaystyle V^*(\mu_0)= \begin{cases} \gamma^N,&\text{if the SUBSET SUM instance is positive},\\ 0,&\text{otherwise}. \end{cases}\)
Every subset can also be implemented by a finite rational polyhedral stationary policy: assign its chosen action to each choice slice \(G_k\), the prescribed action to each digit slice, and \(a_0\) to each complementary cell. Thus the positive value is attainable within the required output class.
4. The approximation gap and policy extraction
Set
\(\displaystyle \gamma=1-\frac1{2N},\qquad \varepsilon=\frac14.\)
Bernoulli’s inequality gives
\(\displaystyle \gamma^N=\left(1-\frac1{2N}\right)^N\ge1-\frac N{2N}=\frac12.\)
On a positive SUBSET SUM instance, any policy satisfying the requested guarantee must therefore have
\(\displaystyle V^\pi(\mu_0)\ge V^*(\mu_0)-\frac14\ge\frac14>0.\)
Because the only possible values are \(0\) and \(\gamma^N\), that policy must select a subset summing to \(T\).
Suppose a polynomial-time synthesis algorithm existed. Run it on the constructed instance, evaluate its explicitly listed policy along the first \(N\) transitions, and test whether \(u_N=Ts_N\). This decides SUBSET SUM:
The extraction is polynomial-time. A polynomial-time algorithm has polynomial-length output; membership in its cells is decidable by exact rational comparisons. Along these trajectories, rational coordinate bit lengths are polynomially bounded, since the denominator at time \(k\) is \(3^k\).
The reduction itself is polynomial-size. There are \(O(N)\) restriction cells; their clock coefficients have \(O(\log N)\) bits. The kernels are fixed, and the target coefficient \(T\) retains its original binary encoding. Moreover,
\(\displaystyle (1-\gamma)^{-1}=2N,\)
which is polynomially bounded in the constructed input length.
This proves \(\mathrm{NP}\)-hardness for \(m=4,\tau=1\), even with rewards in \(\{0,1\}\), constant tolerance, and polynomially bounded inverse discount gap. In particular, unless \(\mathrm{P}=\mathrm{NP}\), there is no algorithm polynomial in \(L\), \(1/\varepsilon\), and \(1/(1-\gamma)\) for this subclass.
Two further parameter regimes follow from the same construction:
These establish the claimed dependence on discounting, accuracy, and reward magnitude.
5. A finite-state synthesis algorithm
We now prove the upper bound for the full stated model, including signed rewards and discontinuous restrictions.
For an affine reward formula
\(\displaystyle g_a(q)=b+\sum_{r\in L(A)}c_rq_r,\)
the simplex conditions imply
\(\displaystyle |g_a(q)|\le |b|+\max_r|c_r|.\)
Taking the maximum of this expression over all listed formulas gives a rational bound \(M\). If \(M=0\), every admissible policy has value zero.
Assume \(M>0\), and choose \(H\ge1\) with
\(\displaystyle C_H:=\frac{M\gamma^H}{1-\gamma}\le\frac{\varepsilon}{2}.\)
Enumerate all admissible action prefixes of lengths less than \(H\). Let \(S\) be the set of distinct states reached by these prefixes. For \(m\ge2\),
\(\displaystyle |S|\le\sum_{k=0}^{H-1}m^k\le m^H.\)
All these states are rational. Exact matrix multiplication and exact cell-membership tests suffice to generate them and remove duplicates.
Construct a finite discounted deterministic MDP on \(S\cup\{\partial\}\), where \(\partial\) is an absorbing state with reward zero. At \(s\in S\):
This finite MDP has an optimal deterministic stationary policy. For completeness, its optimal values are obtained by the rational linear program
\(\displaystyle \min \sum_{s\in S}v_s,\)
subject to \(v_\partial=0\) and
\(\displaystyle v_s\ge \bar R(s,a)+\gamma v_{\widehat F_a(s)} \quad\text{for every }s\in S,\ a\in\Psi(s).\)
To justify the program, its Bellman operator is monotone and is a contraction with factor \(\gamma<1\) in the supremum norm. It has a unique fixed point \(W\). Every feasible vector \(v\) satisfies \(v\ge Tv\), so iteration and contraction give \(v\ge W\) coordinatewise. Conversely, \(W\) satisfies every constraint. Therefore the program returns \(W\).
Choose at each state an action attaining its Bellman maximum. The resulting stationary policy has value \(W\), because its policy operator is also a contraction and fixes \(W\). Bellman inequalities, iterated along any action sequence, show that \(W\) dominates that sequence’s discounted value. Thus it is the required finite-model optimum. Rational linear programming runs in polynomial time in the listed bit length of this finite model.
6. Extending the policy to all states
First construct an admissible finite rational polyhedral policy on all of \(X\). Pull back every hyperplane appearing in the listed restrictions \(D_a\) through the rational linear map \(q\). Their arrangement, including lower-dimensional faces, partitions \(X\) into rational polyhedral cells.
Membership in every \(D_a\) is constant on each resulting cell. Since the allowed-action set is everywhere nonempty, assign any allowed action to each cell. In dimension \(d=\tau(m!-1)\), this construction has size and running time \((L+\tau m!)^{O(d+1)}\), using standard fixed-dimensional hyperplane-arrangement enumeration and rational feasibility tests.
Override this policy at every point of \(S\) with the finite-MDP action. The overrides admit a finite polyhedral partition without an exponential blow-up in the number of points.
Indeed, choose \(d\) independent coordinates \(\xi_1,\ldots,\xi_d\) on \(X\). To isolate a rational point \(p\) inside its current cell \(C\), replace \(C\) by the singleton \(\{p\}\) and the cells
\(\displaystyle C\cap \{\xi_i=p_i\text{ for }i<j,\ \xi_j<p_j\},\)
\(\displaystyle C\cap \{\xi_i=p_i\text{ for }i<j,\ \xi_j>p_j\}, \qquad 1\le j\le d.\)
Empty cells are discarded. These cells partition \(C\): every point different from \(p\) has a unique first coordinate in which it differs. Retain the previous action on the nonsingleton cells and assign the finite-MDP action at \(p\).
Each override adds at most \(2d\) cells. All actions remain admissible, and the resulting policy \(\pi\) has the required explicit finite rational polyhedral representation.
7. Approximation guarantee and running time
Every admissible trajectory starting at \(\mu_0\) stays in \(S\) through times \(0,\ldots,H-1\), by the definition of \(S\). Its first exit from \(S\), if any, therefore occurs at some time \(k\ge H\).
Couple an original trajectory with its finite-model trajectory until this exit. The finite model thereafter receives zero reward. The absolute difference between their returns is at most
\(\displaystyle \sum_{j=k}^{\infty}\gamma^jM =\frac{M\gamma^k}{1-\gamma}\le C_H.\)
This estimate uses absolute rewards, so it applies to signed rewards.
Let \(W^*(\mu_0)\) be the finite-model optimum. Applying the estimate to arbitrary original action sequences, and then taking their supremum, gives
\(\displaystyle V^*(\mu_0)\le W^*(\mu_0)+C_H.\)
The extended policy agrees with the optimal finite-model policy until an exit, so the same estimate gives
\(\displaystyle V^\pi(\mu_0)\ge W^*(\mu_0)-C_H.\)
Combining these inequalities yields
\(\displaystyle V^\pi(\mu_0)\ge V^*(\mu_0)-2C_H \ge V^*(\mu_0)-\varepsilon.\)
This proves the synthesis guarantee without continuity assumptions.
Coordinates reached within \(H\) updates have bit lengths polynomial in \(H,L,\tau m!\): a common denominator for each input matrix has polynomial bit length, and denominators multiply across successive updates. The finite MDP therefore has polynomial bit length in \(|S|,H,L,\tau m!\). Together with the global partition and singleton refinement, this gives the announced conservative bound
\(\displaystyle (L+\tau m!)^{O(\tau(m!-1)+1)} \,m^{O(H)}\,\operatorname{poly}(H).\)
For \(0<\gamma<1\), one may take
\(\displaystyle H=\max\left\{1,\left\lceil \frac{\log(2M/(\varepsilon(1-\gamma)))}{-\log\gamma} \right\rceil\right\}.\)
Equivalently, with \(\log^+x=\max\{0,\log x\}\),
\(\displaystyle H= O\left( 1+\frac{\log^+(M/\varepsilon)+\log(1/(1-\gamma))} {1-\gamma} \right).\)
For \(\gamma=0\), take \(H=1\).
Consequently, when \(m,\tau\) are fixed, \(M\) is bounded, \(\varepsilon\) is fixed, and \(\gamma\) is bounded away from one, this algorithm is polynomial in \(L\). The hardness constructions vary precisely the parameters that prevent that conclusion.
The finite-society theorem of [Parkes–Procaccia](https://procaccia.info/wp-content/uploads/2020/03/dynamic.pdf) obtains polynomial tractability from a finite symmetry quotient. The construction above shows why fixed continuous-state dimension does not provide the same guarantee. The symbolic method of [Sanner–Delgado–de Barros](https://ssanner.github.io/papers/anu/cont_mdp.pdf) supplies exact finite-horizon dynamic programming, but that does not imply polynomial complexity for the present synthesis problem.
⟨structured verdict parsed — rendered above⟩
The substantive argument is correct under the evidently intended convention that actions are alternatives in \(A\). The reduction establishes NP-hardness for fixed \(m=4\) and \(\tau=1\), and the proposed algorithm produces an admissible finite rational polyhedral stationary policy with the claimed approximation guarantee.
I found no false central step or gap requiring new mathematics. One minor clarification is needed: explicitly identify the action set with \(A\), since the running-time analysis uses exactly \(m\) available actions.
The output addresses both requested parts: complexity for fixed alternative and supported-type counts, and running-time dependence on accuracy and discounting.
The proof uses the following natural readings of the task:
The second reading follows naturally from the rational binary-input model. The third is a standard restriction of the source problem and causes no hardness issue. The first should be stated explicitly because it directly controls the branching bound.
The output correctly distinguishes hardness for particular fixed constants from hardness for every fixed alternative count. It makes no unsupported claim of NP membership or NP-completeness.
Verified.
There are enough ranking coordinates: \(m=4\) gives \(24\) rankings, while the construction uses five distinguished coordinates.
The column-sum assertion is correct. In the coordinate order \(s,t,v,u\), the column sums are:
| Map | Column sums |
|---|---|
| \(B_0\) | \(2,1,2,1\) |
| \(B_1\) | \(3,1,2,1\) |
| \(B_+\) | \(2,1,1,1\) |
| \(B_{\mathrm{skip}}\) | \(2,1,0,1\) |
Consequently, dividing these blocks by \(3\) and sending each residual column mass to \(z\) produces nonnegative, column-stochastic kernels. Sending all mass from every remaining column, including the \(z\) column, to \(z\) completes the definition correctly.
The ratio calculations are also correct. Because \(s'=s/3\), the common scaling cancels in \(t'/s'\), \(v'/s'\), and \(u'/s'\), yielding exactly the four decoded updates listed in the output.
The condition \(s>0\) is maintained along the constructed trajectory. No division by zero occurs. Tests involving the decoded quantities are implemented by rational linear conditions on the original coordinates.
With \(\tau=1\) and \(\rho_1=1\), \(q=\mu_1\), so the constructed rewards and restrictions satisfy anonymity.
Verified.
The source problem is the standard NP-hard binary SUBSET SUM problem with positive integer items. The cited [Polak–Rohwedder–Węgrzycki paper](https://arxiv.org/html/2105.04035v1) concerns this problem and identifies its NP-hardness.
The schedule has exactly \(N=\sum_i(\ell_i+1)\) instructions. Its construction and encoding length are polynomial in the source input length.
The slices \(G_k\) are pairwise disjoint: when \(s>0\), the equations \(t=ks\) and \(t=js\) imply \(k=j\).
The listed complement cells exhaust the complement of the scheduled slices within the simplex:
Thus the restrictions leave an admissible action everywhere, and no boundary is omitted.
The initial state belongs to the simplex. The identities \(s_k=3^{-k}\) and \(c_k=k\) follow from the displayed updates. Hence the trajectory reaches the prescribed instruction slice at every scheduled time.
For each item, the digit updates start with \(x=0\), construct its binary value, and are followed by an action that resets \(x\). The choice action adds precisely that item or adds nothing. Therefore the asserted terminal values of \(x_N\) and \(y_N\) are correct.
The terminal reward is permitted by the input model. Its defining equalities and strict positivity condition are rational polyhedral conditions, and the proposed sign partition explicitly assigns all boundaries.
Since the clock increases at every transition, the reward can occur only at time \(N\). It occurs there exactly when the selected subset sums to \(T\). The asserted values \(0\) and \(\gamma^N\) are therefore correct.
Finally, the output explicitly implements every subset choice using a stationary polyhedral policy. The clock slices distinguish the successive decisions, so stationarity imposes no conflict.
Verified.
For \(N\ge1\), the chosen discount satisfies \(0<\gamma<1\). Bernoulli’s inequality applies and gives the displayed lower bound \(\gamma^N\ge1/2\).
On a positive instance, the synthesis guarantee with tolerance \(1/4\) forces strictly positive return. Since every admissible trajectory has one of the two established returns, the synthesized policy must select a successful subset.
On a negative instance, the terminal equality cannot hold for any admissible trajectory. Thus the extraction test distinguishes the two cases.
The extraction is polynomial-time under the assumed polynomial-time synthesis algorithm:
The restriction cells, target coefficient, initial state, kernels, discount, and tolerance all have polynomial-size encodings. The inverse discount gap is exactly \(2N\), as claimed.
Both further regimes check out:
These parameter choices retain polynomial binary encoding length. The distinction between binary encoding length and numerical reward magnitude or numerical inverse tolerance is handled correctly.
Verified.
For an affine formula on the ranking simplex, the inequality \(\left|\sum_r c_rq_r\right|\le\max_r|c_r|\) holds because the coordinates are nonnegative and sum to one. The proposed \(M\) therefore bounds every absolute reward, including signed rewards and discontinuous pieces.
The choice of \(H\) gives the required discounted tail bound.
Under the action-set convention \(a\in A\), the count \(|S|\le\sum_{k=0}^{H-1}m^k\le m^H\) is valid for \(m\ge2\). Duplicated states only reduce this count.
The finite model retains exactly the admissible original actions at each state in \(S\). Its absorbing state and zero continuation reward are well-defined. Every state has an action because the original restrictions are everywhere nonempty.
The linear-program justification is sound:
This also works for \(\gamma=0\). Signed rewards do not invalidate any of these steps.
The appeal to polynomial-time rational linear programming is appropriate: the model is finite and explicitly encoded, all coefficients are rational, and the argument establishes a finite attained optimum.
Verified.
The affine dimension of \(X\) is \(d=\tau(m!-1)\).
Pulling back the restriction hyperplanes through \(q\) gives rational hyperplanes on this affine space. Their arrangement, intersected with \(X\) and including equality faces, has constant restriction membership on each cell. Assigning an allowed action on every cell is justified by the everywhere-nonempty assumption.
The stated arrangement bound is consistent with standard fixed-dimensional enumeration. The number and coefficient lengths of the input hyperplanes are controlled by \(L+\tau m!\), and rational feasibility testing applies to the listed strict and weak conditions.
The point-isolation construction is correct. Independent affine coordinates distinguish every pair of points in \(X\). Every point of \(C\) different from \(p\) has a unique first differing coordinate and belongs to exactly one listed refinement cell. The singleton and the remaining cells therefore form a disjoint partition of \(C\).
Each override replaces one cell by at most \(2d+1\) cells, increasing the count by at most \(2d\). Previously isolated distinct points are preserved. All defining coefficients remain rational.
The finite-model action is admissible at the overridden point, while the prior admissible action is retained elsewhere. Thus the resulting policy satisfies the required global admissibility and representation conditions.
The zero-reward case also has an admissible output available through this global construction; it does not require optimization.
Verified.
Every admissible original trajectory remains in \(S\) at times strictly below \(H\), since its corresponding prefix is among those used to define \(S\). Therefore its first exit, if any, occurs at time at least \(H\).
The coupling argument correctly compares rewards before the exit and bounds the omitted original tail afterward. If there is no exit, the returns agree. Taking an absolute reward bound makes the estimate valid for signed rewards.
For each original action sequence, its finite-model counterpart has value at most the finite-model optimum. This justifies taking the supremum to obtain \(V^*(\mu_0)\le W^*(\mu_0)+C_H\).
The extended policy follows the finite optimal policy until exit, giving \(V^\pi(\mu_0)\ge W^*(\mu_0)-C_H\). Combining the two inequalities yields the requested error bound.
Repeated states do not break this argument. The finite discounted model is solved with a stationary optimal policy, and the extension assigns one consistent action to each distinct state.
Verified, subject to the action-domain clarification below.
The rational-state bit-length estimate is sound: denominators accumulate across at most \(H\) rational matrix updates, producing lengths polynomial in \(H,L,\tau m!\). Rewards evaluated at these states retain polynomial bit length.
Polynomial work in the finite-model size, together with the arrangement and refinement costs, fits the announced conservative bound \((L+\tau m!)^{O(\tau(m!-1)+1)}m^{O(H)}\operatorname{poly}(H)\).
The explicit formula for \(H\), its asymptotic estimate, and the separate treatment of \(\gamma=0\) are correct. The final polynomial-time conclusion correctly requires bounded reward magnitude, fixed positive tolerance, and discount bounded away from one.
The contextual discussion is accurate. [Parkes–Procaccia, Theorem 4.10](https://procaccia.info/wp-content/uploads/2020/03/dynamic.pdf), uses a finite symmetry quotient under the stated constant-size assumptions. The [Sanner–Delgado–de Barros paper](https://ssanner.github.io/papers/anu/cont_mdp.pdf) discusses exact symbolic finite-horizon methods. Neither cited result is used as an unsupported infinite-horizon complexity theorem.
Minor — Sections 1, 2, and 5: action-domain assumption.
The output uses four actions when \(m=4\), asserts a sole action when \(m=1\), and bounds branching by \(m\). These statements assume that the action set is \(A\). The task evidently intends this social-choice convention, but does not expressly declare the domain of \(a\), and the prover does not make the convention explicit.
Minimum clarification: State that actions range over \(A\). If a separate action set was intended, its cardinality must instead be reflected in the branching and running-time statements.
There are no blocking mathematical issues under the intended reading.
⟨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.