Answer: \(\mathrm{P}\)
Theorem 1 — class: hardness
DEMAND-TF is NP–complete.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Mass-Demand-\(TF_R\): Given a finite type tournament with deterministic winner map, rational type masses, \(R\) rounds, demanded type arcs \(S\), and rational quotas \(\rho\), decide whether nonnegative round-by-type match masses satisfy survivor conservation, deterministic winner transitions, and total mass at least \(\rho\) for every demanded arc.
Let \(C\) be a finite set of types, \(m_i\in\mathbb{Q}_{\ge0}\) their initial masses, and for every distinct \(i,j\in C\) exactly one of \(i o j\) or \(j o i\) hold. An \(R\)-round mass bracket uses match masses \(x^r_{ij}=x^r_{ji}\ge0\), including \(x^r_{ii}\), and survivor masses \(y_i^r\), with \(y_i^0=m_i\).
For each round \(r\), require \(y_i^r=2x^r_{ii}+\sum_{j
e i}x^r_{ij}\) and \(y_i^{r+1}=x^r_{ii}+\sum_{j
e i:\,i o j}x^r_{ij}\). For demanded arcs \(S\), with quotas \(
ho:S o\mathbb{Q}_{\ge0}\), require \(\sum_{r=0}^{R-1}x^r_{ij}\ge
ho(i,j)\) for every \((i,j)\in S\).
Target. Is Mass-Demand-TF_R in \(\mathrm{P}\), or is it NP-hard?
For finite-player Demand-TF, deciding whether a single-elimination seeding realizes every demanded match is NP-complete, even when every demand arc is incident to one vertex. No result for the mass formulation above is stated by the supplied source.
For every fixed number of rounds \(R\), Mass-Demand-TF\(_R\) is in \(\mathrm{P}\). More generally, the same conclusion holds when \(R\) is given explicitly or in unary, since the running time is polynomial in \(R\), \(|C|\), and the binary encoding length of the rational data.
Let \(n=|C|\), and assume \(R\ge 1\). For every round \(r\in\{0,\ldots,R-1\}\) and every unordered pair \(\{i,j\}\), including \(i=j\), introduce one variable \(z_{\{i,j\}}^r\). It represents the symmetric match mass:
\(x_{ij}^r=x_{ji}^r=z_{\{i,j\}}^r\).
Consider the following rational linear system.
For every \(i\in C\), impose the initial-round equations
\(2z_{ii}^0+\sum_{j\ne i}z_{\{i,j\}}^0=m_i.\)
For every \(i\in C\) and \(r\in\{0,\ldots,R-2\}\), impose the inter-round equations
\(2z_{ii}^{r+1}+\sum_{j\ne i}z_{\{i,j\}}^{r+1}=z_{ii}^r+\sum_{j\ne i:\,i\to j}z_{\{i,j\}}^r.\)
For every demanded arc \((i,j)\in S\), impose
\(\sum_{r=0}^{R-1}z_{\{i,j\}}^r\ge \rho(i,j).\)
Finally, impose \(z_{\{i,j\}}^r\ge 0\) for every variable.
All coefficients in this system belong to \(\{-1,0,1,2\}\), while all right-hand sides are input rationals.
Suppose an \(R\)-round mass bracket exists. Set \(z_{\{i,j\}}^r=x_{ij}^r\).
The initial-round equations follow from
\(y_i^0=m_i=2x_{ii}^0+\sum_{j\ne i}x_{ij}^0.\)
For \(0\le r\le R-2\), the matching equation in round \(r+1\) and the survivor equation in round \(r\) give
\(2x_{ii}^{r+1}+\sum_{j\ne i}x_{ij}^{r+1}=y_i^{r+1}=x_{ii}^r+\sum_{j\ne i:\,i\to j}x_{ij}^r.\)
Thus every inter-round equation holds. Nonnegativity and all quota inequalities hold directly by the definition of a feasible bracket. Hence the linear system is feasible.
Conversely, suppose the linear system has a feasible solution \(z\). Define
\(x_{ij}^r=x_{ji}^r=z_{\{i,j\}}^r\)
and set \(y_i^0=m_i\). For \(0\le r\le R-1\), define
\(y_i^{r+1}=z_{ii}^r+\sum_{j\ne i:\,i\to j}z_{\{i,j\}}^r.\)
The survivor equations then hold by definition.
The initial-round matching equation holds by the initial LP equations. For every \(1\le r\le R-1\), the inter-round equation with index \(r-1\) gives
\(2z_{ii}^{r}+\sum_{j\ne i}z_{\{i,j\}}^{r}=z_{ii}^{r-1}+\sum_{j\ne i:\,i\to j}z_{\{i,j\}}^{r-1}=y_i^r.\)
Thus every matching equation holds. The LP quota inequalities give all demanded-match quotas. Therefore \(x,y\) form an \(R\)-round mass bracket.
Consequently, the mass-bracket instance is feasible if and only if this rational linear system is feasible.
The formulation has
\(R\,n(n+1)/2\)
nonnegative variables, \(Rn\) equality constraints, and \(|S|\) quota inequalities. Its encoding length is polynomial in \(R\), \(n\), and the encoding length of \(m\) and \(\rho\).
Feasibility of a rational linear system is decidable in polynomial time in the Turing bit model. This theorem applies because every coefficient and right-hand side above is rational and the entire system has polynomial encoding length. It decides exact real feasibility; moreover, every nonempty rational polyhedron contains a rational feasible point.
Hence Mass-Demand-TF\(_R\) belongs to \(\mathrm{P}\). It therefore cannot be NP-hard under polynomial-time many-one reductions unless \(\mathrm{P}=\mathrm{NP}\).
The finite-player problem contains discrete seeding and integrality constraints. In the mass formulation, match masses are arbitrarily divisible, and all restrictions are linear. The feasible set is therefore a convex rational polyhedron. Even when the initial masses happen to be integers, the definition does not require the variables \(x_{ij}^r\) to be integral, so the finite-player NP-hardness reduction does not apply.
If \(R\) were instead encoded succinctly in binary and allowed to be exponentially large, the explicit formulation would have size proportional to \(R\); that would define a different succinct-horizon problem and is not the fixed-\(R\) problem denoted Mass-Demand-TF\(_R\).
⟨structured verdict parsed — rendered above⟩
The prover correctly reduces Mass-Demand-TF\(_R\) to feasibility of a rational linear system. The variables, equations, and quota inequalities are equivalent to the bracket definition, and the resulting system has polynomial size for fixed \(R\), or when the horizon is represented in unary.
The central answer—Mass-Demand-TF\(_R\) is in \(\mathrm{P}\) for every fixed positive \(R\)—is rigorously established. There are two minor qualifications concerning the representation of variable \(R\) and the unhandled case \(R=0\).
Introducing one variable \(z_{\{i,j\}}^r\) for each unordered pair, including \(\{i,i\}\), correctly incorporates the symmetry condition
\[ x_{ij}^r=x_{ji}^r. \]
There are \(n(n+1)/2\) such variables per round, hence \(Rn(n+1)/2\) variables in total. This count is correct.
The equations
\[ 2z_{ii}^0+\sum_{j\ne i}z_{\{i,j\}}^0=m_i \]
are exactly the round-\(0\) matching equations after substituting \(y_i^0=m_i\). No condition is lost.
For \(0\le r\le R-2\), the equation
\[ 2z_{ii}^{r+1}+\sum_{j\ne i}z_{\{i,j\}}^{r+1} = z_{ii}^r+\sum_{j\ne i:\,i\to j}z_{\{i,j\}}^r \]
equates the mass assigned to matches in round \(r+1\) with the mass surviving round \(r\). This is exactly what results from eliminating \(y_i^{r+1}\) between the matching and survivor equations.
The indexing is correct: these equations enforce the matching equation for rounds \(1,\ldots,R-1\). No matching equation is required after the last round, while \(y_i^R\) may still be defined as the final survivor mass.
The inequalities
\[ \sum_{r=0}^{R-1}z_{\{i,j\}}^r\ge \rho(i,j) \]
are exactly the demanded-arc quota constraints. Using an unordered-pair variable causes no problem because the match mass is symmetric even though the tournament orientation determines its survivor.
All required nonnegativity conditions on match masses are explicitly imposed.
Given a bracket, setting \(z_{\{i,j\}}^r=x_{ij}^r\) satisfies:
This implication is complete.
Given a feasible \(z\), the definitions
\[ x_{ij}^r=x_{ji}^r=z_{\{i,j\}}^r \]
and
\[ y_i^{r+1}=z_{ii}^r+\sum_{j\ne i:\,i\to j}z_{\{i,j\}}^r \]
ensure symmetry, nonnegativity, and every survivor equation.
The initial LP equation gives the matching equation at \(r=0\). For \(1\le r\le R-1\), the inter-round equation indexed by \(r-1\) gives
\[ 2z_{ii}^{r}+\sum_{j\ne i}z_{\{i,j\}}^{r}=y_i^r. \]
Thus all matching equations are recovered. Quotas follow directly. This establishes exact equivalence.
The constraint count is correct:
\[ n+n(R-1)=Rn \]
equalities, together with \(|S|\) quota inequalities and nonnegativity constraints.
All coefficients are rational with polynomial encoding length, so standard rational linear-programming feasibility algorithms decide the system in polynomial time. For fixed \(R\), the formulation has polynomial size in the original instance. The observation that rational feasibility can be witnessed by a rational point is correct, though not essential to the decision argument.
The explanation correctly identifies why the cited finite-player hardness does not imply hardness here: the mass problem permits divisible variables and imposes no integrality constraints. The prover does not improperly rely on the finite-player result.
⟨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.