Complexity Theory

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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:

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

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

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)}$

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)

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)

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

Motivation

Project scheduling with cumulative resources models production and logistics projects in which activities fill and empty storage: an activity withdraws material from an inventory when it starts and deposits its output when it completes, and every inventory must stay between a safety stock and a storage capacity. Neumann, Schwindt and Zimmermann treat this model in §2.12 of Project Scheduling with Time Windows and Scarce Resources (2nd ed., Springer 2003, doi:10.1007/978-3-540-24800-2) and use it in their process-industry applications.

Before any optimization, a scheduler must know whether a feasible schedule exists at all. Theorem 2.12.1 of the book answers the complexity of this question: it is NP-complete, and it stays NP-complete when the project network has no cycles. The contrast with renewable resources (machines, workers) is the point of the theorem: with renewable resources, the feasibility problem is NP-complete as well (Theorem 2.3.13, after Bartusch, Möhring and Radermacher, 1988), but an acyclic network always admits a feasible schedule when every requirement is within capacity.

The mission also collects the two other reductions the book proves in full: Proposition 2.5.4 (recognizing whether an activity lies in some minimal delaying alternative, the branching object of the book's branch-and-bound procedures, is NP-complete) and Proposition 3.4.2 (maximizing weighted start-time deviations, a resource-levelling objective, is NP-hard without any resource constraints).

Setting

A project has activities $V=\{0,1,\dots,n+1\}$ with $n\ge1$; activity $0$ is the project beginning and $n+1$ the project completion. Activity $i$ has a duration $p_i\in\mathbb N$, with $p_0=p_{n+1}=0$. The project network $N$ has arc set $E$; an arc $\langle i,j\rangle$ with integer weight $\delta_{ij}$ imposes the temporal constraint $S_j-S_i\ge\delta_{ij}$ on the start times. A schedule is a real vector $S=(S_i)_{i\in V}$ with $S_0=0$ and $S_i\ge0$; it is time-feasible if it meets every temporal constraint.

Cumulative resources $k\in\mathcal R^\gamma$ carry integer demands $r_{ik}$: $r_{ik}<0$ depletes $-r_{ik}$ units at the start $S_i$, $r_{ik}>0$ replenishes $r_{ik}$ units at the completion $S_i+p_i$, and $r_{0k}$ is the initial stock. The inventory at time $t$ is

With safety stock $\underline R_k$ and storage capacity $\overline R_k$ (integers, $\underline R_k\le\sum_{i\in V}r_{ik}\le\overline R_k$ by (2.12.1)), $S$ is feasible if it is time-feasible and $\underline R_k\le r_k(S,t)\le\overline R_k$ for every $k$ and every $t\ge0$. The decision problem of $PSc|temp|C_{\max}$ asks whether a feasible schedule exists.

For renewable resources $k\in\mathcal R$ with capacities $R_k$ and requirements $r_{ik}\in\mathbb N$, a set $F\subseteq V$ is forbidden if $\sum_{i\in F}r_{ik}>R_k$ for some $k$. A delaying alternative for $F$ is a set $B\subseteq F$ such that $F\setminus B$ is not forbidden; it is minimal if no proper subset of $B$ is one.

In $PS\infty|temp,\bar d|f$ there are no resources, schedules must also satisfy $S_{n+1}\le\bar d$, and the objective here is $f(S)=-\sum_{i\in V}\sum_{j>i}w_{ij}|S_j-S_i|$ with weights $w_{ij}\ge0$.

NP and NP-completeness are taken in the sense of Cook's Turing-machine formulation, with instances written in binary.

Formalization targets

Goal: Theorem 2.12.1

Assuming PARTITION is NP-complete,

are both NP-complete.

Milestones

1. Membership (proof of Theorem 2.12.1): $L\in\mathrm{NP}$ and $L_{\mathrm{acyc}}\in\mathrm{NP}$.
2. Reduction correctness (proof of Theorem 2.12.1): for sizes $s(1),\dots,s(\nu)$ with even sum, the project with $r_0=r_{n+1}=-\sum s(i)/2$, $r_i=s(i)$, $\underline R=\overline R=0$, $d^{\min}_{0,n+1}=1$ has an acyclic network, and it has a feasible schedule iff the sizes split into two parts of equal sum.
3. Polynomial transformation: $\mathrm{PARTITION}\le_p L_{\mathrm{acyc}}$.
4. Proof of Proposition 2.5.4, one resource: for $j^*\in B\subseteq F$, $B$ is a minimal delaying alternative iff $R-\min_{j\in B}r_j<\sum_{i\in F\setminus B}r_i\le R$.
5. Proof of Proposition 2.5.4, with $r_{j^*}=1$: a minimal delaying alternative contains $j^*$ iff some $A\subseteq F\setminus\{j^*\}$ has $\sum_{i\in A}r_i=R$.
6. Proposition 2.5.4: assuming SUBSET SUM is NP-complete, deciding whether some minimal delaying alternative for a forbidden set $F$ contains $j^*\in F$ is NP-complete.
7. Proof of Proposition 3.4.2: a graph has a cut of at least $M$ edges iff the constructed instance has a schedule with $S_i\in\{0,1\}$ and $\sum_{i<j}w_{ij}|S_j-S_i|\ge M$.
8. Proposition 3.4.2: assuming SIMPLE MAX CUT is NP-complete, the decision version of $PS\infty|temp,\bar d|-\sum\sum w_{ij}|S_j-S_i|$ is NP-hard.

The goal follows from milestones 1 and 3 together with the transfer of NP-completeness along $\le_p$ (on the platform as CookPvsNP.npComplete_of_polyReducible).

Significance

The result. Theorem 2.12.1 explains why the book's methods for cumulative resources enumerate precedence relations between depleting and replenishing activities (minimal surplus and shortage sets, Theorem 2.12.4) instead of relying on a constructive feasibility test: unless P = NP, no polynomial algorithm decides feasibility, even for acyclic networks, where the renewable-resource case is trivial. Proposition 2.5.4 does the same for the branching scheme of §2.5, and Proposition 3.4.2 places the resource-levelling objectives of Chapter 3 among the hard ones.

Formalizing it. The three results are proved in the book, as short reductions whose delicate steps are left implicit: the polynomial size of a certificate for real-valued schedules, the handling of instances outside the construction (odd sums, empty index sets, oversized items), and the passage from an optimization problem to its decision version. None of the three reductions is machine-checked anywhere known. The mission states them against a single Turing-machine model and a single binary encoding, reusing the published definitions CookPvsNP_defs, so that the reductions compose with the Cook–Levin development already on the platform.

Difficulty

The mathematical content of the reductions is short; the difficulty is in the complexity-theoretic layer. Two steps resist the obvious argument.

First, NP membership. The book's certificate is a schedule, and a schedule is a real vector: it is not a string. A verifier needs a finite certificate of polynomial length, and it is not immediate that a feasible instance has a feasible schedule with small rational (or integer) start times, since the inventory constraints involve strict orderings between event times.

Second, polynomial-time computability in a concrete Turing-machine model. The transformation must compute, on a one-tape machine, binary codes of sums and halves of the input sizes, an arc list of quadratic length, and must map malformed strings to fixed no-instances. Informal "clearly polynomial" arguments have to become explicit machine constructions or a reusable library of closure properties.

Formalization scope

The Lean development fixes the following conventions.

• Activities are Fin (n + 2), with the completion Fin.last (n + 1); resources are Fin m. Start times are real.
• The inventory constraints hold for every $t\ge0$, not only for $0\le t\le\bar d$ as (2.12.2) is printed; the book's proofs use this reading.
• Real activities may have duration $0$ in $PSc|temp|C_{\max}$: the reduction of Theorem 2.12.1 uses only such activities.
• Instances are coded as lists of integers written in binary over the alphabet $\{0,1,-,\#\}$; arc weights are listed for every ordered pair of activities together with an arc indicator. Well-formedness (standing assumptions such as $n\ge1$, $p_0=p_{n+1}=0$, no loops, (2.12.1), $r_{ik}\le R_k$) is part of each language.
• "Acyclic" means the nodes admit a numbering increasing along every arc.
• The NP-completeness of PARTITION, SUBSET SUM and SIMPLE MAX CUT (Karp, 1972) enters as a hypothesis of the corresponding theorem; these are not results of the book.
• Proposition 3.4.2 is stated for the decision version of the optimization problem, with natural-number weights and threshold.

A trivializing formalization is ruled out: the languages contain only codes of well-formed instances, the encoding is injective, and the hypotheses on the source problems are true theorems, so the goal cannot hold vacuously or by a degenerate encoding.

A complete development needs closure properties of polynomial-time computable functions in Cook's model (composition, binary arithmetic, list manipulation), transitivity of $\le_p$, and a small-certificate lemma for systems of difference constraints with strict and non-strict inequalities. These are reusable for every NP-hardness proof stated in the same framework. Contributions to any of them, to the instance-level milestones 2, 4, 5 and 7, or to the NP-completeness of PARTITION, SUBSET SUM and SIMPLE MAX CUT in this model, are welcome.

Selected references

• K. Neumann, C. Schwindt, J. Zimmermann, Project Scheduling with Time Windows and Scarce Resources, 2nd ed., Springer, 2003. doi:10.1007/978-3-540-24800-2
• M. Bartusch, R. H. Möhring, F. J. Radermacher, Scheduling project networks with resource constraints and time windows, Annals of Operations Research 16, 1988.
• M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979.
• R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 1972. doi:10.1007/978-1-4684-2001-2_9
• S. Cook, The P versus NP Problem, Clay Mathematics Institute problem description. claymath.org

Prove a block-sensitivity versus sensitivity separation exponent of 2.15.

Motivation

Recommendation platforms and online retailers choose which products to show a customer, and customers often buy more than one of them in a single visit. Classical choice models such as the multinomial logit (MNL) assume a customer buys at most one product, and under MNL the revenue-maximizing set of products to display is easy to find: it is one of the $n$ revenue-ordered sets, so it can be found in linear time. Tulabandhula, Sinha, Karra and Patidar (arXiv:2006.08055, Manufacturing & Service Operations Management, 2023) introduce the BundleMVL-K model, a multivariate logit model in which a customer buys a bundle of up to $K$ products, with pairwise interaction terms that capture complementarity and substitution. They estimate it on retail data and design algorithms for choosing the recommendation set.

The first question for any such model is whether the revenue problem stays tractable once purchases of two products are allowed. Theorem 1 of the paper answers it negatively: already for $K=2$ the unconstrained revenue problem is NP-complete. This mission formalizes that theorem and its proof, a reduction from Max-Cut.

Setting

The products are $W=\{1,\dots,n\}$. Product $i$ has a revenue $r_i>0$. A BundleMVL-2 instance assigns a nonnegative weight $V_{\{i\}}$ to every product and $V_{\{i,j\}}$ to every unordered pair of products, together with a no-purchase weight $v_0>0$. (In the paper $V_S=\exp(\sum_{i\in S}\alpha_i+\sum_{i<j\in S}\beta_{ij})$, and $\beta_{ij}=-\infty$, so $V_{\{i,j\}}=0$, is allowed.) A customer shown the recommendation set $C\subseteq W$ buys the nonempty bundle $S\subseteq C$, $|S|\le 2$, with probability $V_S/(v_0+\sum_{S'}V_{S'})$, and buys nothing with probability $v_0/(v_0+\sum_{S'}V_{S'})$. The expected revenue of $C$ is eq. (4),

With the indicator $x^C_i$ of $C$, the weights $\theta_{ii}=V_{\{i\}}$, $\theta_{ij}=V_{\{i,j\}}/2$ ($i\ne j$) and the revenues $\hat r_{ii}=r_i$, $\hat r_{ij}=r_i+r_j$ ($i\ne j$), both numerator and denominator are quadratic forms in $x^C$.

The revenue problem (5) is $\max_{C\subseteq W}R_2(C)$; its decision version asks, for a threshold $\kappa$, whether some $C$ has $R_2(C)\ge\kappa$. SIMPLE MAX CUT asks, for a simple graph $G$ and an integer $M$, whether the nodes of $G$ split into two parts with at least $M$ edges between them.

Formalization targets

Goal: Theorem 1

NP-completeness is in the sense of Cook's Definition 4: membership in NP and a polynomial-time many-one reduction from every NP language.

Milestones

1. Eq. (4), second form: $R_2(C)=\dfrac{\sum_{i,j}\hat r_{ij}\theta_{ij}x^C_ix^C_j}{v_0+\sum_{i,j}\theta_{ij}x^C_ix^C_j}$.
2. Compare-Step: $\max_C R_2(C)\ge\kappa\iff\max_C\sum_{i,j}\theta_{ij}x^C_ix^C_j(\hat r_{ij}-\kappa)\ge\kappa v_0$.
3. Problem (7) is Max-Cut: for $Q=\begin{pmatrix}0&\mathbf d^\top/2\\ \mathbf d/2&-A'\end{pmatrix}$, the objective $\sum_{i,j}q_{ij}x^C_ix^C_j$ never decreases when the hub $0$ is added to $C$, and equals the size of the cut $(C\setminus\{0\},\ \text{rest})$ when $0\in C$.
4. The $\theta$ transformation: with $r_0>\kappa$ and $\kappa/2>r_1>\dots>r_m>0$, $\theta_{ij}=q_{ij}/(r_i+r_j-\kappa)$ is nonnegative and $\theta_{ij}(r_i+r_j-\kappa)=q_{ij}$.
5. Reduction correctness: $G$ has a cut of size $\ge M$ iff the constructed instance ($\kappa=1$, $v_0=M$) has some $C$ with $R_2(C)\ge 1$.
6. Hardness half: $\text{SIMPLE MAX CUT}\le_p\text{BundleMVL-2-DEC}$.
7. Membership half: $\text{BundleMVL-2-DEC}\in\mathrm{NP}$.

Significance

The result. Theorem 1 separates the multi-purchase model from its single-purchase counterpart: the revenue-ordered structure that makes MNL assortment optimization linear-time fails once pairs can be bought, and no polynomial-time exact algorithm exists unless P = NP. This is what justifies the paper's design of exact algorithms without running-time guarantees (a noisy binary search over the Compare-Step) and of polynomial-time heuristics, and it places BundleMVL-2 next to other hard assortment problems such as the mixture of two multinomial logits (Rusmevichientong et al. 2010, as cited by the paper) and the MMC model of Benson, Kumar and Tomkins (2018), whose hardness is the paper's Theorem 2.

Formalizing it. The theorem is proved in the paper; no machine-checked proof exists. The paper's argument constructs the instance and asserts the equivalence; it does not argue NP membership or the polynomial running time of the reduction, and it leaves the revenues and threshold free subject to inequalities. A formal proof must fix concrete rational parameters, show that the instance code has polynomial size, and handle malformed inputs. The Compare-Step identity (milestone 2) is also the correctness lemma for the paper's binary-search algorithm.

Difficulty

The mathematics of the reduction is short; the obstacles are the two halves that the paper treats as evident. First, the reduction must be a polynomial-time computable map on strings, in Cook's one-tape Turing-machine model, that sends codes of Max-Cut instances to codes of BundleMVL-2 instances and every other string to a non-member; the rational entries $\theta_{ij}=2q_{ij}/(r_i+r_j-\kappa)$ must be computed and written in reduced form. Second, NP membership needs a polynomial-time verifier that evaluates $R_2(C)$ exactly in rational arithmetic, with a bound on the bit size of the sums. An approach that states the reduction as "for every graph there is an instance with the same answer" proves nothing: a fixed yes- or no-instance does that.

Formalization scope

The development is in MultiPurchase.Hardness. Conventions committed to:

• Products are Fin n, 0-based; in the reduction the hub is 0 : Fin (m+1) and graph node i : Fin m is product i.succ.
• All parameters are rational (ℚ). Weights may be zero ($V\ge 0$), as the paper's own reduction requires ($V_{\{i\}}=\theta_{ii}=0$); revenues are positive and $v_0>0$. These well-formedness conditions are part of the yes-predicate.
• Only pair weights $V_{\{i,j\}}$ with $i<j$ are read, so the code of an instance determines its answer. The empty bundle is the no-purchase option; $R_2(\emptyset)=0$.
• The decision version is "some $C\subseteq W$ has $R_2(C)\ge\kappa$" (ties count). Instances are coded over the published four-letter alphabet BSym, rationals as reduced numerator and denominator.
• The reduction uses $\kappa=1$, $r_0=2$, $r_i=1/4-i/(8(m+1))$ for the nodes, $V_{\{i,j\}}=2\theta_{ij}$, $v_0=M$; Max-Cut instances with $M=0$ are outside the construction (they need $v_0=0$).
• The NP-completeness of SIMPLE MAX CUT (Karp 1972) is a hypothesis of the goal; the platform has no proof of it.

The complexity layer is the published CookPvsNP_defs (Cook's $P$, $NP$, $\le_p$, NP-completeness) and ProjSchedTW_Complexity_Encoding (binary codes, cutSize, maxCutLang), with the proved CookPvsNP.polyReducible_trans. Contributions welcome: Turing-machine programs for rational arithmetic and list manipulation (reusable for every NP-membership proof over rational data), the polynomial-time reduction, and a proof of Karp's theorem for SIMPLE MAX CUT, which would discharge the hypothesis.

Selected references

• T. Tulabandhula, D. Sinha, S. R. Karra, P. Patidar, Multi-Purchase Behavior: Modeling, Estimation and Optimization, Manufacturing & Service Operations Management, 2023; arXiv:2006.08055v2. https://arxiv.org/abs/2006.08055
• 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
• A. R. Benson, R. Kumar, A. Tomkins, A Discrete Choice Model for Subset Selection, WSDM 2018. https://doi.org/10.1145/3159652.3159702
• S. Cook, The P versus NP Problem, Clay Mathematics Institute problem description. https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf

Motivation

Many proposed quantum optimization and machine-learning methods (variational quantum eigensolvers, QAOA, quantum classifiers) tune the real parameters of a circuit by gradient descent on an objective $f:\mathbb R^d\to\mathbb R$ that is only accessible as a black box. Classically, a finite-difference estimate of $\nabla f$ costs on the order of $d$ evaluations of $f$. Quantum algorithms can access $f$ coherently through a phase oracle $O_f:|x\rangle\mapsto e^{if(x)}|x\rangle$, and the question is how many such queries are needed to learn $\nabla f(x)$ to accuracy $\varepsilon$ in the sup norm.

Timeline.

• 2005: Jordan (Phys. Rev. Lett. 95, 050501) gave an algorithm that reads off the gradient of a nearly affine function from a single oracle call on a uniform superposition over a grid, followed by an inverse quantum Fourier transform. The guarantee requires $f$ to be very close to affine on the grid.
• 2017–2019: Gilyén, Arunachalam and Wiebe (arXiv:1711.00465v3; SODA 2019) ran Jordan's algorithm on a high-degree central difference of $f$ rather than on $f$. For functions whose derivatives satisfy a Gevrey-type bound, they obtained $\widetilde O(c\sqrt d/\varepsilon)$ phase queries (Theorem 25), and proved a matching $\Omega(\sqrt d/\varepsilon)$ lower bound for a class of smooth functions.
• 2024: Nannicini's lecture notes (arXiv:2408.07086) present Jordan's algorithm in this form. Their Lean formalization on the platform contains the grid, its Fourier transform and the algorithm's state, which this mission reuses.