Complexity Theory

Motivation

In multi-agent scheduling, several decision makers share one processing resource, and each one cares only about the completion of its own jobs. Agnetis, Mirchandani, Pacciarelli and Pacifici (Oper. Res. 52(2), 2004) set up the two-agent version of this problem and classified its complexity for most combinations of classical objectives. Typical settings are a manufacturing cell that serves an internal and an external customer, or two departments that negotiate access to a shared machine. Most of the paper treats a single machine. Its §10 asks what happens when the shared resource is a small shop: two machines that every job must visit.

The answer is that even the simplest two-machine case is hard. In the classical single-agent setting, the two-machine flow shop makespan problem is solved by Johnson's rule (Johnson 1954) and the two-machine open shop makespan problem by Gonzalez and Sahni (1976), both in polynomial time. As soon as two agents each want their own jobs finished early, both problems become NP-hard.

Setting

There are two agents, A and B. Agent A owns jobs $J^A_1,\dots,J^A_{n_A}$ and agent B owns jobs $J^B_1,\dots,J^B_{n_B}$. Every job consists of one operation on machine $M_1$ and one on machine $M_2$, and $p^X_{ih}\ge 0$ is the processing time of job $J^X_i$ on machine $M_h$. A schedule gives every operation a start time. It is feasible when no operation starts before time $0$, each machine processes at most one operation at a time, and the two operations of one job do not overlap in time. Processing is nonpreemptive.

• In the flow shop $F2$ every job is processed first on $M_1$ and then on $M_2$.
• In the open shop $O2$ the two operations of a job may be processed in either order.

The makespan of agent $X$, $C^X_{\max}$, is the latest completion time of an operation of one of its jobs. The recognition problem $F2\|C^A_{\max}\le Q_A,\ C^B_{\max}\le Q_B$ asks, for given thresholds $Q_A, Q_B$, whether some feasible flow shop schedule has $C^A_{\max}\le Q_A$ and $C^B_{\max}\le Q_B$. The problem $O2\|C^A_{\max}\le Q_A,\ C^B_{\max}\le Q_B$ is the same question for the open shop.

PARTITION (Problem 9.1 of the paper) asks whether a finite list of nonnegative integers $p_1,\dots,p_k$ can be split into two parts of equal sum $P/2$, where $P=\sum_i p_i$.

Formalization targets

Goal: Theorems 10.1 and 10.2

$$\text{PARTITION}\ \le_p\ F2\,\|\,C^A_{\max}\le Q_A,\ C^B_{\max}\le Q_B \qquad\text{and}\qquad \text{PARTITION}\ \le_p\ O2\,\|\,C^A_{\max}\le Q_A,\ C^B_{\max}\le Q_B,$$

with $\le_p$ polynomial-time many-one reducibility between binary-coded languages. This is how the paper proves "$F2\|C^A_{\max}:C^B_{\max}$ is NP-hard" (Theorem 10.1, p. 238) and "$O2\|C^A_{\max}:C^B_{\max}$ is NP-hard" (Theorem 10.2, p. 239).

Milestones: the two constructions

For Theorem 10.1, with $\varepsilon=1/(k+1)$, the paper builds the instance with $k$ A-jobs of times $(\varepsilon, p_i)$, one B-job of times $(P/2-(k-1)\varepsilon,\ P/2)$, and thresholds $Q_A = 3P/2+\varepsilon$, $Q_B = P+\varepsilon$. The milestones are:

1. under $C^B_{\max}\le Q_B$ the B-job starts on $M_2$ by $P/2+\varepsilon$, and the A-jobs before it on $M_2$ total at most $P/2$;
2. for even $P$, PARTITION has a solution if and only if this instance meets both thresholds.

For Theorem 10.2 the instance has $k$ A-jobs of time $p_i$ on both machines, one B-job of time $P/2$ on both machines, and thresholds $Q_A=3P/2$, $Q_B=P$. The milestones are:

3. under $C^B_{\max}\le Q_B$ the B-job starts at $0$ on one machine and at $P/2$ on the other;
4. PARTITION has a solution if and only if this instance meets both thresholds.

Significance

The two theorems mark the boundary of tractability of §10. The single-agent problems $F2\|C_{\max}$ and $O2\|C_{\max}$ are polynomial. Giving the second agent a single job and a deadline is already enough to make the problems NP-hard, so no extension of Johnson's rule or of the Gonzalez–Sahni algorithm solves the two-agent versions unless P = NP. The paper also observes that any other combination of the objectives it considers is NP-hard in these shops.

The theorems are proved in the paper by short reductions. As far as we know none of them is machine-checked. This mission produces checked statements of both reductions on a general two-machine shop model with real start times. It also corrects the flow shop equivalence, which as printed does not hold for odd $P$.

Difficulty

The hard direction of each equivalence goes from a feasible schedule to a partition. A schedule is a set of real start times, not a permutation. Nothing forces the jobs into a fixed order or rules out idle time. The proof has to extract a combinatorial split from interval packing: which A-jobs fit into the gap before the B-job on one machine and which fit into the gap after it. The sum of lengths of pairwise disjoint intervals inside a window must be bounded by the window's length.

In the flow shop the gap after the B-job has length $P/2+k\varepsilon$, which is not $P/2$. Integrality of the A-lengths is what closes the gap, and it only works when $P/2$ is an integer. In the open shop, the same argument has to cover both orders of the B-job's operations. Both reductions output rational data, so the goal also needs a scaling to integer data and a polynomial-time bound on the code map.

Formalization scope

• Model. Jobs are numbered Fin (n_A + n_B), the A-jobs first. Start times are real numbers, and idle time and different job orders on the two machines are allowed. Flow shop feasibility is the published JohnsonFlowShop.TwoStage.IsFeasible from the Johnson (1954) series. Open shop feasibility is the definition IsOpenFeasible of this mission: no machine overlap between distinct jobs, and no time overlap between the two operations of a job. "$C^X_{\max}\le Q_X$" is stated as "every operation of every $X$-job ends by $Q_X$", so no maximum over a possibly empty set is taken.
• Languages. The target languages hold the binary codes of instances with natural-number processing times and thresholds that have a feasible schedule meeting both thresholds. PARTITION is the published ProjSchedTW.Complexity.partitionLang (nonnegative sizes, zero allowed), and reducibility is CookPvsNP.PolyReducible. Both come from published definitions of the Neumann–Schwindt–Zimmermann and Cook series. NP-membership is not formalized.
• Constructions. They are defined over $\mathbb R$ exactly as printed. A reduction to the $\mathbb N$-coded languages has to rescale (for example by $2(k+1)$). That rescaling is the solver's to choose and is not a milestone.
• Corrections. The printed flow shop equivalence uses $\lfloor P/2+k\varepsilon\rfloor = P/2$ and fails for odd $P$: $p=(1)$ gives a yes-instance of the scheduling problem but has no partition. It also fails for $P=0$ and $k\ge 2$, where the printed $p^B_{11}$ is negative. Milestone 2 therefore assumes $P$ even and ($P\ge2$ or $k\le1$). The goal is unaffected, because odd $P$ is a PARTITION no-instance. In the open shop proof, the printed identity "$\sum p^A_i+\sum p^B_i = 2P$" is read as "each machine carries $3P/2$ of work", and the statement is unchanged.
• No trivialization. The flow shop and open shop languages are not restricted to the instances the constructions produce, so they cannot be decided by reading off the construction. A schedule must satisfy the machine and job non-overlap constraints, including in the open shop, where a definition without the job constraint would let a job run on both machines at once.
• Welcome contributions. Interval-packing lemmas on $\mathbb R$, a polynomial-time bound for list arithmetic over encNats, and a scaling lemma for shop schedules are reusable beyond this mission.

Selected references

• A. Agnetis, P. B. Mirchandani, D. Pacciarelli, A. Pacifici, Scheduling Problems with Two Competing Agents, Operations Research 52(2) (2004) 229–242. https://doi.org/10.1287/opre.1030.0092
• S. M. Johnson, Optimal two- and three-stage production schedules with setup times included, Naval Research Logistics Quarterly 1 (1954) 61–68. https://doi.org/10.1002/nav.3800010110
• T. Gonzalez, S. Sahni, Open shop scheduling to minimize finish time, Journal of the ACM 23(4) (1976) 665–679. https://doi.org/10.1145/321978.321985
• M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979.

Two agents sharing one machine

In many production and service settings a single resource is shared by parties with different goals: two departments sending orders to the same machine, two customers of a contract manufacturer, or two classes of requests on one processor. Multi-agent scheduling models this directly. Each agent owns its own jobs and its own objective, and a schedule is judged by the pair of objective values it gives the two agents rather than by a single combined criterion.

Agnetis, Mirchandani, Pacciarelli and Pacifici (Oper. Res. 52(2), 2004, pp. 229–242) set up the systematic study of the two-agent single-machine problem. For each pair of classical objectives they ask how hard it is to optimise one agent's objective while the other agent's objective stays within a given bound. This mission formalises their §9, the case in which both agents minimise their own total completion time. With a single agent, minimising the total completion time is solved by sorting the jobs by length (the shortest-processing-time rule of Smith, 1956). §9 shows that two agents, each with this easiest of objectives, already give an NP-hard problem (Theorem 9.2), and that the problem is solved in pseudopolynomial time by a dynamic program (Theorem 9.3).

Setting

There are two agents, A and B. Agent A owns jobs $J^A_1,\dots,J^A_{n_A}$ with processing times $p^A_h\in\mathbb N$; agent B owns jobs $J^B_1,\dots,J^B_{n_B}$ with processing times $p^B_k\in\mathbb N$. All jobs are available at time $0$ and are processed on one machine, one at a time, without interruption. Since both objectives are nondecreasing in the completion times, a schedule $\sigma$ is a sequence of all $n_A+n_B$ jobs processed back to back from time $0$. The completion time $C_j(\sigma)$ of a job is the total processing time of the job and of all jobs before it. Agent A's cost is $\sum_hC^A_h(\sigma)$ and agent B's cost is $\sum_kC^B_k(\sigma)$.

The recognition problem $1\|\sum C^A_i\le Q_A,\ \sum C^B_i\le Q_B$ asks, for thresholds $Q_A,Q_B$, whether some schedule has

$$\sum_{h=1}^{n_A}C^A_h(\sigma)\le Q_A\qquad\text{and}\qquad\sum_{k=1}^{n_B}C^B_k(\sigma)\le Q_B .$$

The source problem is PARTITION (Problem 9.1): given integers $p_1,\dots,p_k$ with $P=\sum_ip_i$, is there a set $S\subseteq\{1,\dots,k\}$ with $\sum_{i\in S}p_i=\sum_{i\notin S}p_i=P/2$?

The paper's reduction numbers the integers so that $p_1\le\dots\le p_k$ and gives both agents identical job sets, $k$ jobs of lengths $p_1,\dots,p_k$, with thresholds $Q_A=Q_B=T/2$, where

$$T=3P+4\sum_{i=1}^k(k-i)p_i .$$

Writing $J[i]$ for the pair $J^A_i,J^B_i$, an SPT schedule processes $J[1],\dots,J[k]$ in order, each pair in either internal order; $x$ denotes the total length of the pairs in which B goes first.

Formalization targets

Goal: Theorem 9.2

$$\text{PARTITION}\ \le_p\ 1\|\textstyle\sum C^A_i\le Q_A,\ \sum C^B_i\le Q_B$$

Here $\le_p$ is polynomial-time many-one reducibility between languages of binary codes: a polynomial-time Turing-machine-computable map on strings that sends codes of PARTITION yes-instances, and only those, to codes of yes-instances of the recognition problem. Together with the NP-completeness of PARTITION (Karp 1972) this is the statement "$1\|\sum C^A_i : \sum C^B_i$ is binary NP-hard".

Milestones of the proof

1. Every SPT schedule has $\sum C^A_i+\sum C^B_i=T$, and $Q_A=Q_B=T/2$.
2. Eqs. (5) and (6): in an SPT schedule, $\sum C^A_i=P+2\sum_i(k-i)p_i+x$ and $\sum C^B_i=P+2\sum_i(k-i)p_i+(P-x)$.
3. A schedule with $\sum C^A_i\le T/2$ and $\sum C^B_i\le T/2$ processes the jobs in nondecreasing order of length.
4. For pairwise distinct $p_1<\dots<p_k$: PARTITION has a solution iff some schedule meets $T/2$ for both agents.

Further result: Theorem 9.3 with recursion (7)

With each agent's jobs numbered by nondecreasing length and $P(i,j)$ the total length of $J^A_1,\dots,J^A_i,J^B_1,\dots,J^B_j$, the recursion

$$F(i,j,q)=\min\bigl\{F(i-1,j,q)+P(i-1,j)+p^A_i;\ F(i,j-1,q-P(i,j))\bigr\}$$

with $F(0,0,q)=0$ for $q\ge0$ and $F=+\infty$ for $q<0$ yields $F(n_A,n_B,Q)=\min\{\sum C^A_i:\sum C^B_i\le Q\}$, and $+\infty$ when no schedule meets the bound.

Significance

Theorem 9.2 fills one cell of the paper's complexity table: even when both agents use the objective that is trivial for one agent, sharing the machine makes the constrained problem NP-hard. Together with Theorem 9.3 it places $1\|\sum C^A_i:\sum C^B_i$ exactly: NP-hard under binary encoding, solvable in pseudopolynomial time, hence not strongly NP-hard unless P = NP. The later literature on two-agent and multi-agent scheduling (for example the monograph of Agnetis, Billaut, Gawiejnowicz, Pacciarelli and Soukhal, Multiagent Scheduling, Springer 2014) cites this classification.

Neither result has a machine-checked proof that we know of. The mission adds a formal record of the reduction and of the dynamic program, reusable definitions for the two-agent total-completion-time problem, and a correction of the printed proof: the equivalence between PARTITION and the constructed instance, as printed, holds only when the integers are pairwise distinct. For $p=(1,1,1,1,10)$ PARTITION has no solution, yet a schedule meets $T/2=41$ for both agents. Theorem 9.2 itself is not affected, since PARTITION remains NP-hard, but a complete formal proof needs a reduction that is correct on every input.

Difficulty

The equivalence for distinct integers rests on two facts: the overall total $\sum C^A_i+\sum C^B_i$ is at least $T$ for every schedule, with equality only for sequences in nondecreasing order of length; and, with distinct lengths, such a sequence is made of consecutive pairs, whose split is controlled by $x$. The naive formal argument stops at the second fact, which is false with repeated lengths: a block of equal-length jobs can be shared between the agents in ways no sequence of pairs realises. The goal adds the encoding layer: the reduction must be computable in polynomial time on a Turing machine, must handle repeated and zero sizes and odd $P$ (where $T/2$ is not an integer and the language's thresholds are), and must send strings that do not code a PARTITION instance outside the target language. For Theorem 9.3, the dynamic program is correct only because some optimal schedule orders each agent's jobs by length, and the constraint makes this exchange argument less direct than for a single agent.

Formalization scope

Jobs are Fin nA ⊕ Fin nB (Sum.inl h is $J^A_{h+1}$, Sum.inr k is $J^B_{k+1}$, 0-based). Schedules, completion times and the idle-free sequence model are the published MooreLateJobs.Shared.completionTime (Moore 1968 series): a schedule is a duplicate-free list containing every job once, and completion times are real numbers. Processing times and thresholds of the language are natural numbers. Reducibility is the published CookPvsNP.PolyReducible, and PARTITION, the alphabet and the binary codes are the published ProjSchedTW.Complexity.Encoding (partitionLang, whose sizes are natural numbers including $0$). The target language allows any job counts and any processing times; identical job sets are a property of the construction only.

The following readings are explicit:

• An SPT schedule of the construction is given by a choice $x:\mathrm{Fin}\,k\to\mathrm{Bool}$ of the first agent in each pair; "feasible implies SPT" is stated as "lengths are nondecreasing along the sequence", which is what the paper's exchange argument proves.
• The milestones take the integers already sorted, as a hypothesis; the paper's thresholds $T/2$ are real numbers in the milestones.
• The equivalence milestone assumes $p_1<\dots<p_k$; the printed version with $\le$ is false, as shown above.
• In recursion (7), the terms $F(-1,j,q)$ and $F(i,-1,q)$ that the paper leaves undefined are $+\infty$.
• The running time $O(n_An_BQ)$ of Theorem 9.3 is not formalised; only the correctness of (7) is. Membership in NP is not formalised.

The goal cannot be met by a trivial reduction: PolyReducible requires the map to be computed by a polynomial-time Turing machine and to be correct on every string, and the target language contains every two-agent instance, not only those with identical job sets. Contributions welcome: the exchange lemmas for total completion time on the shared sequence model, the SPT formulas, and Turing-machine constructions for list sorting and arithmetic on binary codes, which other reductions of this series reuse.

Selected references

• A. Agnetis, P. B. Mirchandani, D. Pacciarelli, A. Pacifici, Scheduling Problems with Two Competing Agents, Operations Research 52(2) (2004) 229–242. https://doi.org/10.1287/opre.1030.0092
• R. M. Karp, Reducibility among Combinatorial Problems, in Complexity of Computer Computations, Plenum (1972) 85–103. https://doi.org/10.1007/978-1-4684-2001-2_9
• W. E. Smith, Various Optimizers for Single-Stage Production, Naval Research Logistics Quarterly 3 (1956) 59–66. https://doi.org/10.1002/nav.3800030106
• J. M. Moore, An n Job, One Machine Sequencing Algorithm for Minimizing the Number of Late Jobs, Management Science 15(1) (1968) 102–109. https://doi.org/10.1287/mnsc.15.1.102
• S. Cook, The P versus NP Problem, Clay Mathematics Institute Millennium Problems (2000). https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf
• A. Agnetis, J.-C. Billaut, S. Gawiejnowicz, D. Pacciarelli, A. Soukhal, Multiagent Scheduling: Models and Algorithms, Springer (2014). https://doi.org/10.1007/978-3-642-41880-8

Two agents sharing one machine

In many production and logistics settings a single resource is shared by parties with different goals: two departments of a plant that send orders to the same machine, two customers of a contract manufacturer, or two classes of traffic on one processor. Multi-agent scheduling models this directly. Each agent owns its own jobs and its own objective, and a schedule is judged by the pair of objective values it gives the two agents rather than by one combined criterion.

Agnetis, Mirchandani, Pacciarelli and Pacifici (Oper. Res. 52(2), 2004, pp. 229–242) set up the systematic study of the two-agent single-machine problem. For each pair of classical objectives they ask how hard it is to optimise one agent's objective while the other agent's objective stays within a given bound. Their Table 1 lists the outcome for each pair. This mission formalises one entry, Theorem 5.2: when agent A minimises its total weighted completion time and agent B only requires its makespan to stay below a bound, the problem is NP-hard under binary encoding of the numbers. The corresponding single-agent bicriteria problem had been shown NP-hard in the strong sense by Lenstra, Rinnooy Kan and Brucker (1977); the two-agent version differs because only B's jobs are constrained.

Setting

There are two agents, A and B. Agent A owns jobs $J^A_1,\dots,J^A_{n_A}$; job $J^A_h$ has a processing time $p^A_h\in\mathbb N$ and a weight $w^A_h\in\mathbb N$. Agent B owns jobs $J^B_1,\dots,J^B_{n_B}$ with processing times $p^B_k\in\mathbb N$. All jobs are available at time $0$ and are processed on one machine, one at a time, without interruption.

Because both objectives are nondecreasing in the completion times, there is no reason to leave the machine idle, so a schedule $\sigma$ is a sequence of all $n_A+n_B$ jobs processed back to back from time $0$. The completion time $C_j(\sigma)$ of a job $j$ is the total processing time of $j$ and of all jobs sequenced before it. Agent A's cost is $\sum_{h}w^A_hC^A_h(\sigma)$; agent B's cost is its makespan $C^B_{\max}(\sigma)=\max_kC^B_k(\sigma)$.

The paper's recognition problem $1\|\sum w_iC^A_i\le Q_A,\ C^B_{\max}\le Q_B$ asks, for given thresholds $Q_A,Q_B$, whether some schedule has

$$\sum_{h=1}^{n_A}w^A_hC^A_h(\sigma)\le Q_A\qquad\text{and}\qquad C^B_k(\sigma)\le Q_B\ \text{ for all }k .$$

The source problem is KNAPSACK (Problem 5.1): given nonnegative integers $u_1,\dots,u_n$, $w_1,\dots,w_n$ and integers $b,W$, is there $S\subseteq\{1,\dots,n\}$ with $\sum_{i\in S}u_i\le b$ and $\sum_{i\in S}w_i\ge W$?

Formalization targets

Goal: Theorem 5.2

$$\text{KNAPSACK}\ \le_p\ 1\|\textstyle\sum w_iC^A_i\le Q_A,\ C^B_{\max}\le Q_B$$

Here $\le_p$ is polynomial-time many-one reducibility between languages of binary codes: a Turing-machine-computable, polynomial-time map on strings sending codes of KNAPSACK yes-instances, and only those, to codes of yes-instances of the recognition problem. Together with the NP-completeness of KNAPSACK (Garey and Johnson 1979) this is the statement "$1\|\sum w_iC^A_i : C^B_{\max}$ is binary NP-hard".

Milestones

The paper's reduction builds, from a KNAPSACK instance, the two-agent instance with $p^A_i=u_i$, $w^A_i=w_i$, a single B-job of length $p^B_1=\hat w\hat u$ (where $\hat u=\sum_iu_i$, $\hat w=\sum_iw_i$), and thresholds $Q_B=b+p^B_1$, $Q_A=\hat w\hat u+(\hat w-W)p^B_1$. The milestones are the two directions of the proof and their combination:

1. Eq. (1): if $S$ solves KNAPSACK, every sequence with exactly the A-jobs of $S$ before the B-job meets both thresholds.
2. Eq. (2): if $\sum_iw_iu_i>0$ and a sequence meets both thresholds, the A-jobs before the B-job solve KNAPSACK.
3. Equivalence: under $\sum_iw_iu_i>0$, KNAPSACK is a yes-instance iff the constructed instance is.
4. §8: with every B-job given due date $Q$ and $Q'=0$, a sequence meets $\sum U^B_i\le Q'$ (and A's bound) iff it meets $C^B_{\max}\le Q$, which carries the hardness over to $1\|\sum w_iC^A_i:\sum U^B_i$.

Significance

Theorem 5.2 fixes the complexity of one cell of the two-agent classification. It shows that the polynomial algorithm for the unweighted case $1\|\sum C^A_i:f^B_{\max}$ (Theorem 5.5 of the same paper) cannot be extended to arbitrary weights unless P = NP. Through §8 it also settles $1\|\sum w_iC^A_i:\sum U^B_i$. The hardness is binary, not strong: the reduction produces numbers of size about $\hat w\hat u$, so pseudo-polynomial algorithms are not ruled out, which is consistent with the dynamic programs studied in later two-agent literature.

The result is proved in the paper; no machine-checked proof is known to exist. Formalizing it produces a complete reduction from a two-constraint knapsack problem to a scheduling recognition problem, with the encoding, the degenerate instances and the polynomial running time all made explicit. The model and the KNAPSACK language are reusable by other two-agent reductions (Theorems 9.2, 10.1 and 10.2 of the paper reduce from PARTITION in the same frame).

Difficulty

The two directions of the equivalence are short computations with completion times. The printed argument, however, is not correct as written in two places. The bounds "smaller than $\hat w\hat u$" and "smaller than $(\hat w-W)p^B_1$" in the derivation of (1) hold only with equality allowed. The strict inequalities in (2) fail when $\sum_iw_iu_i=0$, and then the reduction itself fails: with all $u_i=0$ and $W>\hat w$ the KNAPSACK instance is a no-instance while the constructed instance has $Q_A=Q_B=0$ and every schedule meets both thresholds. A complete reduction must recognise such instances and treat them separately.

The construction also produces integer thresholds that can be negative ($b<-p^B_1$, or $W>\hat w+1$), while instances of the target are coded with natural numbers. Finally, the reduction must be a polynomial-time Turing machine computation over binary codes, including the decoding of arbitrary strings and the binary multiplication $\hat w\hat u$; that is where most of the formal work lies.

Formalization scope

• Model. Jobs are Fin nA ⊕ Fin nB (0-based: Sum.inl h is $J^A_{h+1}$, Sum.inr k is $J^B_{k+1}$). Schedules and completion times are the published MooreLateJobs.Shared sequence model (IsSchedule, completionTime) of the Moore (1968) series: a duplicate-free list of all jobs, processed without idle time from time $0$. Integer processing times are cast to $\mathbb R$.
• Makespan bound. $C^B_{\max}\le Q_B$ is written as $C^B_k\le Q_B$ for every B-job; no nonemptiness of B's job set is assumed.
• Languages. Polynomial-time reducibility is the published CookPvsNP.PolyReducible (Cook's Definition 3, one-tape Turing machines). Codes use the published binary encoding ProjSchedTW.Complexity.Encoding (alphabet BSym, encNat, encInt) of the Neumann–Schwindt–Zimmermann series. A KNAPSACK instance is coded as the integers $n,u_1,\dots,u_n,w_1,\dots,w_n,b,W$; a target instance as the natural numbers $n_A,n_B$, the processing times and weights, and $Q_A,Q_B$. The target language allows any $n_A,n_B\ge0$; the reduction uses $n_B=1$.
• Readings of the paper. "Binary NP-hard" is formalised as the reduction from KNAPSACK, without the NP-completeness of KNAPSACK and without membership in NP. The milestone Eq. (2) and the equivalence carry the added hypothesis $\sum_iw_iu_i>0$; the inequalities "smaller than" in (1) are read as $\le$. Eq. (1) is stated for every order of the jobs inside $S$ and inside its complement. The §8 result is stated as the encoding-free equivalence of feasible solutions, not as a reduction between languages.
• Ruled out. The goal cannot be met by a reduction that ignores the input: the equivalence must hold for every string, and the target language is exactly the codes of yes-instances of the two-agent recognition problem with B's objective the makespan. KNAPSACK here is the two-constraint problem of Problem 5.1, not subset sum.

Contributions welcome: proofs of the two directions, of the equivalence, the treatment of the degenerate instances, and the Turing machine for the reduction, which would also serve the other binary-coded reductions on the platform.

Selected references

• A. Agnetis, P. B. Mirchandani, D. Pacciarelli, A. Pacifici, Scheduling Problems with Two Competing Agents, Operations Research 52(2) (2004) 229–242. https://doi.org/10.1287/opre.1030.0092
• M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979.
• J. K. Lenstra, A. H. G. Rinnooy Kan, P. Brucker, Complexity of Machine Scheduling Problems, Annals of Discrete Mathematics 1 (1977) 343–362. https://doi.org/10.1016/S0167-5060(08)70743-X
• S. Cook, The P versus NP Problem, Clay Mathematics Institute Millennium Problem description. https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf
• J. M. Moore, An n Job, One Machine Sequencing Algorithm for Minimizing the Number of Late Jobs, Management Science 15(1) (1968) 102–109. https://doi.org/10.1287/mnsc.15.1.102

Why expected recourse is a counting question

A two-stage stochastic program chooses a first action before uncertainty is observed and then takes a recourse action after the observation. Evaluating the expected optimal recourse value can be difficult even when the recourse problem for each fixed observation is a small linear program. This mission isolates the example in Section 3 of Hanasusanto, Kuhn and Wiesemann's preprint: the second-stage program has no first-stage decision at all, yet sufficiently accurate expected values determine how many ways a finite partial order can be arranged into a total order.

The counting connection has a specific history. Brightwell and Winkler (1991) established the complexity of counting linear extensions and related their number to an order-polytope volume. Hanasusanto, Kuhn and Wiesemann use that relation in their October 2015 preprint to establish Theorem 3's strong #P-hardness claim for approximate expected recourse with random recourse coefficients. The mission addresses the exact mathematical relation and the error threshold that support that claim. The complexity-class and encoding parts are outside its Lean statement.

Finite orders, volumes, and program (10)

Let $P$ be a finite partially ordered set with $k=|P|$. A linear extension lists its elements in a total order that respects the partial order. The number of these lists is $N(P)$. The unit cube is $C=[0,1]^P$. Its order polytope is

$$O(P)=\{\xi\in C:\xi_i\le\xi_j\text{ whenever }i\le_P j\}.$$

Write $V(P)$ for the Lebesgue volume of $O(P)$. The paper writes $S=\{1,\ldots,k\}$ and $P(S;\preceq)$ for this polytope; changing the names of the elements does not change either the count or the volume.

For a realization $\xi\in C$, define $q_P(\xi)$ as the optimal objective value of the paper's random-recourse program (10). It maximizes a scalar $z$, subject to $0\le z\le1$, nonnegative variables $y_{ij}$, and

$$z\le\sum_{i,j\in P:\,i\le_P j}(\xi_i-\xi_j)y_{ij}.$$

The sum includes reflexive pairs, for which the summand is zero. The expected recourse value is $Q(P)=\int_C q_P(\xi)\,d\xi$. Lebesgue measure of $C$ is one, so this integral is the expectation under the uniform distribution on the cube. The program is feasible for every $\xi$: $y=0$ and $z=0$ are allowed. Its objective is bounded by one because $z\le1$. These details give the value a genuine finite meaning at every realization.

Formalization targets

The first target is the exact value of the second stage for every $\xi\in C$:

$$q_P(\xi)=\mathbf 1_{C\setminus O(P)}(\xi).$$

Consequently, the expected recourse value satisfies the displayed identity in the proof of Theorem 3:

$$Q(P)=1-V(P).$$

The counting target quoted in the proof of Lemma 3 is

$$N(P)=k!\,V(P).$$

Lemma 3's rounding step concerns an approximation $\vartheta$ of $V(P)$. If $|\vartheta-V(P)|\le\varepsilon$ and $0\le\varepsilon<1/(2k!)$, then $|k!\vartheta-N(P)|<1/2$. The mission's main goal uses an approximation of $Q(P)$, as in Theorem 3. Under the same strict error threshold,

$$|\vartheta-Q(P)|\le\varepsilon \quad\Longrightarrow\quad \left|k!(1-\vartheta)-N(P)\right|<\frac12.$$

The target leaves no independent dimension parameter or unspecified oracle value: $k$ is the cardinality of the very poset used in program (10), and $\vartheta$ must approximate that program's expected value. The strict half-unit bound makes $N(P)$ the unique nearest integer to $k!(1-\vartheta)$.

What the result provides

The theorem shows that an accurate numerical answer to the expected-recourse question contains an exact combinatorial count. This explains why a routine second-stage linear optimization problem can lead to a difficult expectation problem: the expectation records the volume of a polytope whose geometry encodes all linear extensions. The page's threshold specifies precisely how much accuracy is needed to recover the count; a coarser estimate does not support the same rounding conclusion. The original paper also explains why its instance yields strong #P-hardness: the coefficients needed for its random-recourse representation are only $-1$, $0$, and $1$ in the continuation of Theorem 3's proof.

Formalizing the reduction's mathematical claims produces reusable interfaces for order-polytopes, their volumes, and the expectation of this recourse program. It also poses the factorial volume identity as a theorem rather than treating it as a free assumption. The published Prove2Me definition FCP.Order.LinearExtensions already represents the same linear-extension object and is reused here. The five theorem statements in this proposal are open proof obligations; the existence of the published definition is not a claim that these results already have machine-checked proofs. Proofs of the pointwise value, the expectation identity, the volume identity, and the rounding consequences are welcome.

Where the difficulty lies

For a fixed realization, the program's $y_{ij}$ variables have no upper bounds. That feature makes its value jump between zero and one according to whether the order inequalities hold. The pointwise characterization does not by itself settle the expectation: the set where the value changes must be represented measurably, and the integral is over the unit cube with its normalized mass. The factorial relation is a separate geometric statement about the order polytope. Simply counting its defining inequalities gives neither its volume nor the number of linear extensions. These are the substantive steps behind the short rounding calculation.

Formalization scope and conventions

Lean uses a finite type with a PartialOrder in place of the paper's labeled set $S=\{1,\ldots,k\}$. The published FCP.Order.LinearExtensions definition counts order-preserving bijections from this type to the positions $0,\ldots,k-1$. It has exactly the paper's meaning of a compatible permutation. The cube and order polytope are sets of real-valued functions on that finite type. Volume is volume converted to a real number; expected recourse is the Lebesgue integral over the cube. The cube has mass one, including when $P$ is empty, and the results include that edge case.

The reusable cube, order polytope, volume, and linear-extension count form a separate definition module. The paper's second-stage program imports that module and defines only its own feasible levels, optimal value, and expected recourse.

The second-stage program is encoded through its feasible objective levels and their real supremum. Since zero is feasible and every feasible level is at most one, the supremum cannot use Lean's default value for an empty or unbounded real set. Classical decidability selects the comparable pairs in the finite sum. Accuracy means an absolute-error inequality with a nonnegative $\varepsilon$ and a strict threshold $\varepsilon<1/(2k!)$. These choices preserve both the page's feasibility and its rounding margin.

The main goal is the correctness of the reduction in Theorem 3. It does not formalize #P, strong #P-hardness, pseudo-polynomial running time, unary encodings, or bit lengths. A formulation that assumes $Q(P)=1-V(P)$ or $N(P)=k!V(P)$ in the goal would erase the result's content; those are separate milestone theorems. Reusable work includes the finite-order volume identity and measure-theoretic handling of the indicator on the cube. The preprint's Section 3 supplies every object and convention used here.

Selected references

• G. A. Hanasusanto, D. Kuhn, and W. Wiesemann, A comment on “computational complexity of stochastic programming problems”, Optimization Online preprint 2015/03/4825, version of October 6, 2015, pp. 10–12. Preprint.
• G. Brightwell and P. Winkler, Counting linear extensions, Order 8(3), 225–242, 1991. DOI.

Motivation

A matrix $A \in \mathbb C^{n\times n}$ is singular exactly when the pair of linear systems $\mathbf x^\top A = 0$, $A\mathbf y = 0$ has a solution with both $\mathbf x$ and $\mathbf y$ nonzero, and this is decided in polynomial time by Gaussian elimination. The natural analogue for a 3-tensor replaces the two linear systems by three families of bilinear equations, one for each way of contracting the tensor against two vectors. For tensors whose dimensions satisfy the Gelfand–Kapranov–Zelevinsky condition, solvability of that system is equivalent to the vanishing of the hyperdeterminant, and for any tensor it is equivalent to $0$ being a singular value in the sense of Lim (2005). The same system appears in multiview geometry (Cohen and Tomasi 1997).

C. J. Hillar and L.-H. Lim, Most Tensor Problems Are NP-Hard (J. ACM 60(6), 2013; arXiv:0911.1393), show that, unlike the matrix case, this feasibility question is NP-hard over $\mathbb R$ and over $\mathbb C$ (their Theorem 3.7). The proof is a reduction from graph 3-colorability through the polynomial color encoding of a graph, an idea the authors trace to Bayer's thesis (1982) and to Lovász (1994) and De Loera (1995). This mission formalizes that reduction and its consequence for tensor singular values (Theorem 6.2).

Setting

A 3-tensor over a field $F$ is an array $\mathcal A = [\![a_{ijk}]\!] \in F^{l\times m\times n}$. Its slices are the matrices $A_i(j,k) = B_j(i,k) = C_k(i,j) = a_{ijk}$, all read off the same array.

Tensor bilinear feasibility (Problem 3.1) asks, for a rational tensor $\mathcal A \in \mathbb Q^{l\times m\times n}$ and $F = \mathbb R$ or $\mathbb C$, whether the system (9)

$$\mathbf v^\top A_i\mathbf w = 0\ (i \le l),\qquad \mathbf u^\top B_j \mathbf w = 0\ (j \le m),\qquad \mathbf u^\top C_k \mathbf v = 0\ (k \le n)$$

has a solution $\mathbf u \in F^l$, $\mathbf v\in F^m$, $\mathbf w \in F^n$ with each of the three vectors nonzero. In Lean this is TBF A.

The color encoding $C_G$ of a graph $G = (V,E)$ on $v$ vertices (Definition 2.9) is the set of $4v$ quadratics in $x_1,\dots,x_v,y_1,\dots,y_v,z$:

$$x_iy_i - z^2,\quad y_iz - x_i^2,\quad x_iz - y_i^2,\quad \sum_{j:\{i,j\}\in E}(x_i^2 + x_ix_j + x_j^2),\qquad i = 1,\dots,v .$$

The tensor $\mathcal A_G \in \mathbb Z^{l\times m\times n}$ of the proof of Theorem 3.7 has $m = n = 2v+1$ and $l = v(2v+5)$ slices: $v(2v+1)$ slices whose bilinear forms are the $2\times 2$ minors of the matrix $[\mathbf v\ \mathbf w]$, then $3v + v$ slices whose bilinear forms restrict, on $\mathbf w = \mathbf v$, to the polynomials of $C_G$ (Lean: AG G).

The tensor $\mathcal B$ of Lemma 3.6 doubles a real tensor $\mathcal A$ into $\mathbb R^{2l\times 2m\times 2n}$ through the slices $B_i = \left[\begin{smallmatrix} A_i & 0 \\ 0 & -A_i\end{smallmatrix}\right]$, $B_{l+i} = \left[\begin{smallmatrix} 0 & A_i \\ A_i & 0\end{smallmatrix}\right]$ (Lean: doubling A).

An $\ell^2$-singular value $\sigma$ of $\mathcal A$ (Definition 6.1) admits nonzero $\mathbf u,\mathbf v,\mathbf w$ with $\sum_{j,k}a_{ijk}v_jw_k = \sigma u_i$ and the two analogous equations; an $\ell^3$-singular value has $\sigma u_i^2$, $\sigma v_j^2$, $\sigma w_k^2$ on the right. At $\sigma = 0$ both reduce to (9).

Formalization targets

Goal: Theorem 3.7

$$\textsf{3-COLORABILITY} \le_p \textsf{TBF}_{\mathbb R} \quad\text{and}\quad \textsf{3-COLORABILITY} \le_p \textsf{TBF}_{\mathbb C},$$

polynomial-time many-one reductions between languages of binary codes. NP-hardness of tensor bilinear feasibility then follows from the NP-completeness of 3-colorability (Karp 1972), which is cited and not part of the statement.

Milestones, in the order the proof uses them

1. Lemma 2.10. $C_G$ has a nonzero complex zero iff $G$ is 3-colorable.
2. The minors (proof of Theorem 3.7). For nonzero $\mathbf v, \mathbf w \in \mathbb C^N$, all $2\times2$ minors of $[\mathbf v\ \mathbf w]$ vanish iff $\mathbf v = c\mathbf w$ for some $c \in \mathbb C$.
3. Correctness over $\mathbb C$ (proof of Theorem 3.7). For $v \ge 1$, $\mathrm{TBF}_{\mathbb C}(\mathcal A_G) \iff G$ is 3-colorable.
4. Lemma 3.6. $\mathrm{TBF}_{\mathbb R}(\mathcal B) \iff \mathrm{TBF}_{\mathbb C}(\mathcal A)$ for real $\mathcal A$.
5. Theorem 6.2 (further result). 3-colorability reduces to deciding whether $0$ is an $\ell^2$-singular value, and whether it is an $\ell^3$-singular value, over $\mathbb R$ and over $\mathbb C$.

Significance

Theorem 3.7 is the hub of the paper's bilinear results: Section 6 derives from it the NP-hardness of deciding whether $0$ is a tensor singular value (Theorem 6.2), and the triple bilinear problem (Theorem 3.8) is handled by the same techniques. It separates tensors from matrices in a precise sense: the matrix analogue of (9) is decided by a determinant, while the tensor version encodes a classical NP-complete problem. It does not settle the hardness of the hyperdeterminant, since the dimensions $l = v(2v+5)$, $m = n = 2v+1$ of $\mathcal A_G$ violate the GKZ condition; the paper leaves that as a conjecture.

The result is proved in the paper; none of it is formalized on Prove2Me or, to our knowledge, elsewhere. A complete development produces a machine-checked polynomial-time reduction in Cook's Turing-machine model between two concrete algebraic problems, the color-encoding lemma for 3-colorability (reusable by any reduction that goes through polynomial systems, including Theorems 1.3 and 2.6 of the same paper), and the realification of bilinear systems.

Difficulty

The algebra of the reduction is short; two places need care. First, the bilinear system does not see $C_G$ directly: (9) involves two independent vectors $\mathbf v, \mathbf w$, and the reduction recovers the quadratic system only because the minors force $\mathbf v = c\mathbf w$, which requires both vectors to be nonzero. Second, the converse direction must produce a nonzero $\mathbf u$ satisfying the second and third families, a homogeneous linear system of $4v+2$ equations in $l = v(2v+5)$ unknowns; this works only when $l > 4v+2$, which fails for the empty graph, so the reduction has to treat $v = 0$ separately.

The goal also asks for polynomial-time computability in a Turing-machine model: decoding a graph code, rejecting malformed words, and writing the binary code of $\mathcal A_G$ (or of its doubling over $\mathbb R$). This bookkeeping, not the algebra, is the bulk of a complete proof.

Formalization scope

• Tensors are functions I → J → K → F over finite index types, 0-based: the paper's $a_{ijk}$ is A (i-1) (j-1) (k-1). Problem 3.1 requires $\mathbf u$, $\mathbf v$, $\mathbf w$ each nonzero, not merely $(\mathbf u, \mathbf v, \mathbf w) \neq 0$, and the three equation families come from one tensor.
• The doubled tensor of Lemma 3.6 is indexed by I ⊕ I, J ⊕ J, K ⊕ K, with Sum.inr i standing for the paper's index $l+i$. Lemma 3.6 is stated for this explicit $\mathcal B$; a bare existential would be witnessed by any tensor with the right truth value. Only the equivalence of existence is stated, not the paper's "one-to-one" correspondence (which pairs $\mathbf u' = (\mathbf p,\mathbf q)$ with the conjugate-type vector $\mathbf p - i\mathbf q$).
• The paper does not print the matrices of the last $4v$ slices of $\mathcal A_G$. The mission fixes the bilinearizations $x_i\hat y_i - z\hat z$, $y_i\hat z - x_i\hat x_i$, $x_i\hat z - y_i\hat y_i$ and $\sum_{j\sim i}(x_i\hat x_i + x_i\hat x_j + x_j\hat x_j)$; each restricts to the printed polynomial on $\mathbf w = \mathbf v$.
• "Nontrivial zero" in the minors claim is read as both $\mathbf v$ and $\mathbf w$ nonzero; the correctness milestone over $\mathbb C$ assumes $v \geq 1$, since for $v = 0$ the printed tensor has no slices and its system (9) is infeasible.
• "Polynomially reducible" is formalized as Cook–Karp many-one reducibility (CookPvsNP.PolyReducible), which the paper's proof constructs and which implies the paper's oracle notion of §1.4. "NP-hard" in Theorem 6.2 is rendered the same way, and "($\ell^2$ or $\ell^3$)" as the claim for each notion. Rational inputs are coded as numerator and denominator in binary; tensors as $l, m, n$ and then their entries in lexicographic order.
• The singular-value equations (20)–(21) are taken literally over $\mathbb C$, without conjugates and without normalization; only $\sigma = 0$ is used, where they are scale-free.
• NP-completeness of 3-colorability is cited, not formalized; no statement mentions P, NP-membership, or hyperdeterminants.
• A trivializing formalization is ruled out: the goal is the polynomial-time reduction, not the bare equivalence of yes-instances, and the reduction must handle every input word.

The mission reuses the published definitions CookPvsNP_defs (Turing machines, polynomial-time computability, many-one reducibility) and ProjSchedTW.Complexity.Encoding (the binary alphabet and number codes), and Mathlib's SimpleGraph.Colorable. Contributions welcome: the algebraic milestones (Lemma 2.10, the minors, Lemma 3.6) are independent and self-contained; a library of polynomial-time computable list and arithmetic operations on BSym codes would serve both this goal and Theorem 6.2.

Selected references

• C. J. Hillar, L.-H. Lim, Most Tensor Problems Are NP-Hard, J. ACM 60(6), Art. 45, 2013. https://doi.org/10.1145/2512329 (arXiv:0911.1393v5, https://arxiv.org/abs/0911.1393)
• R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 1972. https://doi.org/10.1007/978-1-4684-2001-2_9
• L.-H. Lim, Singular values and eigenvalues of tensors: a variational approach, Proc. IEEE CAMSAP, 2005. https://arxiv.org/abs/math/0607648
• I. M. Gelfand, M. M. Kapranov, A. V. Zelevinsky, Discriminants, Resultants, and Multidimensional Determinants, Birkhäuser, 1994. https://doi.org/10.1007/978-0-8176-4771-1
• S. A. Cook, The P versus NP problem, Clay Mathematics Institute problem description, 2000. https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf

Motivation

Eigenvalues of matrices are computable in polynomial time to any accuracy, and numerical linear algebra rests on that fact. Higher-order tensors appear in statistics (moment and cumulant tensors), signal processing, quantum information and polynomial optimization, and several notions of tensor eigenvalue were proposed for them, independently by Lim and by Qi in 2005 (Lim 2005; Qi 2005). Hillar and Lim (J. ACM 60(6), 2013, Art. 45; arXiv:0911.1393) showed that most of the natural tensor analogues of tractable matrix problems are NP-hard. Their first example, Theorem 1.3, concerns the simplest one: deciding whether a given number is an eigenvalue of a 3-tensor.

This mission formalizes that theorem together with the lemmas its proof uses. The reduction starts from graph 3-colorability, and its intermediate step, quadratic feasibility (Theorem 2.6), is reused throughout the paper: the bilinear, singular value and triple-bilinear results all go through the same color encoding.

Setting

A 3-tensor over a field $F$ is an array $\mathcal A=[\![a_{ijk}]\!]\in F^{n\times n\times n}$. A scalar $\lambda\in F$ is an eigenvalue of $\mathcal A$ (eq. (3) of the paper) if there is a nonzero $\mathbf x\in F^n$ with

$$\sum_{i,j=1}^{n}a_{ijk}\,x_ix_j=\lambda x_k,\qquad k=1,\dots,n.$$

The sum is over the first two indices. For $\lambda=0$ the condition is invariant under scaling of $\mathbf x$, so no normalization enters.

Problem 1.2 (tensor $\lambda$-eigenvalue) fixes $F\in\{\mathbb R,\mathbb C\}$ and $\lambda\in\mathbb Q$, and asks, for a rational tensor $\mathcal A\in\mathbb Q^{n\times n\times n}$, whether $\lambda$ is an eigenvalue of $\mathcal A$ with an eigenvector in $F^n$.

Problem 2.2 (quadratic feasibility) asks, for rational matrices $A_1,\dots,A_m\in\mathbb Q^{n\times n}$, whether the system $\mathbf x^\top A_i\mathbf x=0$ ($i=1,\dots,m$) has a nonzero solution $\mathbf x\in F^n$.

A proper 3-coloring of a simple graph $G=(V,E)$ assigns one of three colors to each vertex so that adjacent vertices receive different colors.

The color encoding $C_G$ of a graph on vertices $1,\dots,v$ (Definition 2.9) is the family of $4v$ quadratics in $x_1,\dots,x_v,y_1,\dots,y_v,z$:

$$x_iy_i-z^2,\quad y_iz-x_i^2,\quad x_iz-y_i^2,\quad \sum_{j:\{i,j\}\in E}(x_i^2+x_ix_j+x_j^2),\qquad i=1,\dots,v.$$

Lemma 2.7 replaces a complex quadratic system by a real one of twice the size, and Lemma 2.8 pads a real system to a square one. Applied to $C_G$, they give $N$ real quadratics $\mathbf x^\top B_k\mathbf x$ in $N$ unknowns. The tensor $T_G$ with $a_{ijk}=(B_k)_{ij}$ is the output of the reduction.

Formalization targets

Goal: Theorem 1.3

$$\textsf{3-COL}\ \le_p\ \textsf{TENSOR-0-EIG}_{\mathbb R}.$$

Graph 3-colorability is polynomial-time many-one reducible to the language of binary codes of rational tensors having $0$ as a real eigenvalue.

Milestones, in the order the proof uses them

1. Lemma 2.10. $C_G$ has a nonzero complex solution if and only if $G$ is 3-colorable.
2. Lemma 2.7. The $2m$ real equations with matrices $\begin{bmatrix}A_i&0\\0&-A_i\end{bmatrix}$ and $\begin{bmatrix}0&A_i\\A_i&0\end{bmatrix}$ have a nonzero real solution iff $\{\mathbf z^\top A_i\mathbf z=0\}$ has a nonzero complex solution.
3. Lemma 2.8. Padding to $r\ge m+1$ equations in $s\ge n$ unknowns preserves real feasibility.
4. Theorem 2.6. $\textsf{3-COL}\le_p$ quadratic feasibility over $\mathbb R$ and over $\mathbb C$.
5. Proof of Theorem 1.3, first step. $0$ is a real eigenvalue of $\mathcal A$ iff the square system $\mathbf x^\top A_k\mathbf x=0$, $A_k(i,j)=a_{ijk}$, has a nonzero real solution.
6. Proof of Theorem 1.3, the construction. $G$ is 3-colorable iff $0$ is a real eigenvalue of $T_G$.

Significance

The result. Theorem 1.3 shows that deciding whether $0$ is an eigenvalue of a rational 3-tensor over $\mathbb R$ is NP-hard, in contrast to the matrix case. Because the instance is a single rational tensor with small integer entries, the hardness does not come from numerical precision: it is a property of the exact problem. The same encoding underlies the paper's hardness of approximating an eigenvector (Theorem 1.5) and its remarks on counting eigenvectors (Corollary 1.16).

Formalizing it. The result is proved in the paper, but no part of it is machine-checked. The mission adds three things. It gives a precise language-level statement of what "polynomially reducible" means for this problem. It gives a checked equivalence between 3-colorability and the eigenvalue condition for the explicit tensor $T_G$. And it gives reusable statements about homogeneous quadratic systems (realification and padding), which the bilinear and singular value missions of this series also need.

Difficulty

The algebraic core is Lemma 2.10, and its reverse direction is where a first attempt fails. The fourth family of $C_G$ does not say that each term $x_i^2+x_ix_j+x_j^2$ vanishes; it says only that their sum over the neighbours of $i$ vanishes, over $\mathbb C$, where nonzero terms can cancel. A common zero yields a coloring only after the first three families have pinned down each coordinate, and the case $z=0$ must be excluded separately.

Lemma 2.7 needs care because the matrices $A_i$ are not assumed symmetric: the imaginary part of $\mathbf z^\top A\mathbf z$ is $\mathbf u^\top A\mathbf v+\mathbf v^\top A\mathbf u$, not $2\mathbf u^\top A\mathbf v$. Lemma 2.8 uses that $\mathbb R$ is formally real; it fails over $\mathbb C$.

At the language level, the reduction must be exhibited as a Turing machine computation on binary codes in polynomial time. That is bookkeeping, but it is the part the paper does not write down.

Formalization scope

• Tensors and vectors. Tensors are arrays Fin n → Fin n → Fin n → F, vectors Fin n → F, and indices are 0-based. The eigenvalue condition is eq. (3) verbatim, without normalization; for $\lambda=0$ none is needed. Rational data are cast into $\mathbb R$ or $\mathbb C$.
• Quadratic polynomials. A homogeneous quadratic is a (not necessarily symmetric) rational matrix $M$, read as $\mathbf x^\top M\mathbf x$, and the monomial $x_ax_b$ is the matrix unit $E_{ab}$. A vertex without neighbours contributes the zero polynomial to $C_G$.
• Choices in the construction. The square size is $N=8v+2$. It meets Lemma 2.8's bounds $r\ge 8v+1$ and $s\ge 4v+2$ for every $v\ge 0$; Example 1.4's count differs and is not used.
• Reducibility. "Polynomially reducible" is Cook's polynomial-time many-one reducibility (CookPvsNP.PolyReducible, published definition CookPvsNP_defs). The paper's reduction maps one graph to one tensor, and a many-one reduction implies the oracle notion of its §1.4.
• Binary codes. Instances are coded over the alphabet BSym with the binary codes of the published definition ProjSchedTW.Complexity.Encoding. A graph is $\nu$ followed by its adjacency matrix. A rational is its numerator then its denominator. A tensor is $n$ followed by its entries in lexicographic order. The target language contains all rational tensors, not only integral ones.
• Not formalized. NP-completeness of 3-colorability (Karp 1972) is cited, not formalized, and the goal states only the reduction. Approximation (Theorem 1.5), counting (Corollary 1.16) and the solution count of Example 1.4 are out of scope.
• Trivializations ruled out. Every feasibility statement requires a nonzero solution, since the zero vector solves every homogeneous system. The goal includes polynomial-time computability of the reduction, not just the existence of an equivalence-preserving map, which would be trivial. The milestones concern the paper's explicit $C_G$ and $T_G$, not an arbitrary tensor.

Contributions are welcome in four places:

• proofs of the milestones;
• a polynomial-time Turing machine computing $G\mapsto T_G$ on codes;
• general lemmas on homogeneous quadratic systems over formally real fields;
• a composition (transitivity) lemma for CookPvsNP.PolyReducible.

Selected references

• C. J. Hillar and L.-H. Lim, Most Tensor Problems Are NP-Hard, Journal of the ACM 60(6), Article 45, 2013. https://doi.org/10.1145/2512329 (arXiv:0911.1393v5, https://arxiv.org/abs/0911.1393)
• L.-H. Lim, Singular values and eigenvalues of tensors: a variational approach, Proc. IEEE CAMSAP 2005, pp. 129–132. https://doi.org/10.1109/CAMAP.2005.1574201
• L. Qi, Eigenvalues of a real supersymmetric tensor, Journal of Symbolic Computation 40(6), 2005, pp. 1302–1324. https://doi.org/10.1016/j.jsc.2005.05.007
• R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 1972, pp. 85–103. https://doi.org/10.1007/978-1-4684-2001-2_9
• S. Cook, The P versus NP problem, Clay Mathematics Institute Millennium Problem description, 2000. https://www.claymath.org/millennium/p-vs-np/

Motivation

MAX-CUT asks for a partition of the vertices of a graph that cuts as many edges, or as much edge weight, as possible. It is one of Karp's original NP-hard problems and the standard test case for approximation algorithms. A uniformly random partition cuts half of the edges in expectation. Goemans and Williamson (JACM 1995) rounded a semidefinite relaxation with a random hyperplane and obtained the ratio

$$\alpha_{GW}=\min_{0<\theta<\pi}\frac{\theta/\pi}{(1-\cos\theta)/2}\approx 0.878567.$$

Whether a better ratio can be achieved in polynomial time was a central open question.

Timeline.

• 1995: Goemans and Williamson give the $\alpha_{GW}$-approximation.
• 2001: Håstad (JACM 2001) shows, via PCPs and gadgets, that approximating MAX-CUT within $16/17+\epsilon\approx 0.941$ is NP-hard. This remains the best unconditional bound.
• 2002: Khot (STOC 2002) formulates the Unique Games Conjecture (UGC).
• 2004–2007: Khot, Kindler, Mossel and O'Donnell (SIAM J. Comput. 2007) show that the UGC implies that $\alpha_{GW}$ is optimal. Their reduction rests on the Majority Is Stablest conjecture, which they formulate.
• 2005–2010: Mossel, O'Donnell and Oleszkiewicz (Annals of Math. 2010, arXiv:math/0503503) prove Majority Is Stablest via the invariance principle.

Setting

A Unique Label Cover instance $\mathcal L(V,W,E,[M],\{\sigma_{v,w}\})$ is a bipartite graph with left vertices $V$, right vertices $W$ and edges $E\subseteq V\times W$, together with a bijection $\sigma_{v,w}:[M]\to[M]$ on each edge. A labeling assigns a label in $[M]$ to every vertex, and it satisfies $(v,w)$ if $\sigma_{v,w}(\mathrm{label}(w))=\mathrm{label}(v)$. $\mathrm{OPT}$ is the largest fraction of edges satisfied by a labeling. The Unique Games Conjecture says that for all $\eta,\gamma>0$ there is $M=M(\eta,\gamma)$ such that it is NP-hard to distinguish instances with label set $[M]$ and $\mathrm{OPT}\ge 1-\eta$ from those with $\mathrm{OPT}\le\gamma$.

A weighted MAX-CUT instance is a graph with nonnegative edge weights. It is at least $c$-satisfiable if some partition cuts at least a $c$ fraction of the total weight, and at most $s$-satisfiable if no partition cuts more than an $s$ fraction.

On the cube $\{-1,1\}^n$, with TRUE $=-1$ and the uniform measure, the noise stability of $f:\{-1,1\}^n\to\mathbb R$ at $\rho\in[-1,1]$ is $\mathbb S_\rho(f)=\mathbf E[f(x)f(y)]$. Here $x$ is uniform and $y$ is $\rho$-correlated with $x$: each $y_i$ independently equals $x_i$ with probability $\tfrac12+\tfrac12\rho$. The influence $\mathrm{Inf}_i(f)$ is the expected variance of $f$ in the coordinate $x_i$, and the low-degree influence is $\mathrm{Inf}_i^{\le k}(f)=\sum_{S\ni i,|S|\le k}\hat f(S)^2$. Majority Is Stablest states: for $\rho\in[0,1)$ and $\epsilon>0$ there is $\delta>0$ such that every $f:\{-1,1\}^n\to[-1,1]$ with $\mathbf E[f]=0$ and all $\mathrm{Inf}_i(f)\le\delta$ has $\mathbb S_\rho(f)\le 1-\tfrac2\pi\arccos\rho+\epsilon$.

Formalization targets

Goal: Theorem 1 (p. 11)

Assume the UGC and Majority Is Stablest. For every $-1<\rho<0$ and $\epsilon>0$ it is NP-hard to distinguish MAX-CUT instances that are at least $c$-satisfiable from those that are at most $s$-satisfiable, where

$$c=\tfrac12-\tfrac12\rho,\qquad s=\frac{\arccos\rho}{\pi}+\epsilon.$$

Choosing $\rho$ to minimize $s/c$ gives hardness of approximation within any factor above $\alpha_{GW}$; that consequence is not part of the goal.

Milestones

• The Fourier formulas $\mathbb S_\rho(f)=\langle f,T_\rho f\rangle=\sum_S\rho^{|S|}\hat f(S)^2$ (Proposition 7.1) and $\mathrm{Inf}_i(f)=\sum_{S\ni i}\hat f(S)^2$ (Proposition 7.2).
• Three variants of Majority Is Stablest:
  • with low-degree influences (Proposition 7.3);
  • in reverse for $\rho\in(-1,0]$, without $\mathbf E[f]=0$ (Proposition 7.4);
  • both at once (Proposition 7.5).
• The completeness of the Long-Code verifier, $(1-2\eta)(\tfrac12-\tfrac12\rho)$ (§8.2).
• The arithmetization $\Pr[\mathrm{acc}]=\tfrac12-\tfrac12\mathbf E_v[\mathbb S_\rho(g_v)]$ (6).
• The influence-transfer inequality (7).
• The candidate-set bound $|\mathrm{Cand}[w]|\le 2k/\delta$.
• The soundness: acceptance $\ge(\arccos\rho)/\pi+\epsilon$ forces $\mathrm{OPT}\ge\gamma'(\epsilon,\rho)$, independently of $M$ (§8.3).

Significance

Under the UGC, Theorem 1 shows that the Goemans–Williamson algorithm is optimal for MAX-CUT. It also shows that the semidefinite relaxation's integrality gap and the hardness threshold coincide. This correspondence was later extended to every constraint satisfaction problem (Raghavendra, STOC 2008). The verifier analysis here is the template for many later UGC-hardness results: dictatorship tests via noise stability, and list-decoding via low-degree influences.

The paper's result is proved, conditional on the UGC; the UGC itself is open. To our knowledge, neither the reduction nor the Majority Is Stablest theorem has a machine-checked proof. This mission produces a checked version of the conditional reduction. Its by-products are reusable: Fourier analysis on the cube (noise stability, influences, the Bonami–Beckner operator), the Long-Code verifier analysis, and a gap-hardness interface on top of a Turing-machine definition of NP.

Difficulty

Completeness is a short calculation. The difficulty is soundness. A proof that the verifier accepts with probability above $(\arccos\rho)/\pi+\epsilon$ must be decoded into a labeling that satisfies a fraction $\gamma'$ of the edges, and $\gamma'$ must not depend on the label set size $M$. Labeling each $w$ by a coordinate of large influence of $f_w$ is the obvious decoding, but on its own it does not work. The test is passed with high probability by the averaged functions $g_v$, not by the $f_w$ themselves. Ruling out functions with only small influences is exactly the content of Majority Is Stablest. The analysis needs both the reverse form of Majority Is Stablest for negative $\rho$ and low-degree influences, whose sum is bounded by $k$ independently of $M$. Turning the PCP into polynomial-time gap-hardness adds further work on top of the analysis:

• the regularity assumption must be removed;
• an irrational $\rho$ must be replaced by a nearby rational one, so that the weights are integers;
• the reduction must be shown polynomial-time on Turing machines.

Formalization scope

• The cube. $\{-1,1\}^n$ is Fin n → Bool, with TRUE $\mapsto-1$. Expectations are finite averages.
• No Fourier shortcuts. Noise stability and influence are defined as on pp. 5–6 (a correlated-pair average, an expected coordinate variance), not by their Fourier formulas, which are milestones.
• Unique Label Cover. Instances have finite $V,W$, $E\subseteq V\times W$, and a permutation of $\mathrm{Fin}\,M$ for every pair. $\mathrm{OPT}$ is the maximum over the finitely many labelings, and $0$ when there is none.
• MAX-CUT instances are loopless graphs with natural-number edge weights (edge multiplicities), as §7.1 permits.
• NP-hardness. "NP-hard to distinguish" is GapNPHard: every NP language of the published CookPvsNP_defs maps by a polynomial-time Turing-machine computable function to Yes-instances or No-instances. Instances are encoded in unary.
• Hypotheses of the goal. The UGC is a hypothesis of Theorem 1. Majority Is Stablest, which the paper cites from [45] and does not prove, is a second, disclosed hypothesis, of Theorem 1 and of every milestone that uses it.
• Regularity. The verifier milestones assume the $V$-side regularity of §8.1; Theorem 1 and the UGC do not.
• No trivial instances. Every Yes- and No-predicate requires a nonempty edge set, so the empty instance cannot carry the hardness. Placeholder (True/False) versions of the UGC or of Majority Is Stablest would trivialize the goal and are excluded.
• Welcome contributions.
  • The Fourier milestones are self-contained and reusable.
  • A proof of Majority Is Stablest would discharge the second hypothesis.
  • A formal regularization of Unique Label Cover ([38]) would make the reduction self-contained.

Selected references

• S. Khot, G. Kindler, E. Mossel, R. O'Donnell, Optimal Inapproximability Results for MAX-CUT and Other 2-Variable CSPs?, SIAM J. Comput. 37(1), 2007. https://doi.org/10.1137/S0097539705447372
• M. X. Goemans, D. P. Williamson, Improved approximation algorithms for maximum cut and satisfiability problems using semidefinite programming, J. ACM 42(6), 1995. https://doi.org/10.1145/227683.227684
• J. Håstad, Some optimal inapproximability results, J. ACM 48(4), 2001. https://doi.org/10.1145/502090.502098
• S. Khot, On the power of unique 2-prover 1-round games, STOC 2002. https://doi.org/10.1145/509907.510017
• E. Mossel, R. O'Donnell, K. Oleszkiewicz, Noise stability of functions with low influences: invariance and optimality, Annals of Math. 171(1), 2010. https://doi.org/10.4007/annals.2010.171.295 (arXiv:math/0503503)

Motivation

Bounded-error factoring and exact factoring have different correctness requirements. Repetition until success and increasingly accurate rotations do not automatically give a fixed-gate, worst-case polynomial exact algorithm. The pinned manuscript supplies the research context.

Setting

Circuit instructions use NOT, CNOT, Toffoli, Hadamard and phase primitives, their inverses and singly controlled versions. A classical finite-stack machine generates each encoded circuit from unary input length.

Formalization target

The selected goal is OAI.ExactQuantumFactoring.exact_quantum_factoring. Its central assertion is

$$P(\mathrm{complete\ prime\ factorization\ of}\ N)=1.$$

The theorem states that the defined proposition MainTheorem holds, i.e. there is a family of quantum circuits indexed by input bit length ℓ with three properties. Circuits are lists of instructions on q qubits, each applying one of 20 named gates (the primitives NOT, CNOT, Toffoli, Hadamard and phase, each optionally inverted and optionally given one extra control) to distinct wires; the output state is obtained by applying the instructions in order to the basis state holding the binary digits of N, least significant bit first, on the first ℓ wires, with all other wires zero. First, the family is uniform: a single Turing machine (TM2) with finite stack alphabets computes in polynomial time the encoding of the ℓth circuit from the unary string of length ℓ, where the encoding writes the qubit count, instruction count and each instruction's gate code, inverse and control flags and wire indices in unary. Second, the numbers of qubits and of instructions of the ℓth circuit are both bounded by one fixed polynomial in ℓ with natural-number coefficients. Third, for every ℓ and every integer N ≥ 2 whose binary length is exactly ℓ, the circuit has at least ℓ + n² qubits, where n = max(128, ℓ), and the total squared amplitude on basis states whose output is correct equals exactly 1. A basis state is correct if reading n consecutive blocks of n bits after the input wires, each block as a binary number, gives the nondecreasing list of prime factors of N with multiplicity, padded with zeros to length n.

Significance and status

The output is a sorted list of prime factors with multiplicity in fixed binary blocks, padded with zeros. The target is an existence theorem for a uniform circuit family, not an uploaded executable factoring program. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.

Difficulty

Uniform generation, polynomial qubit and gate bounds, a fixed finite gate alphabet, and probability-one correctness must all hold together.

Formalization scope

The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.

The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.

Selected references

• OpenAI, Exact quantum factoring over a fixed finite gate set, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.