Complexity Theory

Motivation

Schönhage and Strassen conjectured in 1971 that $n\log n$ is the optimal order of growth for multiplying two $n$-bit integers on a multitape Turing machine. Harvey and van der Hoeven proved the matching upper bound $O(n\log n)$ (Annals of Mathematics, 2021). In September 2026, a preprint by OpenAI, Integer multiplication below $n\log n$, claimed that this bound can itself be beaten by a power of the logarithm, in the same model. If correct, the upper half of the conjecture's "$\Theta(n\log n)$" is false. Two independent follow-up projects then increased the exponent saving $\kappa$ by many orders of magnitude. This mission targets the strongest claimed saving and takes the earlier claims as milestones.

Timeline (multitape Turing model; all bounds are of the form $O(n(\lg n)^{1-\kappa})$).

• 2021: Harvey and van der Hoeven, $\kappa=0$, that is, $O(n\log n)$. Published and refereed.
• 23 September 2026: OpenAI preprint, $\kappa=2^{-182}$ (Theorem 1 of the preprint). The preprint has not been refereed.
• October 2026: D. Colkitt, integer-mult-bounds, a series of patches to the OpenAI manuscript with checked numerical certificates, reaching $\kappa=2^{-30}$. The project describes this as conditional on the OpenAI manuscript and as having had no independent review.
• October 2026: S. Jain, integer-mult-kappa, building on both, reaching $\kappa=3666565558019/10^{17}\approx3.67\times10^{-5}>2^{-15}$ ("round six"). It is also stated to be conditional and unreviewed. Its numerical certificate is checked by computation in the Lean kernel, but the analytic facts behind that certificate are taken as premises.

Setting

A $k$-tape Turing machine, in the conventions of Montanaro's Computational Complexity lecture notes (§3, §3.4), has the following parts:

• a finite alphabet containing a blank $\square$ and a start symbol $\triangleright$;
• a finite set of states with a start state $\mathrm{START}$ and a distinct halting state $\mathrm{HALT}$;
• $k\ge2$ tapes: a read-only input tape, an output tape, and $k-2$ work tapes. Each tape is infinite in one direction, has its own head, and holds $\triangleright$ in its first cell and nowhere else.

In one step the machine reads the symbol under every head, writes a symbol under every head, moves each head by at most one cell (never left of $\triangleright$), and changes state. Once in $\mathrm{HALT}$ it stays there unchanged.

For $x\in\{0,1\}^n$ (most significant bit first), $\operatorname{val}(x)$ is the integer that $x$ represents, and $\operatorname{bin}_k(z)$ is the length-$k$ binary representation of $z$. A machine computes the product if, for every $n\ge1$ and all $x,y\in\{0,1\}^n$, when started on input $\triangleright\,x\#y$ it reaches $\mathrm{HALT}$ with the output tape holding exactly $\triangleright\,\operatorname{bin}_{2n}(\operatorname{val}(x)\operatorname{val}(y))$ followed by blanks. Its running time $T(n)$ is the largest number of steps on any pair of $n$-bit inputs. With $\lg n=\max(\lceil\log_2n\rceil,1)$, define

$$\mathrm{KappaBound}(\kappa)\iff \exists\,M\text{ computing the product with }T(n)=O\big(n(\lg n)^{1-\kappa}\big).$$

Formalization targets

Goal

$$\mathrm{KappaBound}\!\left(\tfrac{3666565558019}{10^{17}}\right).$$

Milestones: the earlier, weaker bounds

1. $\mathrm{KappaBound}(0)$: Harvey–van der Hoeven, Theorem 1.1. This is stated as a milestone of the companion mission, in the same machine model, and is referenced here.
2. $\mathrm{KappaBound}(2^{-182})$: OpenAI, Theorem 1.
3. $\mathrm{KappaBound}(2^{-30})$: Colkitt's ternary five-subset checkpoint.

Each milestone is implied by the goal, because $(\lg n)^{1-\kappa}$ decreases in $\kappa$. Each one is also a published claim in its own right and a natural intermediate formalization target. The $\kappa=0$ and $\kappa=2^{-182}$ constructions are the ones that the later claims rely on.

Significance

The result. Any $\kappa>0$ shows that $n\log n$ is not the optimal running time for multitape machines, which refutes the upper half of the Schönhage–Strassen conjecture as usually stated. The OpenAI preprint also derives the same bound for exact division and integer square roots (its Corollary 2). Larger values of $\kappa$ quantify how far below $n\log n$ multiplication can go. The bound is a statement about growth rates, and the constants involved are astronomically large.

Formalizing it. None of the three positive-$\kappa$ results has been refereed, and the two follow-ups explicitly depend on the OpenAI manuscript. Their written arguments, their computer-checked combinatorial certificates (rank sums, moment bounds, rational margins), and the full multiplication theorem have not been formally verified. Machine-checking any of the milestones would be the first independent confirmation of the corresponding claim. A formal disproof, or a formal identification of a gap, would be equally informative.

Difficulty

Fourier-based multiplication scans $\Theta(n)$ stored bits at each of $\Theta(\log n)$ transform levels, so any algorithm that performs those levels one at a time pays $\Theta(n\log n)$ for data movement and arithmetic alone. Beating this requires both moving data and carrying out butterfly layers at cost $o(V\log n)$ on a tape that is accessed sequentially, where $V$ is the stored volume. In the preprint this is done with recursive linear networks whose total number of smaller calls is strictly less than (number of roles) × (arity). The follow-ups improve $\kappa$ by finding better networks and tighter parameter choices, all certified by large exact computations. Each claim therefore combines a long analytic argument, a Turing-machine implementation, and a finite certificate, and all three must be formalized.

Formalization scope

• Machine model. The definitions are in IntMul_MultitapeModel, shared with the Harvey–van der Hoeven mission, and follow the $k$-tape conventions of Montanaro's lecture notes. Tapes begin with $\triangleright$. There is a $\mathrm{HALT}$ state that freezes the configuration. Tape $0$ is a read-only input tape holding $\triangleright\,x\#y$, and tape $1$ is the output tape, which must hold exactly $\triangleright$, then the product bits, then blanks. Running time is the number of steps until $\mathrm{HALT}$.
• The bound. As in the notes' definition of $O(\cdot)$: there are $c>0$ and $n_0$ with $T(n)\le c\,n(\lg n)^{1-\kappa}$ for $n\ge n_0$, and correctness is required for every $n\ge1$. Following the papers, $n$ is the length of each operand. The exponent $1-\kappa$ is a real power of a number that is at least $1$.
• No trivial solutions. A machine that fails to halt, or halts with a wrong output, on any well-formed input fails the definition. A proof must exhibit one fixed machine for all $n$.
• Infrastructure needed: Turing-machine composition with cost accounting; the Harvey–van der Hoeven reduction; the Nussbaumer synthetic transforms; the interchange and butterfly-layer networks of the preprint, with their rank and moment certificates; and the parameter assembly. The machine library and the certificate-checking infrastructure can be reused in other complexity missions.
• Welcome contributions: formal verification of the published certificates; formalization of the preprint's linear-network propositions; and machine-checked counterexamples to any step.

Selected references

• OpenAI, Integer multiplication below $n\log n$, preprint, 23 September 2026. https://github.com/openai/math/blob/main/preprints/Integer-multiplication-below-n-log-n-September-23-2026/paper.pdf
• D. Colkitt, A sharper exponent for integer multiplication (integer-mult-bounds), research draft, 2026. https://github.com/CrocSwap/integer-mult-bounds
• S. Jain, Integer multiplication: a conditional witness above $2^{-15}$ (integer-mult-kappa), research draft, 2026. https://github.com/Swapnil-jain/integer-mult-kappa
• D. Harvey, J. van der Hoeven, Integer multiplication in time $O(n\log n)$, Annals of Mathematics 193(2), 563–617, 2021. https://doi.org/10.4007/annals.2021.193.2.4
• A. Schönhage, V. Strassen, Schnelle Multiplikation großer Zahlen, Computing 7, 281–292, 1971. https://doi.org/10.1007/BF02242355
• H. J. Nussbaumer, Fast polynomial transform algorithms for digital convolution, IEEE Transactions on Acoustics, Speech, and Signal Processing 28(2), 205–215, 1980. https://doi.org/10.1109/TASSP.1980.1163372

Motivation

Multiplying two binary integers is a basic task in computational complexity. The relevant resource here is the number of individual steps made by a machine whose tapes can only be accessed through moving heads. Harvey and van der Hoeven established an $O(n\log n)$ bound in this model. The OpenAI manuscript proposes a positive saving in the exponent of the logarithm. Subsequent constructions explore larger savings. The formalization target is the complete computation and its time bound, including the analytic and implementation arguments needed to connect a finite construction to every input length.

Setting

A deterministic multitape Turing machine has a fixed finite alphabet, a fixed finite state set, and a fixed finite number of tapes. Each tape extends in one direction and has one head. A step reads the symbols under the heads, changes state, writes at those positions, and moves each head by at most one cell. The alphabet contains distinct blank, start-marker, zero, one, and separator symbols. Tape zero is the read-only input tape; tape one is the output tape; further tapes are available for work. The halting state freezes the configuration.

An input consists of two bit strings $x,y$ of the same positive length $n$, separated by $\#$. The strings are read most significant bit first, with leading zeros permitted. If $\operatorname{val}(x)$ denotes the represented natural number, the required output is exactly the $2n$-bit binary representation of $\operatorname{val}(x)\operatorname{val}(y)$, padded with leading zeros and followed by blanks. All tapes begin with a preserved start marker. Define $L(n)=\max(\lceil\log_2 n\rceil,1)$.

Target

The full target is

$$\mathrm{IntMul.KappaBound}(0.00012612978530233).$$

This asserts the existence of one machine that computes the exact product correctly for every positive input length, together with constants $c>0$ and $n_0$ such that every pair of $n$-bit inputs, for $n\ge n_0$ and $n\ge1$, halts within

$$c\,n\,L(n)^{1-0.00012612978530233}$$

steps. Constants, alphabet, states, and tape count are independent of the input length. The number is an exact real value. Larger $\kappa$ gives a stronger asymptotic saving because $L(n)\ge1$.

Each entry supplies its own exact numerical value and identifies the construction that motivates it. Historical and new entries use the same machine definition. A proposed value may be recorded while its complete proof is still open; it becomes a proved record only when the goal has a verified proof. Numerical certificates are supporting results with their own scope, and do not establish a complete machine time bound.

This entry: Jain, round eight

The value

$$\kappa=\frac{12612978530233}{10^{17}}=0.00012612978530233\;(>2^{-13})$$

is the headline conditional witness of S. Jain's integer-mult-kappa, round eight, at revision 5868dc7. It is bound by the complex side ($a_c=3945999/31250000000$).

• Bit side: the frozen round-seven witness (deferred readouts, $V$ leaves, lifted frames and late copies at $h=23$; Avi Eisenberg's producer from PR #62, compiled by eumemic's joint frame compiler), recompiled with opposite bank orders and a stopped interchange after IceKylin (PR #104).
• Complex side: a signed reclaim with completed-core sharing and one fix-up child per group.

The repository states that the claim is conditional: it assumes the full upstream multiplication theorem (the OpenAI manuscript and Colkitt's framework) and that stage two is the complement time-reversal of stage one, and it rests on three further interfaces that are stated but not machine-checked there — IceKylin's normal form for alternating residuals, the cost of binary address adapters for the exterior fix-up children, and the row stock of the stopped bit interchange. Its Lean files check only finite rational statements (moment certificates, the stopped mix and the parameter assembly), not the analytic inequalities or the multiplication theorem. It has not had independent review.

Earlier claims appear as milestones: Harvey–van der Hoeven ($\kappa=0$), OpenAI Theorem 1 ($2^{-182}$), Colkitt's $2^{-30}$ checkpoint, Jain rounds six and seven, and community PR #62. Each is implied by this goal because $L(n)^{1-\kappa}$ decreases in $\kappa$.

Significance

A proof for any positive value would give a strict asymptotic improvement over $n\log n$. Such an improvement would contradict the proposed $\Omega(n\log n)$ lower bound, while remaining consistent with the known upper bound. The tracked value concerns asymptotic growth; it does not measure the runtime of a practical implementation. No claim about a currently fastest implementation follows from a larger saving.

Formalizing the full target connects exact finite calculations to a uniform algorithm. The community repository explicitly treats the original framework and remaining all-size interfaces as assumptions of its current evidence. In this mission those steps must be proved before the goal can be marked Proved. They are not added as hypotheses that would weaken the full target. Earlier published theorem statements and finite certificates may be reused with their original attribution and proof status.

Difficulty

A finite network certificate can establish a concrete role count or a rational margin, but does not itself supply a machine for every input length. A complete proof must establish correctness of the recursive construction, admissibility of its parameters, precision and error guarantees, and the cost of moving data on tapes. Counts of algebraic operations alone do not account for this last resource. The difficult connection is between these separate contracts and the single uniform machine quantified by the goal.

Formalization scope

The goal imports the existing public Definitions.Def_IntMul_MultitapeModel bundle and uses IntMul.KappaBound directly. No alternative machine or cost model is introduced. Natural numbers describe input lengths, head positions, and step counts; real numbers describe the asymptotic constant and exponent. The real power has base at least one. Correctness is required even below the asymptotic threshold. Inputs of length zero and malformed inputs are outside the specified task.

The input and output conventions exclude a machine that merely decides a predicate about the product. The entire output tape must contain the required product and then blanks. Neither failure to halt nor correctness on a finite collection of test inputs meets the target. The work tapes and final head positions are unconstrained. Reusable contributions include machine composition with explicit costs, exact encodings, analytic estimates, and proofs that the finite certificates imply the contracts required by the recursive algorithm. Every such contribution should state its own assumptions and conclusion explicitly.

Selected references

• D. Harvey and J. van der Hoeven, Integer multiplication in time O(n log n), Annals of Mathematics 193(2), 563–617 (2021). Paper.
• OpenAI, Integer multiplication below n log n, preprint (23 September 2026), pinned manuscript revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source.
• D. Colkitt and community contributors, A sharper exponent for integer multiplication, research repository (2026), revision 56b66d58297deca1d7dd130247d720e960f77a37. Checkpoint and attribution.
• S. Jain, Integer multiplication: a conditional witness above $2^{-13}$ (integer-mult-kappa), research draft (2026), revision 5868dc701a9bec375c9dc5391d992ab3b8c35f3f. Round eight.

Motivation

Multiplying two binary integers is a basic task in computational complexity. The relevant resource here is the number of individual steps made by a machine whose tapes can only be accessed through moving heads. Harvey and van der Hoeven established an $O(n\log n)$ bound in this model. The OpenAI manuscript proposes a positive saving in the exponent of the logarithm. Subsequent constructions explore larger savings. The formalization target is the complete computation and its time bound, including the analytic and implementation arguments needed to connect a finite construction to every input length.

Setting

A deterministic multitape Turing machine has a fixed finite alphabet, a fixed finite state set, and a fixed finite number of tapes. Each tape extends in one direction and has one head. A step reads the symbols under the heads, changes state, writes at those positions, and moves each head by at most one cell. The alphabet contains distinct blank, start-marker, zero, one, and separator symbols. Tape zero is the read-only input tape; tape one is the output tape; further tapes are available for work. The halting state freezes the configuration.

An input consists of two bit strings $x,y$ of the same positive length $n$, separated by $\#$. The strings are read most significant bit first, with leading zeros permitted. If $\operatorname{val}(x)$ denotes the represented natural number, the required output is exactly the $2n$-bit binary representation of $\operatorname{val}(x)\operatorname{val}(y)$, padded with leading zeros and followed by blanks. All tapes begin with a preserved start marker. Define $L(n)=\max(\lceil\log_2 n\rceil,1)$.

Target

The full target is

$$\mathrm{IntMul.KappaBound}(0.00006397891967576).$$

This asserts the existence of one machine that computes the exact product correctly for every positive input length, together with constants $c>0$ and $n_0$ such that every pair of $n$-bit inputs, for $n\ge n_0$ and $n\ge1$, halts within

$$c\,n\,L(n)^{1-0.00006397891967576}$$

steps. Constants, alphabet, states, and tape count are independent of the input length. The number is an exact real value. Larger $\kappa$ gives a stronger asymptotic saving because $L(n)\ge1$.

Each entry supplies its own exact numerical value and identifies the construction that motivates it. Historical and new entries use the same machine definition. A proposed value may be recorded while its complete proof is still open; it becomes a proved record only when the goal has a verified proof. Numerical certificates are supporting results with their own scope, and do not establish a complete machine time bound.

This entry: Jain, round seven

The value

$$\kappa=\frac{799736495947}{12500000000000000}=0.00006397891967576\;(>2^{-14})$$

is the conditional witness of S. Jain's integer-mult-kappa, round seven, at revision c05adfe, with the sharper moment certificate merged there (research/round7-moment-refinement/). The README's headline for the same construction is the slightly smaller $1599247689723/(2.5\cdot10^{16})\approx6.39699\times10^{-5}$; the refinement keeps the frozen round-seven bit network, histogram, complex saving and assembly unchanged, and replaces the reciprocal bound $e^u\le1/(1-u)$ in the moment certificate by a degree-eight Taylor enclosure, which certifies the bit saving $a_b=63983013240044/10^{18}$.

The construction builds on the OpenAI manuscript and on Colkitt's integer-mult-bounds (it uses the PR #62 producer with interval strips and core-aware pair assembly). Its new ingredients are lifted frames with late copies, deferred readouts, and per-use $V$ leaves on the bit side; the complex side is round six's. The repository states that the claim is conditional on the OpenAI manuscript and Colkitt's framework, that stage two (the complement time-reversal of stage one) is assumed rather than machine-checked, and that its Lean files check only finite rational statements (moment certificates and parameter assembly), not the analytic tail inequalities or the multiplication theorem. It has not had independent review.

Earlier claims appear as milestones: Harvey–van der Hoeven ($\kappa=0$), OpenAI Theorem 1 ($2^{-182}$), Colkitt's $2^{-30}$ checkpoint, Jain round six ($3666565558019/10^{17}$) and community PR #62 ($0.000051016920170078$). Each is implied by this goal because $L(n)^{1-\kappa}$ decreases in $\kappa$.

Significance

A proof for any positive value would give a strict asymptotic improvement over $n\log n$. Such an improvement would contradict the proposed $\Omega(n\log n)$ lower bound, while remaining consistent with the known upper bound. The tracked value concerns asymptotic growth; it does not measure the runtime of a practical implementation. No claim about a currently fastest implementation follows from a larger saving.

Formalizing the full target connects exact finite calculations to a uniform algorithm. The community repository explicitly treats the original framework and remaining all-size interfaces as assumptions of its current evidence. In this mission those steps must be proved before the goal can be marked Proved. They are not added as hypotheses that would weaken the full target. Earlier published theorem statements and finite certificates may be reused with their original attribution and proof status.

Difficulty

A finite network certificate can establish a concrete role count or a rational margin, but does not itself supply a machine for every input length. A complete proof must establish correctness of the recursive construction, admissibility of its parameters, precision and error guarantees, and the cost of moving data on tapes. Counts of algebraic operations alone do not account for this last resource. The difficult connection is between these separate contracts and the single uniform machine quantified by the goal.

Formalization scope

The goal imports the existing public Definitions.Def_IntMul_MultitapeModel bundle and uses IntMul.KappaBound directly. No alternative machine or cost model is introduced. Natural numbers describe input lengths, head positions, and step counts; real numbers describe the asymptotic constant and exponent. The real power has base at least one. Correctness is required even below the asymptotic threshold. Inputs of length zero and malformed inputs are outside the specified task.

The input and output conventions exclude a machine that merely decides a predicate about the product. The entire output tape must contain the required product and then blanks. Neither failure to halt nor correctness on a finite collection of test inputs meets the target. The work tapes and final head positions are unconstrained. Reusable contributions include machine composition with explicit costs, exact encodings, analytic estimates, and proofs that the finite certificates imply the contracts required by the recursive algorithm. Every such contribution should state its own assumptions and conclusion explicitly.

Selected references

• D. Harvey and J. van der Hoeven, Integer multiplication in time O(n log n), Annals of Mathematics 193(2), 563–617 (2021). Paper.
• OpenAI, Integer multiplication below n log n, preprint (23 September 2026), pinned manuscript revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source.
• D. Colkitt and community contributors, A sharper exponent for integer multiplication, research repository (2026), revision 56b66d58297deca1d7dd130247d720e960f77a37. Checkpoint and attribution.
• S. Jain, Integer multiplication: a conditional witness above $2^{-14}$ (integer-mult-kappa), research draft (2026), revision c05adfe1dfe85326dd6dcf12bfd53f435bd49bf3. Round seven and the sharper moment certificate.

Motivation

Primal–dual interior-point methods solve a linear program by following, approximately, the central path of strictly feasible primal–dual pairs. Two families dominate the theory. Path-following methods keep the iterates in a neighbourhood of the path and measure progress by the duality gap. Potential-reduction methods measure progress by a merit function, the primal–dual potential of Todd and Ye (Todd–Ye 1990), and choose the step to decrease it.

The potential carries a parameter $\rho > n$. The classical analyses (Ye 1991, Freund, Anstreicher–Bosch, Kojima–Mizuno–Yoshise) give $O(\sqrt n\,t)$ iterations with $\rho = n + \Theta(\sqrt n)$. Practical codes, however, performed better with much larger $\rho$ (McShane–Monma–Shanno, Lustig–Marsten–Shanno). Mizuno, Todd and Ye (Cornell ORIE Technical Report No. 944, 1990, rev. 1991; journal version Math. Oper. Res. 18(4), 1993, doi:10.1287/moor.18.4.964) supply a worst-case justification for a large parameter. With $\rho = n + \Theta(n^2)$ and the step chosen to minimise the potential inside the wide neighbourhood $\mathcal N_\infty^-(\beta)$, the method needs $O(nt)$ iterations. That matches the adaptive-step path-following method in the same neighbourhood (their Theorem 2).

Timeline:

• 1990: Todd and Ye introduce the primal–dual potential function.
• 1989–1991: Kojima–Mizuno–Yoshise, Ye, Freund and others prove $O(\sqrt n\,t)$ bounds for $\rho = n + \Theta(\sqrt n)$.
• 1990–1991: Mizuno, Todd and Ye prove the $O(nt)$ bound for $\rho = n + \Theta(n^2)$ (Theorem 3 of the report formalized here).

Setting

Fix $m \ge 0$, $n \ge 1$, $A \in \mathbb R^{m\times n}$, $b \in \mathbb R^m$, $c \in \mathbb R^n$. The primal problem is $\min c^Tx$ subject to $Ax = b$, $x \ge 0$. The dual is $\max b^Ty$ subject to $A^Ty + s = c$, $s \ge 0$. The strictly feasible set $\mathcal F^0$ is the set of pairs $(x, s)$ with $x > 0$, $s > 0$, $Ax = b$ and $A^Ty + s = c$ for some $y$. The duality measure is $\mu = x^Ts/n$.

For $z \in \mathbb R^n$ put $(z^-)_j = \min\{z_j, 0\}$ and $\|z\|_\infty^- = \|z^-\|_\infty$. For $\beta \in (0,1)$, the wide neighbourhood is

$$\mathcal N_\infty^-(\beta) = \{(x,s) \in \mathcal F^0 : \|Xs - \mu e\|_\infty^- \le \beta\mu\},$$

i.e. $x_js_j \ge (1-\beta)\mu$ for all $j$, where $X = \mathrm{diag}(x)$ and $e$ is the all-ones vector.

The potential is

$$\psi(x,s) = \rho\log(x^Ts) - \sum_{j=1}^n \log(x_js_j), \qquad \rho > n,$$

with the natural logarithm. At $(x,s)$ and for $\gamma \in (0,1)$, a search direction $d = (d_x, d_y, d_s)$ solves

$$S d_x + X d_s = \gamma\mu e - Xs,\qquad A d_x = 0,\qquad A^Td_y + d_s = 0,$$

and the iterates move along $x(\theta) = x + \theta d_x$, $s(\theta) = s + \theta d_s$. The scaled vectors are $p_j = \sqrt{s_j/x_j}\,(d_x)_j$ and $q_j = \sqrt{x_j/s_j}\,(d_s)_j$, $Pq = (p_jq_j)_j$, and $\theta_2^- = \min\{1, \beta\gamma\mu/\|Pq\|_\infty^-\}$.

Algorithm 3. Start from $(x^0,s^0) \in \mathcal N_\infty^-(\beta)$ with $(x^0)^Ts^0 \le 2^t$ and $\psi(x^0,s^0) \le (\rho-n)t + n\log n$. While $(x^k)^Ts^k > 2^{-t}$, compute $d$ at $(x^k, s^k)$, choose $\bar\theta$ with $(x(\bar\theta), s(\bar\theta)) \in \mathcal N_\infty^-(\beta)$ and $\psi(x(\bar\theta), s(\bar\theta)) \le \psi(x(\theta), s(\theta))$ for every $\theta$ with $(x(\theta), s(\theta)) \in \mathcal N_\infty^-(\beta)$, and move to $(x(\bar\theta), s(\bar\theta))$.

Formalization targets

Goal: Theorem 3 (p. 11)

Let $\beta,\gamma \in (0,1)$ with $\gamma \le 2(1-\beta)$ and

$$\rho = n + \Bigl(\frac{3}{\beta\gamma(1-\gamma)}\log\frac{1}{1-\beta}\Bigr)n^2.$$

For every $t > 0$ and every run of Algorithm 3,

$$\exists\, k \le \Bigl\lceil \frac{6nt}{11\beta\gamma(1-\gamma)} \Bigr\rceil:\quad (x^k)^Ts^k \le 2^{-t}.$$

The paper states "$O(nt)$ iterations". The explicit count is the one its own proof yields, and it is stated so that the goal is not an existential over a constant.

Milestones

1. §5, p. 11. $\psi(x,s) = (\rho-n)\log(x^Ts) - \sum_j\log\frac{x_js_j}{x^Ts/n} + n\log n \ge (\rho-n)\log(x^Ts) + n\log n$. Hence reducing $\psi$ to $-(\rho-n)t + n\log n$ gives $x^Ts \le 2^{-t}$.
2. (16), p. 12. One step of Algorithm 3 satisfies $\psi(x(\bar\theta),s(\bar\theta)) - \psi(x,s) \le -\bigl(\frac{3n^2\theta_2^-}{\beta\gamma} - n\bigr)\log\frac{1}{1-\beta}$.
3. Proof of Theorem 3, p. 12. For $n \ge 1$, every step decreases $\psi$ by at least $11n\log\frac{1}{1-\beta}$.

Significance

The result shows that a potential-reduction method with $\rho - n$ of order $n^2$ keeps a polynomial worst-case bound. The earlier analyses cited by the report used $\rho - n$ of order $\sqrt n$. It thereby gives a worst-case justification for the large parameters that worked in practice. It also connects the two families: the direction is the path-following direction, and only the step rule changes. Corollary 3 of the paper adds that iterations with a small second-order term $Pq$ decrease the potential far more.

The result is proved in the report. As far as the platform's index shows, no part of it has been machine-checked. The platform already holds the potential function (Bertsimas–Tsitsiklis §9.3) and a proved bookkeeping theorem converting a constant per-iteration decrease into an iteration count (Bertsimas–Tsitsiklis Theorem 9.4). This mission adds the analysis of a concrete algorithm: the admissibility of the step $\theta_2^-$ in $\mathcal N_\infty^-(\beta)$, the potential decrease (16), and the complexity bound.

Difficulty

The step $\bar\theta$ is defined by minimisation, not by an explicit formula, so its decrease must be bounded by comparison with a step whose effect can be computed. That reference step must be shown to stay in the neighbourhood. This requires controlling the second-order term $Pq$ of the Newton direction in the one-sided norm $\|\cdot\|_\infty^-$, together with the centrality of the current iterate. A fixed decrease of order $n$ arises only because $\rho - n$ is of order $n^2$. Below that scale, the duality-gap term of the potential no longer dominates the loss in centrality from a long step.

A second obstacle is specific to formal work. Algorithm 3's rule ranges over every real $\theta$ whose point lies in the neighbourhood, and a minimiser need not exist. The goal must hold for every run, including the degenerate ones.

Formalization scope

Vectors are Fin n → ℝ, with index $j = 1,\dots,n$ mapped to Fin n; $\|\cdot\|_\infty$ is Mathlib's sup norm. The general standard-form LP pair is a separate definition, and the neighbourhood and algorithm build on its strict feasibility predicate. $\psi$ is the published definition LinearOptimization.interiorPointPotential with $q := \rho$. It equals (1) at every strictly positive pair, and it is evaluated only at points of $\mathcal N_\infty^-(\beta)$. All logarithms are natural, and $2^{\pm t}$ are real powers with real $t > 0$. A run is a pair of sequences satisfying the start conditions and, whenever the current gap exceeds $2^{-t}$, the step relation of Algorithm 3. Iterates after termination are unconstrained.

Conventions and repairs:

• $\theta_2^- := 1$ when $\|Pq\|_\infty^- = 0$, reading $\beta\gamma\mu/0$ as $+\infty$.
• The per-iteration milestone keeps the page's $n \ge 1$. The paper's step $\theta_2^- \ge 4\beta\gamma/n$ needs $4\beta\gamma \le n$, which can fail for $n = 1$; but for $n = 1$ the potential is unbounded below along the line inside the neighbourhood, so no step exists and the statement holds vacuously there. The goal keeps $n \ge 1$ as well.
• The minimisation in Algorithm 3 ranges over all real $\theta$, as printed. It does not range over a segment, and the step is not the largest admissible step of Algorithm 2.
• Both start conditions are kept: $(x^0)^Ts^0 \le 2^t$ from Algorithm 2 and the potential bound of §5.

A formalization in which no run can exist for any instance, or in which $\rho$ or the iteration count absorbs an instance-dependent constant, would trivialize the goal. The step relation above is satisfiable for $n \ge 2$ whenever the potential attains its minimum along the line, and the count is the explicit expression above.

Needed infrastructure: the algebra of system (2), namely $d_x^Td_s = 0$, the identity $\mu(\theta) = (1-(1-\gamma)\theta)\mu$, and $X(\theta)s(\theta) - \mu(\theta)e = (1-\theta)(Xs - \mu e) + \theta^2 Pq$. Also needed are the bounds $\|Pq\|_\infty \le \|r\|^2/4$ and $\|r\|^2 \le n\mu$ on $\mathcal N_\infty^-(\beta)$ when $\gamma \le 2(1-\beta)$, and the arithmetic–geometric mean inequality for $\psi$. These facts are shared with the sibling missions on the predictor–corrector and wide-neighbourhood algorithms of the same paper, and lemmas proved here are welcome there. The proved Bertsimas–Tsitsiklis theorem LinearOptimization.interior_point_potential_reduction is included as a reference item for the final counting step. Its hypotheses quantify over all iterations and need explicit dual iterates, so it does not apply verbatim.

Selected references

• S. Mizuno, M. J. Todd, Y. Ye, On adaptive-step primal-dual interior-point algorithms for linear programming, Cornell ORIE Technical Report No. 944, 1990, rev. 1991; Mathematics of Operations Research 18(4):964–981, 1993. https://doi.org/10.1287/moor.18.4.964
• M. J. Todd, Y. Ye, A centered projective algorithm for linear programming, Mathematics of Operations Research 15(3):508–529, 1990. https://doi.org/10.1287/moor.15.3.508

Motivation

Many combinatorial optimization problems ask for the largest value of a linear objective over discrete feasible solutions. A linear program over the convex hull of those solutions has the same optimum, so one approach is to describe that hull by inequalities. For matching, for example, inequalities support efficient optimization; for other problems, the full family can be very large. A generator of violated inequalities offers a different interface: given a proposed point, it either certifies hull membership or produces one valid inequality that the point violates. Karp and Papadimitriou asked what the existence of an efficient generator implies for the underlying decision problem. Their answer is Theorem 2 of the technical report.

The report appeared as MIT/LCS/TM-154 in 1980 and later in SIAM Journal on Computing in 1982. Its first theorem addresses a small facial description whose inequality family belongs to NP. This mission concerns its second theorem, where the inequalities may be generated on demand in polynomial time. The conclusion is stronger: the decision language itself belongs to P. The report derives an NP-complete consequence as Corollary 2, conditional on the unresolved equality P = NP. The published article gives the later bibliographic record; all numbering here follows the technical report.

Setting

A combinatorial optimization problem $C=(L,n,S)$ consists of a binary input language $L$, a nonnegative integer dimension $n(z)$, and a set $S(z)\subseteq\mathbb Z_+^{n(z)}$ of feasible vectors for each $z\in L$. The report requires polynomial-time recognition of $L$, of correctly sized pairs $\langle z,y\rangle$, and of feasible pairs $\langle z,x\rangle$. An instance adds an integer objective $c\in\mathbb Z^{n(z)}$. Its threshold decision language is

$$D(C)=\{\langle z,c,k\rangle:z\in L,\ k\in\mathbb Z,\ \exists x\in S(z),\ c\cdot x\ge k\}.$$

Write $\mathrm{CH}(S(z))$ for the convex hull of the feasible vectors. A generator $G(C)$ receives $z\in L$ and a rational vector $p\in\mathbb Q^{n(z)}$. It returns “O.K.” exactly when $p$ belongs to the hull. Otherwise it returns an integer vector $f$ and integer $g$ for which $f\cdot p>g$ while $f\cdot x\le g$ for every $x\in S(z)$. The family $F_G(C)$ contains every triple $\langle z,f,g\rangle$ that occurs as some output. It is a facial description because its inequalities describe the hull exactly. The generator is small if one polynomial $p_0$ bounds every coefficient in every output by $2^{p_0(|z|+n(z))}$ in absolute value. Its running time is measured on the full encoded query, including every rational coordinate. These definitions are from §§2 and 4 of the report.

Formalization targets

Theorem 2

The goal is the report's stated implication:

$$G(C)\text{ is a small polynomial-time generator}\quad\Longrightarrow\quad D(C)\in\mathrm P.$$

It allows any c.o.p. satisfying Definition 1, including an empty feasible set or dimension zero. It does not assert P = NP; that consequence needs the additional hypothesis that $D(C)$ is NP-complete. The goal is supported by five source claims: the output family is facial; feasibility of system (4) is equivalent to membership in $D(C)$; Lemma 4 bounds the distance from a rational point to a small hyperplane; its Corollary extends the bound to a real point on a flat; and Lemma 5 controls distance to a flat after one more hyperplane is added. The system (4) target is

$$\exists x\in\mathbb Q^{n(z)}:\quad c\cdot x\ge k,\quad f\cdot x\le g\quad(\langle z,f,g\rangle\in F_G(C))\quad\Longleftrightarrow\quad\langle z,c,k\rangle\in D(C).$$

The distance targets use the report's parameter $t$ and the bounds $2^{-(n(z)+1)t}$ and $(2^t-1)\delta$, exactly as printed on pp. 12–13.

Significance

Theorem 2 turns an efficient separation interface into an efficient test for the threshold language. Consequently, if a c.o.p.'s decision language is NP-complete, a small polynomial-time generator would imply P = NP, as the report's Corollary 2 says. This gives a complexity barrier to a whole class of proposed cutting-plane interfaces, independently of how many inequalities the complete description contains. The result concerns the worst-case running time and output coefficient size; it does not rule out useful generators without those guarantees. Karp and Papadimitriou also point out positive applications to problems already known to be in P.

The mathematical theorem was proved in the report. The mission asks for a machine-checked version of that known result, with explicit interfaces for the generator, coefficient bounds, and the underlying complexity class. The local platform catalog already contains Cook's Turing-machine definitions and a reusable binary-integer encoding; it also contains point-to-hyperplane distance results and a Gram-determinant distance result in other settings. Theorem 2 and these particular source claims are new formalization targets here. The distance and encoding interfaces can serve later missions about separation oracles and bit complexity.

Difficulty

Calling the generator once does not by itself decide whether the objective threshold is attainable: the point supplied to it may be outside the hull, and a single returned inequality says only that this point is excluded. Repeatedly asking at an unchanged point may return the same inequality. The report must also control very small separations, coefficient sizes, and finite precision when an iterative linear-feasibility procedure uses the oracle. Lemmas 4 and 5 quantify the geometric gaps and movement that such a procedure needs. Its Lemmas 2, 3, and 6 address the surrounding perturbation, volume, and iteration arguments; Lemma 6 explicitly relies on another analysis for the finite-precision bound. These are substantive proof obligations even though their statements are not all separate milestones in this proposal. See §4 of the report.

Formalization scope

The report's footnote uses $R$ for the rationals. Thus $p$, the hull, and system (4) live in $\mathbb Q^{n(z)}$. Euclidean distances are evaluated after casting coordinates into $\mathrm{EuclideanSpace}\,\mathbb R\,(\mathrm{Fin}\ n)$; a hyperplane distance is the quotient $|f\cdot r-g|/\|f\|_2$, and distance to a flat uses Euclidean infimum distance. The report does not define “affinely independent hyperplanes”; this mission reads it as linear independence of their normals, which ensures a common flat. Small hyperplanes have nonzero normals, avoiding a zero denominator.

The alphabet is $\{0,1,-,\#\}$. Binary tuple codes contain $z$, an explicit vector dimension, and every integer; a rational coordinate contains its reduced numerator and denominator. The generator's string function must match the mathematical oracle on every valid query and be polynomial time in the complete code length. A malformed string is outside $D(C)$. The source's arbitrary polynomial bound is written $m^a+a$ for one exponent $a$ fixed before all instances. For the bit-length parameter $t$, the printed logarithms of possibly nonpositive $c_i$ and $k$ are read as ceiling logarithms of absolute values, with $\operatorname{clog}_2(0)=0$ and the printed $+1$ terms retained. The source's formula $\varepsilon=2^{-(2n(z)+2)t}$ remains relevant to the eventual proof of Theorem 2, although no $\varepsilon$ system is a separate draft item here.

Every oracle answer must separate the queried point and remain valid on all of $S(z)$; these obligations prevent an arbitrary function from satisfying the goal. The c.o.p. structure retains all three polynomial-recognition conditions of Definition 1. The paper's displayed “min” in (3) is inconsistent with its threshold language and surrounding maximization formulas; $D(C)$ uses the printed $c\cdot x\ge k$. The typed source's “$x\notin H$” in Lemma 4 is read as the already named point $r\notin H$.

Contributions can develop the rational-hull equivalence, the two quantitative hyperplane lemmas, the finite-precision ellipsoid procedure underlying Lemma 6, or the perturbation and volume claims. The complexity substrate is Cook's one-tape model of P and NP, and the binary integer codec is the published ProjSchedTW_Complexity_Encoding definition. The geometry lemmas are phrased so that existing Mathlib Euclidean-space results can be reused without changing the source's rational optimization domain.

Selected references

• Richard M. Karp and Christos H. Papadimitriou, On Linear Characterizations of Combinatorial Optimization Problems, MIT/LCS/TM-154, Massachusetts Institute of Technology, 1980. Technical report.
• Richard M. Karp and Christos H. Papadimitriou, “On Linear Characterizations of Combinatorial Optimization Problems,” SIAM Journal on Computing 11 (1982), 620–632. DOI.
• Stephen A. Cook, “The Complexity of Theorem-Proving Procedures,” Proceedings of the Third Annual ACM Symposium on Theory of Computing, 1971. DOI.

Motivation

Polyhedral combinatorics attacks a combinatorial optimization problem by replacing its finite set of feasible solutions with the convex hull of that set and describing the hull by linear inequalities. Once such a description is known, the problem becomes a linear program, and linear programming duality supplies optimality certificates. For matchings, matroids and network flows this programme succeeded completely (Edmonds' matching polytope is the classical example). For the traveling salesman problem, set covering and integer programming, decades of work produced large families of valid and facet-defining inequalities but never a complete list.

R. M. Karp and C. H. Papadimitriou asked whether the failure is accidental. Their answer, in the MIT technical report On linear characterizations of combinatorial optimization problems (MIT/LCS/TM-154, February 1980; journal version SIAM J. Comput. 11 (1982) 620–632), is that for NP-complete problems a usable complete description cannot exist unless NP = co-NP. This mission formalizes the first of their two complexity results, Theorem 1, together with the steps of its proof and its Corollary 1.

Setting

A combinatorial optimization problem (c.o.p.) $C$ consists of a set $L\subseteq\{0,1\}^*$ of inputs, a function $n$ assigning to each input $z\in L$ a number of variables $n(z)\ge 0$, and for each $z\in L$ a set $S(z)\subseteq(\mathbb Z^+)^{n(z)}$ of nonnegative integer vectors, the feasible solutions. The three languages $L$, $\{\langle z,y\rangle : |y|=n(z)\}$ and $\{\langle z,x\rangle : x\in S(z)\}$ must be recognizable in polynomial time. An instance is a pair $\langle z,c\rangle$ with $z\in L$ and $c\in\mathbb Z^{n(z)}$, and the decision problem of $C$ is

$$D(C)=\{\langle z,c,k\rangle : z\in L,\ c\in\mathbb Z^{n(z)},\ k\in\mathbb Z,\ \exists x\in S(z)\ \ c\cdot x\ge k\}.$$

Write $\mathrm{CH}(S(z))\subseteq\mathbb Q^{n(z)}$ for the convex hull of $S(z)$ over the rationals. A facial description of $C$ is a set $F(C)$ of triples $\langle z,f,g\rangle$, with $z\in L$, $f\in\mathbb Z^{n(z)}$ and $g\in\mathbb Z$, such that for every $z\in L$ and every $x\in\mathbb Q^{n(z)}$

$$x\in\mathrm{CH}(S(z))\iff f\cdot x\le g\ \text{ for all }\langle z,f,g\rangle\in F(C).$$

It is small if for some polynomial $p$ every component of every triple $\langle z,f,g\rangle\in F(C)$ has absolute value at most $2^{p(|z|+n(z))}$, so that each coefficient has polynomially many bits. The statement $F(C)\in\mathrm{NP}$ means that the language of the triples of $F(C)$ is in NP: membership of a listed inequality has short, checkable proofs.

Formalization targets

Goal: Theorem 1 (p. 7)

$$F(C)\ \text{a small facial description of }C,\quad F(C)\in\mathrm{NP}\ \Longrightarrow\ D(C)\in\text{co-NP}.$$

Milestones, in the order the proof uses them

1. (p. 5) For a small facial description and every $z\in L$, only finitely many triples have first entry $z$, and $\mathrm{CH}(S(z))$ is the intersection of finitely many half-spaces.
2. (pp. 7–8, (i)⇔(ii)) $\langle z,c,k\rangle\notin D(C)$ iff $c\cdot x<k$ for every $x\in\mathrm{CH}(S(z))$.
3. (p. 8, (ii)⇔(iii)) For a facial description, the same holds with $\mathrm{CH}(S(z))$ replaced by the system $f\cdot x\le g$, $\langle z,f,g\rangle\in F(C)$.
4. (p. 8, (iii)⇔(vi)) For a small facial description and $S(z)\neq\emptyset$: $c\cdot x<k$ on that system iff there are $n(z)$ triples $\langle z,f_i,g_i\rangle\in F(C)$ whose matrix $\mathbf F$ is nonsingular and the solution $y$ of $y^T\mathbf F=c$ satisfies $y\ge 0$ and $y^Tg<k$.

After the goal: Corollary 1 (p. 8)

$$D(C)\ \text{NP-complete},\ F(C)\ \text{small facial},\ F(C)\in\mathrm{NP}\ \Longrightarrow\ \mathrm{NP}=\text{co-NP}.$$

Significance

Theorem 1 converts a question of polyhedral combinatorics into one of complexity theory. Corollary 1 then says that for the traveling salesman problem, Hamiltonian circuit, set covering, integer programming and every other c.o.p. with an NP-complete decision problem, no complete linear description of the hulls has both polynomially sized coefficients and polynomially verifiable membership, unless NP = co-NP. This explains why the search for complete descriptions of such polytopes has not succeeded and why research on them turned to partial descriptions and separation. The companion result of the same paper (Theorem 2, the subject of the second mission in this series) treats separation routines and P instead of facial descriptions and co-NP.

The result itself is proved, by a short argument in the paper. To our knowledge it has no machine-checked proof. Formalizing it requires connecting three things that the platform holds only separately: Cook's Turing-machine classes P, NP and co-NP (published as CookPvsNP_defs), linear programming duality over the rationals (Farkas' lemma is published, e.g. LinearOptimization.farkas_inequality_form_fintype, for real matrices), and polynomial-time arithmetic on binary-encoded rational data, such as solving a nonsingular integer linear system. The last ingredient, a polynomial-time verifier built from a polynomial-time recognizer, is reusable for every co-NP or NP membership proof on the platform.

Difficulty

The mathematical content of Theorem 1 is the duality chain (i)⇔(vi): the "no" answer is certified by $n(z)$ inequalities of $F(C)$ and a basic dual solution. Two points make the formal proof harder than the paper's page suggests.

First, the duality chain needs care at its edges. When $S(z)$ is empty the chain (iii)⇔(vi) can fail, so the verifier must also accept a different certificate (an infeasibility certificate from at most $n(z)+1$ triples), while milestone 4 carries the hypothesis $S(z)\neq\emptyset$. Pointedness of the hull, which follows from $S(z)\subseteq(\mathbb Z^+)^{n(z)}$, is what guarantees $n(z)$ linearly independent rows.

Second, "Algorithm B clearly runs in polynomial time" hides a complete complexity argument on Cook's one-tape machines: parsing the input, testing $z\in L$ and $|c|=n(z)$ with the recognizers of Definition 1, guessing the matrix within the size bound given by smallness, invoking the NP verifier of $F(C)$ $n(z)$ times, and solving $y^T\mathbf F=c$ exactly over $\mathbb Q$ with polynomially bounded bit sizes (Cramer's rule bounds the numerators and denominators of $y$). The certificate must be of length polynomial in the input, which uses the uniform polynomial in the definition of "small". The naive certificate, a single optimal vertex of the hull, does not work: it proves a "yes" answer, not a "no".

Formalization scope

All definitions live in the namespace KarpPapadimitriou.Facial. Strings are List Bool; $S(z)$ is a set of Fin (n z) → ℤ with nonnegative entries; $\mathrm{CH}(S(z))$ is convexHull ℚ of its image in Fin (n z) → ℚ, because the paper's "R" denotes the rationals (footnote, p. 3). Tuples are coded over the four-letter alphabet $\{0,1,-,\#\}$ of the published ProjSchedTW_Complexity_Encoding, integers in binary, vectors prefixed by their length so that codes are uniquely decodable. P, NP, co-NP and NP-completeness are the published CookPvsNP_defs; $D(C)$ and the triple language of $F(C)$ are sets of codes, so strings encoding no triple lie in the complement of $D(C)$, as in Algorithm B's step (i). The three polynomial-time conditions of Definition 1 are fields of the structure COP.

Explicit readings of the paper's loose phrases:

• "polynomial $p$" in "small" is $m\mapsto m^k+k$ with one $k$ for all triples;
• "has optimal value $<k$" for (ii) and (iii) is "every feasible point has value $<k$", meaningful for infeasible and unbounded programs;
• "the system $y^T\mathbf F=c$ has a unique nonnegative solution $y$ with $y^Tg<k$" is "$\det\mathbf F\neq0$ and the solution satisfies $y\ge 0$, $y^Tg<k$";
• (iii)⇔(vi) carries the hypothesis $S(z)\neq\emptyset$, tacit in the paper; Theorem 1 does not;
• "NP = co-NP" in Corollary 1 holds for every finite nonempty alphabet, since Cook's classes are indexed by the alphabet.

Printed slips: display (3) reads "min" while $D(C)$ and the proof maximize; Algorithm B's step (v) reads "$y^Tb>k$" for $y^Tg<k$. Both are formalized in the corrected sense.

A trivializing formalization is ruled out: the goal quantifies over every c.o.p. and every small facial description, with complements taken over all strings, and no hypothesis restricts $S(z)$ or $F(C)$ beyond Definition 1 and the definitions of p. 4–5. Claim 1 (p. 9), announced without proof, is not part of the mission.

Contributions welcome: proofs of the four milestones (milestone 4 is an exercise in rational LP duality on finite systems), a reusable library of polynomial-time integer and rational arithmetic on Cook's machines, and the closure of NP under polynomial-time reductions across alphabets that Corollary 1 needs.

Selected references

• R. M. Karp and C. H. Papadimitriou, On linear characterizations of combinatorial optimization problems, MIT/LCS/TM-154, February 1980. https://dspace.mit.edu/server/api/core/bitstreams/eb122126-c312-4445-a8d2-153e3e7d285f/content ; journal version SIAM J. Comput. 11 (1982) 620–632, https://doi.org/10.1137/0211053
• S. A. Cook, The P versus NP problem, Clay Mathematics Institute Millennium Problem description, 2000. https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf
• J. Edmonds, Maximum matching and a polyhedron with 0,1-vertices, J. Res. Nat. Bur. Standards 69B (1965) 125–130. https://doi.org/10.6028/jres.069B.013
• A. Schrijver, Theory of Linear and Integer Programming, Wiley, 1986 (LP duality, basic solutions, sizes of solutions of linear systems). ISBN 978-0-471-98232-6
• M. Grötschel and M. W. Padberg, On the symmetric travelling salesman problem I: Inequalities, Math. Programming 16 (1979) 265–280. https://doi.org/10.1007/BF01582116

How far apart can the two sensitivities be?

Sensitivity and block sensitivity measure two ways that a Boolean function can react to changes in its input. Both are basic measures in query complexity, where the input is accessed one coordinate at a time. Their relationship asks how much a function's response to changes involving several coordinates can exceed its response to individual coordinate changes.

Hao Huang's proof of the Sensitivity Conjecture established a polynomial relationship between sensitivity and polynomial degree in 2019, resolving the qualitative polynomial-relation question. The quantitative problem of obtaining the largest possible separation exponent remains the focus of this campaign. This mission asks for the specific exponent $2.10=21/10$.

The relevant progression is:

• The classical benchmark is a quadratic separation, included among the campaign's proved entries.
• In 2026, OpenAI problem 132 supplied a superquadratic construction and a Lean formalization establishing an exponent strictly above $2$.
• On 16 October 2026, the campaign had accepted proofs at exponents $2.0391$ and $2.05$. The 2.05 entry is the proved benchmark when this proposal is drafted.
• The present mission proposes $2.10$ as the next research target. It does not assert that a construction achieving this exponent is already known.

Boolean functions and sensitive changes

A total Boolean function assigns an output bit to every input consisting of $n$ bits:

$$f:\{0,1\}^n\longrightarrow\{0,1\}.$$

For an input $x$ and a coordinate set $B$, write $x^B$ for the input obtained by flipping exactly the coordinates in $B$. The sensitivity at an input counts the individual coordinates whose flip changes the output:

$$s(f,x)=\bigl|\{i:f(x^{\{i\}})\ne f(x)\}\bigr|.$$

The block sensitivity at an input is the largest number of pairwise disjoint nonempty coordinate sets whose separate flips each change the output:

$$bs(f,x)=\max\bigl\{m:\text{there are disjoint nonempty }B_1,\ldots,B_m \text{ with }f(x^{B_j})\ne f(x)\text{ for all }j\bigr\}.$$

The two global measures maximize over all inputs:

$$s(f)=\max_x s(f,x),\qquad bs(f)=\max_x bs(f,x).$$

There is no restriction to monotone functions, symmetric functions, or any particular construction. The number of variables may vary with the desired sensitivity threshold and approximation to the exponent.

Target: separation exponent at least 2.10

Prove that for every real $\varepsilon>0$ and every integer $S\ge2$, there are a dimension $n$ and a total Boolean function $f$ such that

$$s(f)\ge S,\qquad bs(f)\ge s(f)^{21/10-\varepsilon}.$$

The shared campaign predicate SensitivityCampaign.AchievesExponent (2.10 : ℝ) expresses exactly this statement. The decimal denotes the exact rational number $21/10$. The witnesses may depend on both $\varepsilon$ and $S$; no fixed function is required to work for every threshold. The unbounded-threshold requirement is essential to the asymptotic separation being asked for.

What reaching 2.10 would establish

A solution would strengthen the campaign's proved lower bound on the possible separation exponent from $2.05$ to $2.10$. It would provide Boolean functions with arbitrarily large sensitivity and block sensitivity growing with the specified larger power, with an arbitrarily small loss in the exponent.

This is an open research target, rather than a request to transcribe an existing proof of $2.10$. A complete contribution must establish the mathematical claim and provide a Lean proof using the shared definitions. Improvements to constructions, sharper bounds for existing constructions, and reusable supporting results are all relevant contributions. Acceptance of a proposal merely opens the target; a proof is needed to establish the new bound.

The main difficulty

A successful construction must support many disjoint sensitive blocks while controlling sensitivity at every input. A large collection of block witnesses at one input supplies only part of the required information: the upper bound on sensitivity is global. Bounds that lose too much in this global analysis can erase the desired exponent improvement.

The available campaign infrastructure already includes proved theorems converting suitable finite certificates into the asymptotic conclusion. The unresolved work is to obtain stronger certified bounds on a construction, or to establish the asymptotic target directly. A numerical estimate of a separation exponent does not replace a proof of the inequalities on which that estimate depends.

Formalization scope and existing foundations

Functions are represented as (Fin n → Bool) → Bool. Both complexity measures are natural-number maxima over finite sets; the comparison involving an exponent casts them to real numbers and uses real exponentiation. Since every requested witness satisfies $s(f)\ge S\ge2$, its power has a positive base. Zero-dimensional and constant functions cannot satisfy the sensitivity requirement.

The proposal retains the foundation definitions SensitivitySeparation and SensitivityCampaign. It also references two already-proved supporting theorems, rather than introducing alternative definitions or assuming any particular family of functions:

• SensitivityCampaign.finite_certificate: bounds on sensitivity and block sensitivity at a chosen input, together with an exact power inequality, imply the campaign conclusion at the stated nonnegative exponent.
• SensitivityCampaign.finite_certificate_log: the same finite bounds certify the exponent given by the ratio of their logarithms.

These statements are included as reusable foundation milestones. Their hypotheses require integer bounds greater than one, so the logarithmic denominator is positive. Solvers may use either criterion or prove the quantified target directly. The environment is Lean 4.33.1 with the campaign's pinned Mathlib revision.

Selected references

• Hao Huang, Induced subgraphs of hypercubes and a proof of the Sensitivity Conjecture, Annals of Mathematics 190 (2019), 949–955. Article.
• OpenAI, A superquadratic separation between sensitivity and block sensitivity, problem 132, 2026. Formalization scope and source links.
• Prove2Me, Block Sensitivity vs. Sensitivity, 2026. Campaign, shared foundations, and verified entries.

Establish a separation exponent of at least $2.0635$ between block sensitivity and sensitivity of total Boolean functions.

For every $\varepsilon>0$ and integer $S\ge2$, construct $f$ with $s(f)\ge S$ and $bs(f)\ge s(f)^{2.0635-\varepsilon}$.

Motivation

Multiplying two binary integers is a basic task in computational complexity. The relevant resource here is the number of individual steps made by a machine whose tapes can only be accessed through moving heads. Harvey and van der Hoeven established an $O(n\log n)$ bound in this model. The OpenAI manuscript proposes a positive saving in the exponent of the logarithm. Subsequent constructions explore larger savings. The formalization target is the complete computation and its time bound, including the analytic and implementation arguments needed to connect a finite construction to every input length.

Setting

A deterministic multitape Turing machine has a fixed finite alphabet, a fixed finite state set, and a fixed finite number of tapes. Each tape extends in one direction and has one head. A step reads the symbols under the heads, changes state, writes at those positions, and moves each head by at most one cell. The alphabet contains distinct blank, start-marker, zero, one, and separator symbols. Tape zero is the read-only input tape; tape one is the output tape; further tapes are available for work. The halting state freezes the configuration.

An input consists of two bit strings $x,y$ of the same positive length $n$, separated by $\#$. The strings are read most significant bit first, with leading zeros permitted. If $\operatorname{val}(x)$ denotes the represented natural number, the required output is exactly the $2n$-bit binary representation of $\operatorname{val}(x)\operatorname{val}(y)$, padded with leading zeros and followed by blanks. All tapes begin with a preserved start marker. Define $L(n)=\max(\lceil\log_2 n\rceil,1)$.

Target

The full target is

$$\mathrm{IntMul.KappaBound}(0.000051016920170078).$$

This asserts the existence of one machine that computes the exact product correctly for every positive input length, together with constants $c>0$ and $n_0$ such that every pair of $n$-bit inputs, for $n\ge n_0$ and $n\ge1$, halts within

$$c\,n\,L(n)^{1-0.000051016920170078}$$

steps. Constants, alphabet, states, and tape count are independent of the input length. The number is an exact real value. Larger $\kappa$ gives a stronger asymptotic saving because $L(n)\ge1$.

This entry targets the reviewed PR #62 checkpoint, $\kappa=0.000051016920170078=25508460085039/500000000000000000$. The pinned repository attributes the selected construction to Avi Eisenberg’s interval strips and core-aware pair assembly, eumemic’s joint frame compiler, and Alejandro Zarzuelo Urdiales’s exact parameter refinement and scoped Lean certificates. Douglas Colkitt maintains the project and its integration. The checkpoint combines a bit network with 575-way branching and 137,151,806 physical roles with the retained complex construction. Its finite arithmetic checks do not prove the complete multiplication algorithm. The full theorem remains an open obligation.

Significance

A proof for any positive value would give a strict asymptotic improvement over $n\log n$. Such an improvement would contradict the proposed $\Omega(n\log n)$ lower bound, while remaining consistent with the known upper bound. The tracked value concerns asymptotic growth; it does not measure the runtime of a practical implementation. No claim about a currently fastest implementation follows from a larger saving.

Formalizing the full target connects exact finite calculations to a uniform algorithm. The community repository explicitly treats the original framework and remaining all-size interfaces as assumptions of its current evidence. In this mission those steps must be proved before the goal can be marked Proved. They are not added as hypotheses that would weaken the full target. Earlier published theorem statements and finite certificates may be reused with their original attribution and proof status.

Difficulty

A finite network certificate can establish a concrete role count or a rational margin, but does not itself supply a machine for every input length. A complete proof must establish correctness of the recursive construction, admissibility of its parameters, precision and error guarantees, and the cost of moving data on tapes. Counts of algebraic operations alone do not account for this last resource. The difficult connection is between these separate contracts and the single uniform machine quantified by the goal.

Formalization scope

The goal imports the existing public Definitions.Def_IntMul_MultitapeModel bundle and uses IntMul.KappaBound directly. No alternative machine or cost model is introduced. Natural numbers describe input lengths, head positions, and step counts; real numbers describe the asymptotic constant and exponent. The real power has base at least one. Correctness is required even below the asymptotic threshold. Inputs of length zero and malformed inputs are outside the specified task.

The input and output conventions exclude a machine that merely decides a predicate about the product. The entire output tape must contain the required product and then blanks. Neither failure to halt nor correctness on a finite collection of test inputs meets the target. The work tapes and final head positions are unconstrained. Reusable contributions include machine composition with explicit costs, exact encodings, analytic estimates, and proofs that the finite certificates imply the contracts required by the recursive algorithm. Every such contribution should state its own assumptions and conclusion explicitly.

Selected references

• D. Harvey and J. van der Hoeven, Integer multiplication in time O(n log n), Annals of Mathematics 193(2), 563–617 (2021). Paper.
• OpenAI, Integer multiplication below n log n, preprint (23 September 2026), pinned manuscript revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source.
• D. Colkitt and community contributors, A sharper exponent for integer multiplication, research repository (2026), revision 56b66d58297deca1d7dd130247d720e960f77a37. Checkpoint and attribution.

Motivation

Grover's algorithm (Grover 1996) finds a marked item among $N$ with $O(\sqrt N)$ queries, a quadratic speed-up over any classical algorithm. Whether quantum computers can do substantially better on search, and so solve NP-type problems by brute force in polynomial time, was settled in the negative by Bennett, Bernstein, Brassard and Vazirani (arXiv:quant-ph/9701001, SIAM J. Comput. 26(5), 1997): relative to a random oracle, a quantum algorithm needs $\Omega(2^{n/2})$ queries to decide whether a string has a preimage. The bound matches Grover's algorithm up to a constant factor, and its hybrid argument is one of the two standard lower-bound methods of the field, together with the polynomial method (Beals et al. 1998) and the adversary method (Ambainis 2000).

Timeline:

• 1996: Grover's algorithm searches $N$ items with $O(\sqrt N)$ queries.
• 1997: the paper proves $\mathbf{BQTime}(o(2^{n/2})) \not\supseteq \mathbf{NP}$ relative to a random oracle with probability 1 (Theorem 3.5), and the $\Omega(2^{n/3})$ bound for random permutations (Theorem 3.6).
• 1998: Boyer, Brassard, Høyer and Tapp give tight bounds for quantum searching.
• 1999: Zalka shows Grover's algorithm is exactly optimal.

Setting

A $T$-query algorithm acts on vectors $\varphi \in \mathbb{C}^{(X \cup \{\bot\}) \times R \times W}$, where $X$ is the set of query strings, $R$ the set of answers (an additive group) and $W$ a finite workspace. A basis configuration $(x, z, w)$ with $x \in X$ is querying $x$; $(\bot, z, w)$ is not querying. For an oracle $f : X \to R$ the oracle operator is

$$O_f\,|x, z, w\rangle = |x, z + f(x), w\rangle, \qquad O_f\,|\bot, z, w\rangle = |\bot, z, w\rangle .$$

The algorithm consists of a unit vector $\varphi_0$, unitaries $U_0, \dots, U_{T-1}$ that do not depend on the oracle, and a set of accepting configurations. With oracle $A$ its states are $\varphi_{i+1} = U_i O_A \varphi_i$; the acceptance probability is the squared norm of the accepting part of $\varphi_T$. The query magnitude of $y$ in $\varphi$ is $q_y(\varphi) = \sum_{z, w} |\varphi(y, z, w)|^2$ (Definition 3.2). The algorithm decides a property if it accepts with probability at least $2/3$ when the property holds and at most $1/3$ when it fails.

In the main theorem $X = R = \{0,1\}^n$ with bitwise addition, and the oracle is a uniformly random function $A : \{0,1\}^n \to \{0,1\}^n$. The question is whether $1^n$ belongs to $\mathcal{L}_A = \{y : \exists x\ A(x) = y\}$.

Formalization targets

Goal: Theorem 3.5 (finite form)

$$\exists\, c > 0\ \exists N\ \forall n \ge N\ \forall M \text{ with } T \le c\, 2^{n/2} \text{ queries}: \quad \Pr_A\bigl[M^A \text{ fails to decide } \exists x\ A(x) = 1^n\bigr] \ge \tfrac18 .$$

The constant is existential, matching the theorem's hypothesis $T(n) = o(2^{n/2})$; $c$ and $N$ do not depend on the workspace or the algorithm.

Milestones

1. Theorem 3.1: unit vectors at distance $\varepsilon$ have measurement distributions within total variation $4\varepsilon$.
2. Theorem 3.3 (corrected): changing oracle answers on time–string pairs of total query magnitude $\le \varepsilon^2/T$ moves the final state by at most $2\varepsilon$.
3. Corollary 3.4 (corrected): outside a set of at most $4T^2/\varepsilon^2$ strings, changing the oracle at one string moves the final state by at most $\varepsilon$.
4. $\Pr[1^n \text{ has no preimage}] = ((2^n-1)/2^n)^{2^n} \ge 1/4$.
5. $\Pr[1^n \text{ has a unique preimage}] = ((2^n-1)/2^n)^{2^n-1} \ge 1/e$.
6. Final states within $1/13$ for $A$ and $A_y$ force failure on one of them.
7. The double counting: failing oracles with a unique preimage are at least half the successful oracles with none.

Significance

The theorem shows that the quadratic speed-up of Grover's algorithm cannot be improved for unstructured search, and that relative to a random oracle $\mathbf{NP} \not\subseteq \mathbf{BQP}$; any quantum algorithm for NP-complete problems must use the structure of the problem. Theorem 3.3 and Corollary 3.4 isolate the constraint unitary evolution places on "quantum parallelism" and are reused across quantum lower bounds, including the permutation bound of the companion mission (Theorem 3.6).

The results are proved on paper and, to our knowledge, have no machine-checked proof. The mission produces a formal query model with an XOR oracle, a formal hybrid argument, and the lower bound with its constants checked. Two printed bounds are wrong by constant factors (below); the formal statements carry the corrected constants, and a formal proof settles them. Grover's matching upper bound is on the platform as Grover.search_succeeds_bounded, for a phase oracle and one fixed algorithm.

Difficulty

The obvious argument — each query reveals one bit about where the preimage is, so $\Omega(2^n)$ queries are needed — fails for quantum algorithms, which query all strings in superposition at once. The difficulty is to bound how much a superposition of queries can learn, which requires controlling the accumulated effect of small changes across $T$ unitary steps, and then converting a bound on states into a statement about the probability of failure over random oracles, where the set of sensitive strings depends on the oracle.

Formalization scope

The paper's oracle quantum Turing machines are replaced by the query model above, the model its proofs use. Every oracle QTM running $T$ steps is a $T$-query algorithm: oracle answers on lengths other than $n$ are fixed and absorbed into the unitaries, as the proof fixes them, and the input $1^n$ is absorbed into $\varphi_0$. Queries return the full value $A(x) \in \{0,1\}^n$; one Boolean query is two full-value queries, so the goal implies the Boolean-oracle bound with $c$ halved. Strings are Fin n → ZMod 2; states are EuclideanSpace ℂ (Option X × R × W); probabilities over oracles are counting fractions over all $(2^n)^{2^n}$ functions; total variation distance is the paper's $\sum_x |\mathcal D(x) - \mathcal D'(x)|$ without the factor $1/2$.

Corrections: Theorem 3.3 is printed with conclusion $\le \varepsilon$, which fails (one query string, $T = 1$, distance $2$ at $\varepsilon = 1$; machine-checked); the true bound is $2\varepsilon$. Corollary 3.4 is printed with $|S| \le 2T^2/\varepsilon^2$, which fails (16 strings, $T = 1$, $\varepsilon = 0.45$); the true bound is $4T^2/\varepsilon^2$. The printed constant $T(n) \le 2^{n/2}/20$ in the proof of Theorem 3.5 does not support the step $2^n - \mathrm{card}(S) \ge 2^{n-1}$ even with the paper's own count; the goal states an existential constant, and $c = 1/37$ works with the corrected Corollary 3.4. The closing probability-$1$ argument over countably many machines and the class statement about $\mathbf{BQTime}$ are not formalized.

A formalization in which algorithms query at every step on every branch (no $\bot$ sector), only one side of the bounded-error condition is tested, or the probability is taken over a set of oracles that excludes the hard instances, proves a weaker theorem and is ruled out by these definitions.

Needed infrastructure: norms of finite-dimensional complex vectors, unitaries as linear isometry equivalences, finite counting of functions. The query model and the hybrid argument are reusable for any quantum query lower bound.

Selected references

• C. H. Bennett, E. Bernstein, G. Brassard, U. Vazirani, Strengths and weaknesses of quantum computing, SIAM J. Comput. 26(5):1510–1523, 1997. arXiv:quant-ph/9701001
• L. K. Grover, A fast quantum mechanical algorithm for database search, STOC 1996. arXiv:quant-ph/9605043
• M. Boyer, G. Brassard, P. Høyer, A. Tapp, Tight bounds on quantum searching, Fortschr. Phys. 46, 1998. arXiv:quant-ph/9605034
• C. Zalka, Grover's quantum searching algorithm is optimal, Phys. Rev. A 60, 1999. arXiv:quant-ph/9711070
• R. Beals, H. Buhrman, R. Cleve, M. Mosca, R. de Wolf, Quantum lower bounds by polynomials, J. ACM 48, 2001. arXiv:quant-ph/9802049
• A. Ambainis, Quantum lower bounds by quantum arguments, J. Comput. Syst. Sci. 64, 2002. arXiv:quant-ph/0002066

Motivation

In 1975 P. Brucker, J. K. Lenstra and A. H. G. Rinnooy Kan classified a large part of deterministic machine scheduling by computational complexity, using the then new theory of NP-completeness of Cook and Karp. Their report, Complexity of Machine Scheduling Problems (Mathematisch Centrum, Amsterdam, 1975; published in Annals of Discrete Mathematics 1, 1977), gives for many problems either a polynomial algorithm or a polynomial reduction from a known NP-complete problem. It drew the boundary between easy and hard scheduling problems that later surveys and the standard three-field classification build on.

This mission covers four reductions of the report's Theorem 4 that concern shops with several machines. A flow shop processes every job on machines $M_1, \dots, M_m$ in this order; a job shop lets each job follow its own route. For two machines and no further constraints, the flow shop is solved by Johnson's rule (Johnson, 1954) and the job shop with at most two operations per job by Jackson's extension of it (1956). The four reductions show that these positive results stop exactly where one more feature is added: one job with a nonzero release date, tree-shaped precedence constraints, a third operation per job, or a third machine.

Setting

A general shop instance has jobs $J_1,\dots,J_n$ and machines $M_1,\dots,M_m$. Job $J_j$ consists of $m_j$ operations; its $r$-th operation runs on machine $\mu_{jr}$ for $p_{jr}\in\mathbb N$ time units, and the tuple $\mu_j$ is the job's machine order (a machine may occur more than once). Each job has a release date $r_j$, and some pairs of jobs carry a precedence constraint $J_j<J_k$.

A schedule gives every operation a start time. It is feasible if no operation of $J_j$ starts before $r_j$; the operations of each job run in the order $\mu_j$, each after the previous one completes; two operations on the same machine never overlap; and $J_j<J_k$ implies $C_j\le B_k$, where $C_j$ is the completion time of $J_j$ and $B_k$ the starting time of $J_k$. The makespan is $C_{\max}=\max_j C_j$.

In the report's notation $n|m|\ell,\lambda|C_{\max}$, $\ell=F$ means a flow shop and $\ell=G$ a job shop; $\lambda$ may contain $r_n\ge 0$ (only the last job has a release date), tree (the precedence graph is a branching: no directed cycle, and either every indegree or every outdegree is at most one) and $m_j\le m_*$ (at most $m_*$ operations per job). The recognition version of a problem asks, for an instance and a number $y$, whether a feasible schedule with $C_{\max}\le y$ exists.

KNAPSACK asks, for positive integers $a_1,\dots,a_t$ and $b$, whether some $S\subseteq T=\{1,\dots,t\}$ has $\sum_{j\in S}a_j=b$. A problem $P'$ is reducible to $P$ ($P'\propto P$) if every instance of $P'$ can be transformed in polynomial time into an instance of $P$ with the same answer.

Formalization targets

Goal: Theorem 4(g)–(j)

$$\mathrm{KNAPSACK}\ \propto\ n|2|F,r_n{\ge}0|C_{\max},\quad n|2|F,\mathit{tree}|C_{\max},\quad n|2|G,m_j{\le}3|C_{\max},\quad n|3|G,m_j{\le}2|C_{\max}.$$

Each part is a polynomial-time many-one reduction between languages of binary strings. The other six parts of Theorem 4 (single-machine problems) belong to other missions of this series.

Milestones: the four equivalences

For positive $a_1,\dots,a_t,b$ with $0<b<A=\sum_{j\in T}a_j$, and for each of the paper's four constructions with its threshold $y$,

$$\exists\,S\subseteq T:\ \sum_{j\in S}a_j=b\iff\text{the constructed instance has a feasible schedule with } C_{\max}\le y,$$

with $y=A+1$ for (i), $y=2A$ for (j), $y=t(A+1)$ for (g) and $y=t(A+1)+1$ for (h). The milestones are stated directly about the printed constructions, in the order (i), (j), (g), (h) of the report.

Significance

With the NP-completeness of KNAPSACK (Karp, 1972), the goal makes the four problems NP-complete. As the report notes, (i) and (j) together with the elementary reductions of its Theorem 1 make the general job shop $n|m|G|C_{\max}$ NP-complete for every fixed $m\ge 2$. Parts (g) and (h) show that Johnson's two-machine algorithm admits neither release dates nor precedence constraints in general. Because KNAPSACK can be solved in pseudo-polynomial time, these results establish NP-hardness in the ordinary sense only; strong NP-hardness of some of these problems came later (Garey, Johnson and Sethi, 1976, for the three-machine flow shop).

The results are proved in the report; no machine-checked proof of any of them is known to exist. A formalization adds explicit constructions and complete equivalence proofs where the report is brief: in (h) it proves one inequality and states that the rest "is analogous to that of reduction (g)", and the forward directions are given by figures. It also produces a reusable formal model of general shops with integral start times, release dates, precedence and repeated machines.

Difficulty

Polynomial-time computability of the constructions is routine in principle but laborious in Cook's Turing-machine model, which is the setting of the goal: binary arithmetic for $A$, $t a_j$ and $t(A-b)$, and parsing of the KNAPSACK code.

The mathematical difficulty is the reverse direction of each equivalence. The report's arguments are phrased in terms of "a processing order on $M_1$" and treat the jobs before and after an extra job as two blocks. A formal proof must derive such an order from arbitrary start times and must handle every interleaving, including idle time and the case where the extra job's operations do not fit the printed pattern. In (j) the printed bound for the case $c<0$ contains a minimum of two quantities whose justification is left to the reader. In (h) the printed case uses $t a_j\ge t$, so the positivity of the data matters, and the remaining cases are only said to be analogous to (g).

Formalization scope

Jobs are Fin n and machines Fin m, both 0-based. A job's operations form a list of (machine, processing time) pairs, so machine orders may repeat machines, as $\mu_n=(M_2,M_1,M_2)$ in (i) does. Start times are natural numbers. The report computes schedules from processing orders on integer data, the makespan is a regular criterion, and release dates and precedence survive shifting operations left, so integral start times lose no value. $C_{\max}\le y$ is stated as $C_j\le y$ for every $j$; no maximum over an empty set is formed. Precedence $J_j<J_k$ is between jobs: every operation of $J_k$ starts no earlier than $C_j$. A branching is an acyclic precedence graph in which every indegree is at most one or every outdegree is at most one; the report's "either … or" is read for the whole graph. Job-shop classes require at least one operation per job. A flow-shop job has exactly the operations $(M_1,M_2)$, with times allowed to be zero.

The following readings of the report are made explicit. "Reducible" is Karp reducibility, CookPvsNP.PolyReducible from the published definitions CookPvsNP_defs. The languages are over the four-letter alphabet with binary numbers of the published definition ProjSchedTW.Complexity.Encoding. Its subsetSumLang allows zero sizes, while the report's KNAPSACK is over positive integers, so KNAPSACK is defined locally with positivity in the language. "We may assume that $0<b<A$" becomes a hypothesis of every equivalence; the goal's reduction must still handle the other inputs. The printed "value $C_{\max}=y$" of the forward directions is read as "$\le y$", as Section 2 defines the recognition version. The remark that (h) is analogous to (g) becomes the full equivalence for (h). An instance outside the problem's class is not in its language. NP-membership is not part of the goal.

The formal two-stage flow-shop models of Johnson's paper (JohnsonFlowShop.TwoStage.IsFeasible) and the job-shop model of Jansen, Solis-Oba and Sviridenko (JobShopLTAS.Core.Instance) use real start times and have neither release dates nor precedence. They were consulted, but the model here is local.

Ruled out as trivializing: a goal without the polynomial-time condition (the bare equivalence of yes-instances), a target language that accepts instances outside the class, and equivalences about some instance rather than the printed construction.

Contributions are welcome on any milestone, on a general lemma that turns a feasible schedule into a processing order per machine, and on polynomial-time computability of list arithmetic in the Turing-machine model, which every reduction of this series needs.

Selected references

• P. Brucker, J. K. Lenstra, A. H. G. Rinnooy Kan, Complexity of Machine Scheduling Problems, Mathematisch Centrum Report BW 43/75, Amsterdam, 1975; Annals of Discrete Mathematics 1 (1977) 343–362. https://doi.org/10.1016/S0167-5060(08)70743-X
• 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
• 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
• J. R. Jackson, An extension of Johnson's results on job lot scheduling, Naval Research Logistics Quarterly 3 (1956) 201–203. https://doi.org/10.1002/nav.3800030307
• M. R. Garey, D. S. Johnson, R. Sethi, The complexity of flowshop and jobshop scheduling, Mathematics of Operations Research 1 (1976) 117–129. https://doi.org/10.1287/moor.1.2.117
• S. A. Cook, The P versus NP problem, Clay Mathematics Institute. https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf