Complexity Theory

Motivation

A promise constraint satisfaction problem $\mathrm{PCSP}(\mathbf A,\mathbf B)$ asks to distinguish instances that are satisfiable in a structure $\mathbf A$ from instances that are not even satisfiable in a weaker structure $\mathbf B$. Approximate graph colouring (tell 3-colourable graphs from graphs that are not 5-colourable) and $(1\text{-in-}3\text{-SAT},\ \mathrm{NAE\text{-}SAT})$ are standard examples. The algebraic approach to CSPs explains the complexity of such problems through polymorphisms, the multi-argument maps $A^L\to B$ that preserve every relation.

Two polynomial-time relaxations dominate the algorithmic side: the Basic LP relaxation, solved over $\mathbb Q_{\ge0}$, and the affine relaxation, the same linear system solved over $\mathbb Z$. Barto, Bulín, Krokhin and Opršal (BBKO19) characterized each one separately: BLP solves $\mathrm{PCSP}(\mathbf A,\mathbf B)$ exactly when $\mathrm{Pol}(\mathbf A,\mathbf B)$ has symmetric polymorphisms of all arities, and the affine relaxation exactly when it has alternating polymorphisms of all odd arities. Brakensiek and Guruswami (BG19) used ad hoc combinations of the two. Brakensiek, Guruswami, Wrochna and Živný (arXiv:1907.04383) combine them into a single algorithm, BLP+Affine, and characterize its power exactly. This mission formalizes that characterization, Theorem 4 of the paper.

Setting

A signature assigns to each symbol $R$ an arity $\mathrm{ar}(R)$. A relational structure $\mathbf A$ on a finite domain $A$ fixes relations $R^{\mathbf A}\subseteq A^{\mathrm{ar}(R)}$. A homomorphism $\mathbf A\to\mathbf B$ is a map $\sigma:A\to B$ sending every tuple of $R^{\mathbf A}$ into $R^{\mathbf B}$, and $(\mathbf A,\mathbf B)$ is a promise template if one exists. An instance $X$ has variables $x_1,\dots,x_n$ and constraints $(R_j,\bar x_j)$; it is satisfiable in $\mathbf C$ (written $X\to\mathbf C$) if some assignment sends each $\bar x_j$ into $R_j^{\mathbf C}$.

A map $f:A^L\to B$ is a polymorphism if applying $f$ column-wise to any $L\times\mathrm{ar}(R)$ matrix whose rows are in $R^{\mathbf A}$ gives a tuple of $R^{\mathbf B}$. It is block-symmetric for a partition $[L]=B_1\sqcup\dots\sqcup B_\kappa$ if it is invariant under permutations of its arguments that preserve every block, and its width is the largest minimum block size over such partitions.

The Basic LP $\mathrm{LP}_{\mathbb Q}(X,\mathbf A)$ has a probability distribution $w_i$ on $A$ for each variable and $p_j$ on $R_j^{\mathbf A}$ for each constraint, with the marginal of $p_j$ at each position of $\bar x_j$ equal to the distribution of the variable in that position. The affine relaxation $\mathrm{Aff}_{\mathbb Z}(X,\mathbf A)$ is the same system over $\mathbb Z$ with unknowns $r_i$, $q_j$ and no sign constraints. BLP+Affine (Figure 1) takes a relative interior point $(w,p)$ of the LP, keeps only the integer solutions $(r,q)$ that vanish wherever $(w,p)$ does, and accepts iff one remains. It correctly solves $\mathrm{PCSP}(\mathbf A,\mathbf B)$ if it accepts every $X\to\mathbf A$ and rejects every $X\not\to\mathbf B$.

The minor of $f:A^L\to B$ along $\pi:[L]\to[L']$ is $f_{/\pi}(x_1,\dots,x_{L'})=f(x_{\pi(1)},\dots,x_{\pi(L)})$. The minion $\mathcal M_{\mathrm{BLP+Aff}}$ has as $L$-ary objects the pairs $(w,r)$ with $w:[L]\to\mathbb Q_{\ge0}$, $r:[L]\to\mathbb Z$, both summing to $1$, and $w(i)=0\Rightarrow r(i)=0$; the minor along $\pi$ sums both over fibres of $\pi$. A minion homomorphism $\xi:\mathcal M_{\mathrm{BLP+Aff}}\to\mathrm{Pol}(\mathbf A,\mathbf B)$ sends $L$-ary objects to $L$-ary polymorphisms and commutes with minors. The free structure $F_{\mathcal M_{\mathrm{BLP+Aff}}}(\mathbf A)$ has the $|A|$-ary objects as its domain, and a tuple is in $R^F$ iff it is the family of coordinate minors of one $|R^{\mathbf A}|$-ary object.

Formalization targets

Goal: Theorem 4

For a promise template $(\mathbf A,\mathbf B)$ on finite domains, the following are equivalent:

$$\text{BLP+Affine correctly solves } \mathrm{PCSP}(\mathbf A,\mathbf B) \iff \forall N\ \exists f\in\mathrm{Pol}(\mathbf A,\mathbf B):\ \mathrm{width}(f)\ge N \iff \forall L\ \exists f\in\mathrm{Pol}^{(2L+1)}\ \text{symmetric on blocks of sizes } L,\ L+1.$$

Milestones

The paper proves Theorem 4 through Lemmas 7, 8 and 9. The milestones follow that proof:

• $\mathcal M_{\mathrm{BLP+Aff}}$ is a minion (p. 10);
• Lemma 8: a minion homomorphism $\mathcal M_{\mathrm{BLP+Aff}}\to\mathrm{Pol}(\mathbf A,\mathbf B)$ yields the $(2L+1)$-ary two-block polymorphisms;
• the finite-subset construction in the proof of Lemma 9: a symmetric polymorphism of arity $L^*\ge M\ell^2$, $L^*=u\ell+v$, gives a minion homomorphism on the finite set $\mathcal M_{\ell,M}$ by repeating coordinate $i$ exactly $W_i=u\ell w(i)+v r(i)$ times;
• Lemma 9: block-symmetric polymorphisms of arbitrarily high width yield a minion homomorphism;
• Observation 15, Lemma 16 (compactness for structures) and Lemma 17 (free structures versus minion homomorphisms, for $\mathcal M_{\mathrm{BLP+Aff}}$), which together give
• Lemma 7: BLP+Affine correctly solves $\mathrm{PCSP}(\mathbf A,\mathbf B)$ iff $\mathcal M_{\mathrm{BLP+Aff}}\to\mathrm{Pol}(\mathbf A,\mathbf B)$.

A companion item, Example 10, records that the disjoint union of a directed 2-cycle and a directed 3-cycle has no block-symmetric polymorphism of width at least $2$.

Significance

Theorem 4 is an exact criterion: the power of an algorithm is read off from the polymorphisms of the template. Its sufficiency direction (Theorem 3, the subject of the companion mission) says that one fixed algorithm decides every PCSP with block-symmetric polymorphisms of unbounded width, which covers nearly all tractable Boolean PCSPs known at the time, including those with threshold and alternating-threshold polymorphisms. The necessity direction, new in Theorem 4, gives a method for proving that BLP+Affine fails on a template: exhibit, for some $L$, the absence of a $(2L+1)$-ary polymorphism with blocks of sizes $L$ and $L+1$. Example 10 is an instance: a tractable template that the algorithm does not solve. The minion $\mathcal M_{\mathrm{BLP+Aff}}$ and its free structure are the template for later characterizations of relaxation hierarchies.

The result is proved in the paper. As far as is known it has not been machine-checked. A formalization adds a checked development of minions, minion homomorphisms and free structures for PCSPs, a compactness theorem for relational structures, and a checked version of the one-block argument whose many-block extension the paper only asserts.

Difficulty

The equivalence passes through three different kinds of object: an algorithm, an infinite algebraic object (a homomorphism defined on all of $\mathcal M_{\mathrm{BLP+Aff}}$), and finite families of polymorphisms. From polymorphisms one obtains homomorphisms only on finite pieces $\mathcal M_{\ell,M}$, each from a different polymorphism, and these do not agree with one another; a single homomorphism on the whole minion needs a compactness argument over the finitely many restrictions, which uses the finiteness of $A$ and $B$. The passage from "every instance satisfiable in the free structure is satisfiable in $\mathbf B$" to a homomorphism from the infinite free structure is a second compactness step. The relative interior point of Figure 1 must be kept: accepting whenever both relaxations are merely feasible is a different, weaker algorithm.

Formalization scope

All objects are in the definitions file PCSPBLPAff.Characterization.Setting, built on Mathlib only.

• Signatures are (τ : Type) (ar : τ → ℕ), with no finiteness of $\tau$; the paper's requirement that arities be positive is dropped, and no statement needs it. Domains are finite types; instance variables are Fin n and arities Fin L.
• The LP is over $\mathbb Q$ and the affine system over $\mathbb Z$. Constraint distributions are functions on all tuples that vanish outside $R^{\mathbf A}$, and marginal conditions are imposed per position of a constraint's scope.
• The relative interior point is encoded by the only property the algorithm uses: a solution whose zero coordinates are exactly those that vanish on the whole polytope. The algorithm is formalized by its acceptance condition; the polynomial-time claims are out of scope.
• Width requires at least one block, so a nullary function does not have every width.
• There is no abstract minion structure. A minion homomorphism $\mathcal M_{\mathrm{BLP+Aff}}\to\mathrm{Pol}(\mathbf A,\mathbf B)$ is spelled out as a family of maps from objects of each arity to polymorphisms of that arity, commuting with minors. Lemma 17 is stated for $\mathcal M=\mathcal M_{\mathrm{BLP+Aff}}$. Free-structure objects are indexed by $A$ and by tuples, identifying $A$ with $[|A|]$.
• Lemma 16 drops the hypothesis that $\mathbf F$ is infinite, which is unnecessary.

Two trivializing formalizations are ruled out: the acceptance condition keeps the maximal-support requirement, and the free structure's relation requires the witnessing pair to be an object of $\mathcal M_{\mathrm{BLP+Aff}}$ supported in $R^{\mathbf A}$.

A complete development needs finite sums over fibres, transport of objects along Fintype.equivFin, Tychonoff or König's lemma (Mathlib.Order.KonigLemma, Mathlib.Combinatorics.Compactness), and the existence of a maximal-support point of a rational polytope. The compactness theorem for relational structures and the free-structure lemma are reusable beyond this mission. Proofs of any milestone, and of the general Lemma 17 for an abstract minion, are welcome.

Selected references

• J. Brakensiek, V. Guruswami, M. Wrochna, S. Živný, The Power of the Combined Basic LP and Affine Relaxation for Promise CSPs, arXiv:1907.04383v3, 2020 (also SIAM J. Comput., 2020, https://doi.org/10.1137/20M1312745). https://arxiv.org/abs/1907.04383
• L. Barto, J. Bulín, A. Krokhin, J. Opršal, Algebraic approach to promise constraint satisfaction, arXiv:1811.00970, 2019; J. ACM 68(4), 2021. https://arxiv.org/abs/1811.00970
• J. Brakensiek, V. Guruswami, An Algorithmic Blend of LPs and Ring Equations for Promise CSPs, SODA 2019, pp. 436–455. https://arxiv.org/abs/1807.05194
• R. Diestel, Graph Theory, 5th ed., Springer, 2016, Theorem 8.1.3 (de Bruijn–Erdős compactness). https://doi.org/10.1007/978-3-662-53622-3

Motivation

A constraint satisfaction problem (CSP) asks whether variables can be assigned values from a finite domain so that every constraint, drawn from a fixed list of allowed relations, is satisfied. A promise CSP (PCSP) relaxes the question: given two templates $\mathbf A$ and $\mathbf B$ with a homomorphism $\mathbf A\to\mathbf B$, distinguish instances satisfiable in $\mathbf A$ from instances not even satisfiable in the weaker $\mathbf B$. Approximate graph colouring (colour a graph with more colours than its chromatic number) is the standard example. For CSPs, the resolution of the Feder–Vardi dichotomy conjecture by Bulatov and Zhuk (FOCS 2017) ties tractability to the existence of polymorphisms satisfying non-trivial identities; for PCSPs no such dichotomy is known, and the question of which polymorphism families yield algorithms is open in general.

A polymorphism of a PCSP is a function $f:A^L\to B$ mapping tuples of rows satisfying the strict constraints to columns satisfying the weak ones. Brakensiek, Guruswami, Wrochna and Živný (arXiv:1907.04383v3, SIAM J. Comput. 2020) give a single algorithm, BLP+Affine, that decides every PCSP with infinitely many symmetric polymorphisms, and extend it to block-symmetric polymorphisms. As a corollary the same algorithm solves all tractable Boolean CSPs of Schaefer's dichotomy (2-SAT, Horn-SAT and its dual, linear equations mod 2).

Timeline, as recorded in the paper's introduction:

• 2012: Kun, O'Donnell, Tamaki, Yoshida and Zhou (ITCS 2012): with symmetric polymorphisms of all arities, the Basic LP alone decides the CSP; with only some arities (e.g. odd majorities) it does not.
• 2017: Austrin, Guruswami and Håstad classify $(2+\epsilon)$-SAT and introduce polymorphisms for PCSPs (SIAM J. Comput. 46(5), 2017).
• 2018–2019: Brakensiek and Guruswami study PCSPs through polymorphisms; their SODA 2019 algorithm (arXiv:1807.05194) solves the search version for PCSPs with structured symmetric polymorphisms (threshold, threshold-periodic, regional), combining an LP over $\mathbb Z[\sqrt2]$ with an affine relaxation over a finite ring.
• 2019: Barto, Bulín, Krokhin and Opršal (arXiv:1811.00970) show that the identities satisfied by polymorphisms, captured by minion homomorphisms, determine the complexity of a PCSP.
• 2019–2020: the present paper. Theorem 2 needs only that $f$ be symmetric, with no structure beyond that; Theorem 3 handles any number of blocks; Theorem 4 characterizes exactly the PCSPs that BLP+Affine solves.

Setting

A signature $\tau$ is a set of symbols $R$ with arities $\mathrm{ar}(R)$. A relational structure $\mathbf A$ on a finite domain $A$ gives, for each $R$, a relation $R^{\mathbf A}\subseteq A^{\mathrm{ar}(R)}$. A homomorphism $\mathbf A\to\mathbf B$ is a map $\sigma:A\to B$ sending every tuple of $R^{\mathbf A}$, componentwise, into $R^{\mathbf B}$; $(\mathbf A,\mathbf B)$ is a promise template when one exists.

An instance $X$ has variables $x_1,\dots,x_n$ and constraints $c_j=(R_j,\bar x_j)$, $j\in[m]$, where $\bar x_j$ is a tuple of $\mathrm{ar}(R_j)$ variables. $X$ is satisfiable in $\mathbf A$ if some assignment sends every $\bar x_j$ into $R_j^{\mathbf A}$.

A polymorphism of $(\mathbf A,\mathbf B)$ of arity $L$ is $f:A^L\to B$ such that for every $R$ and every $L\times\mathrm{ar}(R)$ matrix whose rows lie in $R^{\mathbf A}$, applying $f$ to each column gives a tuple in $R^{\mathbf B}$. It is symmetric if it is invariant under all permutations of its $L$ arguments.

The Basic LP $\mathrm{LP}_{\mathbb Q}(X,\mathbf A)$ has rational unknowns $w_i(a)\ge0$, a distribution on $A$ for each variable, and $p_j(y)\ge0$, a distribution on $R_j^{\mathbf A}$ for each constraint, linked by the marginal conditions $\sum_{y:\,y_k=a}p_j(y)=w_i(a)$ when $x_i$ is the $k$-th variable of $\bar x_j$. The affine relaxation $\mathrm{Aff}_{\mathbb Z}(X,\mathbf A)$ is the same system of equations in integer unknowns $r_i(a)$, $q_j(y)$, with no sign constraints.

The BLP+Affine algorithm (Figure 1) finds a relative interior point $(w,p)$ of $\mathrm{LP}_{\mathbb Q}(X,\mathbf A)$, rejecting if there is none; restricts the affine system to $\mathrm{Aff}'_{\mathbb Z}(X,\mathbf A)$ by forcing $r_i(a)=0$ wherever $w_i(a)=0$ and $q_j(y)=0$ wherever $p_j(y)=0$; and accepts if and only if the restricted system has an integer solution. It correctly solves $\mathrm{PCSP\text{-}Decision}(\mathbf A,\mathbf B)$ (Definition 1) if it accepts every instance satisfiable in $\mathbf A$ and rejects every instance unsatisfiable in $\mathbf B$.

Formalization targets

Goal: Theorem 2 (p. 6)

$$\Bigl(\forall N\ \exists L\ge N\ \exists f:A^L\to B \text{ symmetric polymorphism of } (\mathbf A,\mathbf B)\Bigr)\ \Longrightarrow\ \text{BLP+Affine correctly solves } \mathrm{PCSP\text{-}Decision}(\mathbf A,\mathbf B).$$

The hypothesis is a property of the template alone; the conclusion quantifies over all instances.

Milestones, in attack order

1. Footnote 1 (p. 5): a feasible $\mathrm{LP}_{\mathbb Q}(X,\mathbf A)$ has a solution of maximal support.
2. Completeness (p. 6): an instance satisfiable in $\mathbf A$ is accepted.
3. Rounding of variables (pp. 6–7): $W_i(a)=u\ell w_i(a)+v r_i(a)$ are non-negative integers with $\sum_a W_i(a)=L$, for $L=u\ell+v\ge M\ell^2$, $0\le v<\ell$.
4. Rounding of constraints (p. 7): $P_j(y)=u\ell p_j(y)+v q_j(y)$ are non-negative integers with $\sum_y P_j(y)=L$.
5. Eq. (9) (p. 7): $W_i(a)=\sum_{y:\,y|i=a}P_j(y)$.
6. Satisfying assignment (p. 7): $X_i:=f(a,\dots,a\ [W_i(a)\text{ times}])$ satisfies $X$ in $\mathbf B$.

Companion: Theorem 3 (p. 8)

The same conclusion when $\mathrm{Pol}(\mathbf A,\mathbf B)$ contains block-symmetric polymorphisms of arbitrarily large width: $[L]$ is split into blocks, each of size at least $N$, within which $f$ is invariant.

Significance

Theorem 2 gives one algorithm that decides every PCSP with an infinite family of symmetric polymorphisms, without knowing or evaluating the polymorphisms; it subsumes the BLP-then-AIP algorithm of Brakensiek and Guruswami for Boolean templates and applies over any finite domain. Theorem 3 extends this to block-symmetric families, which covers nearly all known tractable Boolean PCSPs, including 1-in-3-SAT versus NAE-SAT, whose alternating threshold polymorphisms are block-symmetric but not symmetric.

The results are proved in the paper. No machine-checked formalization of PCSPs, polymorphisms or the Basic LP is known to exist; Mathlib has no theory of constraint satisfaction. This mission produces a formal model of promise templates, instances, polymorphisms, the two relaxations and the algorithm's acceptance condition, together with a formal proof of the correctness theorem. The same model is the starting point for the characterization theorem (Theorem 4) treated in the companion mission.

Difficulty

Completeness is routine. Soundness is the substance: from a rational LP solution and an integer solution of the refined affine system one must produce an actual assignment in $\mathbf B$, using a polymorphism whose arity is chosen only after the instance is known. The natural first idea, clearing denominators of the LP solution and feeding the resulting multiplicities to a polymorphism, needs a polymorphism of exactly the arity the denominators dictate; with polymorphisms of only some arities it fails, and the paper's introduction notes that the LP alone does not suffice there. An integer affine solution, on the other hand, may have negative entries, which are not multiplicities. The paper stresses that the affine system must be the one refined by the support of a relative interior point: an arbitrary solution of the unrefined lattice gives no control on where the negative entries sit. In the formalization, the counting step (the columns of the matrix built from the constraint multiplicities have the variable multiplicities) and the passage from equal multiplicities to equal values of a symmetric function require explicit combinatorics on finite tuples, and the existence of a maximal-support LP solution requires an averaging argument over the finite set of coordinates.

Formalization scope

All declarations are in the namespace PCSPBLPAff.Symmetric. Conventions:

• Domains are Lean types with Fintype and DecidableEq; variables are Fin n, constraints Fin m, and a constraint's scope is a function Fin (ar R_j) → Fin n, possibly repeating variables.
• Arities are any natural numbers (the page asks for positive arities; every statement remains true for arity 0).
• The LP is over $\mathbb Q$ and the affine system over $\mathbb Z$. The weights $p_j$, $q_j$ are total functions on $A^{\mathrm{ar}(R_j)}$ required to vanish off $R_j^{\mathbf A}$.
• The marginal conditions (5) and (8) are imposed per position of the scope.
• The relative interior point is encoded by its only property the algorithm uses (footnote 1): a solution whose support contains the support of every solution. Acceptance requires such a solution and an affine solution vanishing outside its support.
• A block-symmetric function of width at least $N$ has at least one block, each block of size at least $N$.
• The polynomial-time claims of the paper, and the Remark on $\mathbb Z[\sqrt2]$, are out of scope: the algorithm is formalized by its acceptance condition.

The acceptance condition must not be replaced by "the LP is feasible and $\mathrm{Aff}_{\mathbb Z}(X,\mathbf A)$ has a solution", nor by an affine solution vanishing outside the support of an arbitrary LP solution; the first is a different algorithm and the second bypasses footnote 1.

Contributions welcome: proofs of the milestones, in particular the combinatorial lemma that a symmetric function takes the same value on tuples with the same multiplicities, and the averaging argument for maximal-support solutions; the block-wise version for Theorem 3.

Selected references

• J. Brakensiek, V. Guruswami, M. Wrochna, S. Živný, The Power of the Combined Basic Linear Programming and Affine Relaxation for Promise Constraint Satisfaction Problems, SIAM J. Comput. 49(6), 2020; arXiv:1907.04383v3. https://arxiv.org/abs/1907.04383v3
• J. Brakensiek, V. Guruswami, An Algorithmic Blend of LPs and Ring Equations for Promise CSPs, SODA 2019. https://arxiv.org/abs/1807.05194
• J. Brakensiek, V. Guruswami, Promise Constraint Satisfaction: Structure Theory and a Symmetric Boolean Dichotomy, SODA 2018. https://arxiv.org/abs/1704.01937
• L. Barto, J. Bulín, A. Krokhin, J. Opršal, Algebraic Approach to Promise Constraint Satisfaction, J. ACM 68(4), 2021. https://arxiv.org/abs/1811.00970

Motivation

For a real symmetric matrix, the largest eigenvalue is the maximum of the quadratic form $\mathbf x^\top A\mathbf x$ on the unit sphere, and it is computable to any accuracy in polynomial time. Tensor eigenvalues, introduced independently by Lim (2005) and Qi (2005), extend this picture to higher order: they are the stationary values of the cubic form $\mathcal A(\mathbf x,\mathbf x,\mathbf x)$ on the unit sphere. They appear in multilinear statistics, signal processing, hypergraph theory and polynomial optimization, and for these applications the symmetric case is the natural one.

Hillar and Lim, in Most Tensor Problems Are NP-Hard (J. ACM 2013), show that the eigenvalue problem stays NP-hard when the tensor is required to be symmetric (their Theorem 9.3). The proof is short once one ingredient is available: a theorem of Nesterov (2003), in a form corrected by Hillar and Lim, that expresses the stability number of a graph as the maximum of an explicit cubic polynomial over a sphere. This mission formalizes that chain.

Setting

Let $G=(V,E)$ be a simple graph on $V=\{1,\dots,v\}$, $v\ge1$. A set of vertices is stable if no two of its members are adjacent; the stability number $\alpha(G)$ is the size of a largest stable set, so $1\le\alpha(G)\le v$.

Put $n=v+v(v-1)/2$ and write a vector of $\mathbb R^n$ as $\mathbf z=(\mathbf x,\mathbf y)$, with $\mathbf x=(x_1,\dots,x_v)$ indexed by vertices and $\mathbf y=(y_{ij})_{i<j}$ indexed by pairs of vertices. The tensor $\mathcal S_G=[\![s_{abc}]\!]\in\mathbb R^{n\times n\times n}$ has entry $1$ at the six orderings of the triple of coordinates $(x_i,x_j,y_{ij})$ for every non-adjacent pair $i<j$, and $0$ elsewhere. It is symmetric: its entries do not change under any permutation of the three indices.

For a real 3-tensor $\mathcal A=[\![a_{abc}]\!]$ the cubic form is $\mathcal A(\mathbf z,\mathbf z,\mathbf z)=\sum_{a,b,c}a_{abc}z_az_bz_c$, and a real $\lambda$ is a unit $\ell^2$-eigenvalue of $\mathcal A$ if

$$\sum_{a,b}a_{abc}z_az_b=\lambda z_c\quad\text{for all }c,\qquad\text{for some }\mathbf z\text{ with }\|\mathbf z\|_2=1 .$$

Finally, $\lambda_l=2\sqrt{\tfrac23\left(1-\tfrac1l\right)}$ for $l\ge1$. In Lean these are TensorNP.SymEigen.stabTensor, cubicForm, IsUnitL2Eigenvalue and lambdaL, and $\alpha(G)$ is Mathlib's SimpleGraph.indepNum.

Formalization targets

Goal: Theorem 9.3, core

$$\alpha(G)=\max\{\,l\in\{1,\dots,v\}:\ \lambda_l\text{ is a unit }\ell^2\text{-eigenvalue of }\mathcal S_G\,\}.$$

That is, $\lambda_{\alpha(G)}$ is an eigenvalue of $\mathcal S_G$, and no $\lambda_l$ with $\alpha(G)<l\le v$ is. This is the statement on which the paper's $v$-query reduction rests; nothing is claimed about $l<\alpha(G)$.

Milestones, in the paper's order

1. Theorem 9.2 (Nesterov). With $\mathbb S^{n-1}=\{(\mathbf x,\mathbf y):\|\mathbf x\|_2^2+\|\mathbf y\|_2^2=1\}$,

$$\sqrt{1-\frac1{\alpha(G)}}=3\sqrt{\frac32}\cdot\max_{(\mathbf x,\mathbf y)\in\mathbb S^{n-1}}\ \sum_{i<j,\ \{i,j\}\notin E}x_ix_jy_{ij}.$$

2. The tensor. $\mathcal S_G$ is symmetric and $\mathcal S_G(\mathbf z,\mathbf z,\mathbf z)=6\sum_{i<j,\{i,j\}\notin E}x_ix_jy_{ij}$.
3. The maximum is an eigenvalue. $\max_{\|\mathbf z\|_2=1}\mathcal S_G(\mathbf z,\mathbf z,\mathbf z)$ is attained and is a unit $\ell^2$-eigenvalue of $\mathcal S_G$.
4. Its value. $\max_{\|\mathbf z\|_2=1}\mathcal S_G(\mathbf z,\mathbf z,\mathbf z)=\lambda_{\alpha(G)}$.
5. Further result: Theorem 6.9 (Banach), (23). For every symmetric $\mathcal S\in\mathbb R^{n\times n\times n}$,

$$\sup_{\mathbf x,\mathbf y,\mathbf z\ne\mathbf 0}\frac{|\mathcal S(\mathbf x,\mathbf y,\mathbf z)|}{\|\mathbf x\|_2\|\mathbf y\|_2\|\mathbf z\|_2}=\sup_{\mathbf x\ne\mathbf 0}\frac{|\mathcal S(\mathbf x,\mathbf x,\mathbf x)|}{\|\mathbf x\|_2^3},$$

both sides finite. The paper uses it in §10 to transfer Theorem 9.3 to the spectral norm and the best rank-one approximation of symmetric tensors.

Significance

The result. Theorem 9.3 places symmetric tensor eigenvalue among the NP-hard problems of Hillar and Lim's Table I, and through Banach's theorem (Theorem 10.2 of the paper) the same holds for the largest singular value, the spectral norm and the best rank-one approximation of a symmetric 3-tensor. These are the quantities computed by higher-order power methods and by moment-based estimators, so the result marks where the matrix theory stops transferring.

Formalizing it. All results here are proved in the literature; none is machine-checked. Nesterov's theorem, which rests on the Motzkin–Straus theorem for the complement graph, is not on the platform or in Mathlib, and its formal statement settles the constant that the original paper got wrong by a factor $1/\sqrt2$ (Hillar–Lim, footnote 12). Banach's theorem on symmetric multilinear forms is likewise absent from Mathlib and is useful well beyond this mission.

Difficulty

The tensor identity (milestone 2) is bookkeeping. The analytic content sits in two places. First, Nesterov's theorem: the obvious route, fixing $\mathbf x$ and maximizing over $\mathbf y$ by Cauchy–Schwarz, reduces the cubic problem to a quartic one in $\mathbf x$, whose value still has to be identified with $\alpha(G)$; that identification is the Motzkin–Straus theorem, which is not available in Lean and is itself a nontrivial optimization over the simplex. Second, the passage from a maximum to an eigenvalue needs a Lagrange multiplier argument on the sphere, and the symmetry of $\mathcal S_G$ is what makes the gradient of the cubic form match the eigen-equation. Part (b) of the goal needs a further, unprinted observation relating every unit eigenpair to the cubic form. Banach's theorem has no short proof; the classical arguments go through polarization estimates or a variational argument specific to symmetric forms.

Formalization scope

• Tensors and indices. A 3-tensor is a function ι → ι → ι → ℝ on a finite index type. For $\mathcal S_G$ the index type is the disjoint union of the vertices Fin v and the pairs $\{(i,j): i<j\}$; this is $\mathbb R^n$ with coordinates labelled by name instead of by the paper's enumeration $\varphi(i,j)=(i-1)v-i(i-1)/2+j-i$. Vertices are $0,\dots,v-1$.
• Normalization. Eigenvalues are taken with a unit eigenvector. The paper's Problem 9.1 and Definition 5.1 say only $\mathbf x\ne\mathbf 0$; since $(\lambda,\mathbf x)\mapsto(t\lambda,t\mathbf x)$ preserves the eigen-equation, that reading would make every nonzero real an eigenvalue of $\mathcal S_G$ and the goal false. The unit sphere (13) is where the paper derives the notion.
• Explicit readings. The paper's index range "$1\le i<j<k\le v$" in the definition of $s_{ijk}$ is read as $k\le n$ (taken literally it gives $\mathcal S_G=0$). Every "max" is stated as a greatest element, so attainment is claimed. In (23) the suprema are real suprema over nonzero vectors with boundedness part of the conclusion. $v\ge1$ is assumed wherever the paper uses $\alpha(G)\in\{1,\dots,v\}$.
• Not formalized. The oracle procedure of the proof of Theorem 9.3, the polynomial size of $\mathcal S_G$, the input model of Problem 9.1 with quadratic irrationalities (Remark 9.4), and the NP-completeness of the stability number (Karp 1972, via $\alpha(G)=\omega(\overline G)$). The goal is the mathematical core of the Turing reduction, not a complexity statement.
• Trivializations ruled out. Without the unit normalization the eigenvalue statements are trivial or false; a goal stating only (a), or only an inequality between the maximum and $\lambda_{\alpha(G)}$, would not determine $\alpha(G)$; both are excluded by the statements above.
• Infrastructure. Everything rests on Mathlib (SimpleGraph.indepNum, real analysis on finite-dimensional spaces, Lagrange multipliers). A Motzkin–Straus theorem for SimpleGraph and Banach's theorem for symmetric trilinear forms are both reusable beyond this mission; contributions of either, or of a general "maximum of a symmetric cubic form on the sphere is an eigenvalue" lemma, are welcome.

Selected references

• C. J. Hillar, L.-H. Lim, Most Tensor Problems Are NP-Hard, Journal of the ACM 60(6), Article 45, 2013. https://doi.org/10.1145/2512329 (arXiv:0911.1393v5: https://arxiv.org/abs/0911.1393)
• Yu. Nesterov, Random walk in a simplex and quadratic optimization over convex polytopes, CORE Discussion Paper 2003/71, 2003. http://edoc.bib.ucl.ac.be:83/archive/00000238/01/dp2003-71.pdf
• E. de Klerk, The complexity of optimizing over a simplex, hypercube or sphere: a short survey, Central European Journal of Operations Research 16, 111–125, 2008. https://doi.org/10.1007/s10100-007-0052-9
• T. S. Motzkin, E. G. Straus, Maxima for graphs and a new proof of a theorem of Turán, Canadian Journal of Mathematics 17, 533–540, 1965. https://doi.org/10.4153/CJM-1965-053-6
• S. Banach, Über homogene Polynome in ($L^2$), Studia Mathematica 7(1), 36–44, 1938 (reference [Banach 1938] of Hillar–Lim).
• L.-H. Lim, Singular values and eigenvalues of tensors: a variational approach, Proc. IEEE CAMSAP 1, 129–132, 2005. https://arxiv.org/abs/math/0607648
• L. Qi, Eigenvalues of a real supersymmetric tensor, Journal of Symbolic Computation 40, 1302–1324, 2005. https://doi.org/10.1016/j.jsc.2005.05.007
• R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, 85–103, 1972. https://doi.org/10.1007/978-1-4684-2001-2_9

Motivation

The spectral norm of a matrix, its largest singular value, is computable in polynomial time to any accuracy. Its analogue for 3-tensors appears in the analysis of multilinear systems, in the best rank-1 approximation of a data array, in quantum information (the geometric measure of entanglement), and in the injective norm of tensor products. Hillar and Lim, Most Tensor Problems Are NP-Hard (J. ACM 60(6), 2013, Article 45; final version arXiv:0911.1393v5), show that, in contrast with matrices, deciding whether a fixed nonzero rational number is a singular value or the spectral norm of a rational 3-tensor is NP-hard (their Theorems 6.5 and 1.10).

The proof is a reduction from the clique number $\omega(G)$ of a graph. It combines three classical ingredients: the theorem of Motzkin and Straus (1965), which expresses $\omega(G)$ as the value of a quadratic program over the simplex; a theorem of Banach (1938) on the spectral norm of symmetric tensors; and an observation from He, Li and Zhang (2010) on maxima of sums of squared bilinear forms. Deciding $\omega(G)\ge l$ is one of Karp's (1972) NP-complete problems.

Setting

A real 3-tensor is an array $\mathcal A=[\![a_{ijk}]\!]\in\mathbb R^{l\times m\times n}$ with trilinear form $\mathcal A(\mathbf x,\mathbf y,\mathbf z)=\sum_{i,j,k}a_{ijk}x_iy_jz_k$. With the Euclidean norm $\|\cdot\|_2$, its spectral norm is

$$\|\mathcal A\|_{2,2,2}=\sup_{\mathbf x,\mathbf y,\mathbf z\ne\mathbf 0}\frac{|\mathcal A(\mathbf x,\mathbf y,\mathbf z)|}{\|\mathbf x\|_2\|\mathbf y\|_2\|\mathbf z\|_2}.$$

A real $\sigma$ is a unit $\ell^2$-singular value of $\mathcal A$ if there are unit vectors $\mathbf u,\mathbf v,\mathbf w$ with

$$\textstyle\sum_{j,k}a_{ijk}v_jw_k=\sigma u_i,\quad \sum_{i,k}a_{ijk}u_iw_k=\sigma v_j,\quad \sum_{i,j}a_{ijk}u_iv_j=\sigma w_k$$

for all $i,j,k$: the stationarity conditions of $\mathcal A(\mathbf u,\mathbf v,\mathbf w)$ on a product of unit spheres.

Let $G=(V,E)$ be a simple graph on $V=\{1,\dots,v\}$, $v\ge1$, with $e$ edges $\{i_k,j_k\}$, $k=1,\dots,e$, and clique number $\omega$. Let $\Delta_v$ be the standard simplex, $A_G$ the adjacency matrix and $J$ the all-ones matrix. For a positive integer $l$ set $Q_l=A_G+\frac1lJ$ and $M_l=\max_{\mathbf x\in\Delta_v}\mathbf x^\top Q_l\mathbf x$. Let $E_k=\frac12E_{i_kj_k}+\frac12E_{j_ki_k}$, and let $T_l$ be the maximum over unit $\mathbf u,\mathbf v\in\mathbb R^v$, $\mathbf w\in\mathbb R^{l+2e}$ of the multilinear form

$$\sum_{i=1}^l\Big(\mathbf u^\top\tfrac1lI\mathbf v\Big)w_i+\sum_{k=1}^e(\mathbf u^\top E_k\mathbf v)w_{l+k}+\sum_{k=1}^e(\mathbf u^\top E_k\mathbf v)w_{e+l+k}. \tag{26}$$

The graph tensor $\mathcal A_l\in\mathbb Q^{v\times v\times(l+2e)}$ has as entry $a_{ijk}$ the coefficient of $u_iv_jw_k$ in (26).

Formalization targets

Goal: Theorems 6.5 and 1.10, encoding-free core

For every graph $G$ on $v\ge1$ vertices and every enumeration of its edges:

$$\forall l\ge1:\ \|\mathcal A_l\|_{2,2,2}=1\iff l=\omega;\qquad 1\text{ is a unit singular value of }\mathcal A_\omega;\qquad \forall l>\omega:\ 1\text{ is not one of }\mathcal A_l,$$

so $\omega$ is the largest $l\in\{1,\dots,v\}$ for which $1$ is a unit singular value of $\mathcal A_l$. The paper's $v$-query Turing reductions rest on exactly this.

Milestones (in attack order)

1. Theorem 6.7 (Motzkin–Straus): $1-1/\omega=2\max_{\mathbf x\in\Delta_v}\sum_{\{i,j\}\in E}x_ix_j$.
2. (22): $M_l=1+\frac{\omega-l}{l\omega}$; so $M_\omega=1$, $M_l>1$ for $l<\omega$, $M_l<1$ for $l>\omega$.
3. Lemma 6.8: $M_l=N_l$, where $N_l=\max_{\|\mathbf u\|_2=1}\{\sum_{i=1}^l(\mathbf u^\top\frac1lI\mathbf u)^2+2\sum_k(\mathbf u^\top E_k\mathbf u)^2\}$.
4. Theorem 6.9 (Banach), (24): for a symmetric 4-tensor, $\|\mathcal S\|_{2,2,2,2}=\sup_{\mathbf x\neq\mathbf 0}|\mathcal S(\mathbf x,\mathbf x,\mathbf x,\mathbf x)|/\|\mathbf x\|_2^4$.
5. Proposition 6.10 (He–Li–Zhang): for symmetric $A_k$, $\max_{\|\mathbf u\|=\|\mathbf v\|=1}\sum_k(\mathbf u^\top A_k\mathbf v)^2=\max_{\|\mathbf v\|=1}\sum_k(\mathbf v^\top A_k\mathbf v)^2$.
6. Lemma 6.11: $T_l=M_l^{1/2}$, hence $T_l=1$ iff $l=\omega$, $T_l>1$ iff $l<\omega$, $T_l<1$ iff $l>\omega$.
7. Proof of Theorem 6.5: $\|\mathcal A_l\|_{2,2,2}=T_l$, $T_l$ is a unit singular value of $\mathcal A_l$, and every unit singular value has absolute value at most $T_l$.
8. §7 (content of Theorem 1.13): $\min_{\sigma\ge0,\ \text{unit }\mathbf u,\mathbf v,\mathbf w}\|\mathcal A-\sigma\,\mathbf u\otimes\mathbf v\otimes\mathbf w\|_F^2=\|\mathcal A\|_F^2-\|\mathcal A\|_{2,2,2}^2$, attained only with $\sigma=\|\mathcal A\|_{2,2,2}$.

Significance

The result. The goal shows that a single comparison with $1$ of the spectral norm, or of the singular-value spectrum, of an explicit rational tensor of size $v\times v\times(l+2e)$ encodes whether $l=\omega(G)$. It is the step that makes the spectral norm, the largest singular value, and (through §7) the best rank-1 approximation of a 3-tensor NP-hard, whereas all three are polynomial-time for matrices. It explains why the higher-order power method and its relatives carry no global guarantees, and it is the starting point for inapproximability results such as the paper's Theorem 1.11.

Formalizing it. The results are proved on paper; none of them is formalized. Motzkin–Straus, Banach's polarization theorem for symmetric 4-tensors, and the He–Li–Zhang identity are classical results that are not in Mathlib and not on the platform; each is reusable well beyond this mission (Turán-type bounds, polynomial optimization over spheres, injective norms). The mission also checks the paper's construction at the level of indices and constants.

Difficulty

The construction of $\mathcal A_l$ is explicit, and the comparison with $1$ is arithmetic once $T_l=M_l^{1/2}$ is known. Everything rests on the three cited theorems. Motzkin–Straus is an optimization statement over the simplex whose maximizers may lie on the boundary and need not be unique, so a first-order computation at an interior critical point does not settle it. Banach's theorem asserts equality, not equality up to a constant: the standard polarization identity bounds the 4-linear form by its diagonal values only up to a factor. Proposition 6.10 is where the paper's own argument is loose: the 4-linear form it introduces is not symmetric, so (24) does not apply as printed. Finally, the singular-value clauses require that the maximum of a trilinear form on a product of spheres is a stationary value. This must be proved, not assumed.

Formalization scope

Tensors are arrays Fin l → Fin m → Fin n → ℝ with 0-based indices: the paper's $a_{ijk}$ is A (i-1) (j-1) (k-1). The Euclidean norm is Real.sqrt (∑ i, x i ^ 2). Suprema and maxima are sSup of sets that are nonempty and bounded under the stated hypotheses; where the paper's "max" carries content (Motzkin–Straus, (22), §7), attainment is stated with IsGreatest/IsLeast. The graph is a SimpleGraph (Fin v) with $v\ge1$, clique number Mathlib's SimpleGraph.cliqueNum, and its edges are enumerated by an arbitrary Fin e ≃ G.edgeSet. Every statement holds for each enumeration, so the tensor depends on the choice and the conclusions do not. $\mathcal A_l$ is a rational tensor, read over $\mathbb R$ by casting.

Explicit readings of the paper:

• Definition 6.1 has no norm constraint. Since $(\sigma,\mathbf u,\mathbf v,\mathbf w)\mapsto(t\sigma,t\mathbf u,t\mathbf v,t\mathbf w)$ preserves (20), unnormalized singular values make every nonzero real a singular value of $\mathcal A_l$, so the clause "not for $l>\omega$" would be false. Singular vectors are therefore unit vectors, as in the paper's derivation on p. 0:21.
• The statement of Lemma 6.11 prints $w_{m+l+k}$. There is no $m$ in §6, and the proof uses $w_{e+l+k}$, which is formalized.
• $E_k$ is written entrywise as $\frac12[\{i,j\}=\{i_k,j_k\}]$, which equals $\frac12E_{i_kj_k}+\frac12E_{j_ki_k}$ for a loopless edge.
• "$T_l$ is just the maximum $\ell^2$-singular value of $\mathcal A_l$" is made explicit as milestone 7.
• The goal does not claim that $1$ fails to be a singular value of $\mathcal A_l$ for $l<\omega$; the paper neither claims nor uses this.

This is the mathematical core of a polynomial-time Turing reduction, not an NP-hardness theorem. The polynomial size of $\mathcal A_l$, the $v$-query procedure, the scaling to a general fixed $0\ne\sigma\in\mathbb Q$, and the NP-completeness of CLIQUE (Karp 1972, cited) are not formalized. Theorem 1.11 and Corollary 1.12 are out of scope.

Two formalizations would make the goal trivial, and both are excluded. One is dropping the unit-norm constraint, which makes every nonzero number a singular value. The other is a spectral norm taken as a supremum over all vectors without normalization, which makes it unbounded and junk-valued; here the quotients are normalized.

Contributions are welcome on each milestone. Motzkin–Straus, Banach (24) and He–Li–Zhang are self-contained and reusable. Lemma 6.11 and milestone 7 need Cauchy–Schwarz and a Lagrange-type stationarity argument on spheres, which Mathlib supports through IsLocalExtrOn and the Lagrange multiplier files.

Selected references

• C. J. Hillar, L.-H. Lim, Most Tensor Problems Are NP-Hard, J. ACM 60(6), Article 45, 2013. https://doi.org/10.1145/2512329 (final version arXiv:0911.1393v5, https://arxiv.org/abs/0911.1393v5)
• T. S. Motzkin, E. G. Straus, Maxima for graphs and a new proof of a theorem of Turán, Canadian J. Math. 17, 533–540, 1965. https://doi.org/10.4153/CJM-1965-053-6
• S. Banach, Über homogene Polynome in (L²), Studia Math. 7, 36–44, 1938. https://doi.org/10.4064/sm-7-1-36-44
• S. He, Z. Li, S. Zhang, Approximation algorithms for homogeneous polynomial optimization with quadratic constraints, Math. Program. Ser. B 125(2), 353–383, 2010. https://doi.org/10.1007/s10107-010-0409-z
• R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 85–103, 1972. https://doi.org/10.1007/978-1-4684-2001-2_9

Motivation

In distributed computing, many graph problems (minimum spanning tree, shortest paths, connectivity checks) are solved by processors that sit at the vertices of the input network and communicate only along its edges. When every edge can carry only a few bits per round, the number of rounds an algorithm needs can be far larger than the network's diameter. Understanding by how much is the central question of the CONGEST (here: B) model of Peleg's monograph Distributed Computing: A Locality-Sensitive Approach (SIAM, 2000).

Das Sarma, Holzer, Kor, Korman, Nanongkai, Pandurangan, Peleg and Wattenhofer (SIAM J. Comput. 41 (2012) 1235–1265) proved round lower bounds for a long list of verification problems (is a given subgraph a spanning tree, a cut, a Hamiltonian cycle, …) and for approximating optimization problems such as the minimum spanning tree and shortest paths. Every one of those bounds goes through a single reduction, the Simulation Theorem (Theorem 3.1), which transfers lower bounds from two-party communication complexity to distributed algorithms.

Timeline:

• 2000: Peleg and Rubinovich (SIAM J. Comput. 30) prove an $\tilde\Omega(\sqrt n)$ lower bound for distributed MST construction on a family of graphs built from paths and a tree.
• 2006: Elkin (SIAM J. Comput. 36) extends it to MST approximation, using the networks $G(\Gamma,d,p)$ (reference [10] of the paper).
• 2011–2012: Das Sarma et al. isolate the Simulation Theorem as a general reduction for arbitrary Boolean functions $f$ and derive lower bounds for many verification and approximation problems.

Setting

A B-model network is an undirected graph whose vertices are processors with unbounded local computation. Computation proceeds in synchronous rounds; in each round, every vertex sends a message of $B$ bits along each incident edge in each direction, then updates its local state from its old state and the messages it received. Two vertices $s$ and $r$ hold inputs $x,y\in\{0,1\}^b$; all other vertices start without input. A public-coin randomized algorithm additionally lets all vertices read a shared random string. It computes $f:\{0,1\}^b\times\{0,1\}^b\to\{0,1\}$ with $\epsilon$-error in $T$ rounds if, for every $(x,y)$, both $s$ and $r$ output $f(x,y)$ after round $T$ with probability at least $1-\epsilon$. $R^{G}_\epsilon(f)$ is the least such $T$.

In the communication complexity model, Alice holds $x$, Bob holds $y$, one bit is sent per round, and both must output $f(x,y)$. $R^{cc-pub}_\epsilon(f)$ is the least number of bits of an $\epsilon$-error public-coin protocol.

The network $G(\Gamma,d,p)$ consists of $\Gamma$ paths $\mathcal P^1,\dots,\mathcal P^\Gamma$ with $d^p$ vertices $v^\ell_0,\dots,v^\ell_{d^p-1}$ each, a complete $d$-ary tree $\mathcal T$ of depth $p$ with vertices $u^\ell_0,\dots,u^\ell_{d^\ell-1}$ at level $\ell$, and spoke edges joining each leaf $u^p_j$ to $v^\ell_j$ on every path. The inputs sit at the two extreme leaves, $s=u^p_0$ and $r=u^p_{d^p-1}$. The $i$-right set $R_i$ consists of all path vertices at positions $j\ge i$, the leaves $u^p_j$ with $j\ge i$, and their ancestors; the $i$-left set $L_i$ is the mirror image, and $L_0=V\setminus\{r\}$, $R_0=V\setminus\{s\}$. $C_{R_t}$ denotes the vector of states of the vertices of $R_t$ at the end of round $t$.

Formalization targets

Goal: Theorem 3.1 (Simulation Theorem)

If a public-coin algorithm on $G(\Gamma,d,p)$ computes $f$ with $\epsilon$-error in $T$ rounds and

$$T<\frac{d^p-1}{2},$$

then some public-coin two-party protocol computes $f$ with $\epsilon$-error using at most

$$2\,d\,p\,B\,T\ \text{bits},\qquad\text{i.e.}\qquad R^{cc-pub}_\epsilon(f)\le 2dpB\,R^{G(\Gamma,d,p)}_\epsilon(f).$$

Milestones

1. Observation 3.3: the configuration of $U$ at round $t$ is determined by the configuration of $U'\supseteq U$ at round $t-1$ and the messages into $U$ from outside $U'$.
2. §3.3 edge count: for $0<t<(d^p-1)/2$, at most $dp$ edges join $V\setminus R_{t-1}$ to $R_t$ (and $V\setminus L_{t-1}$ to $L_t$).
3. Inclusion from the proof of Lemma 3.4: $V\setminus R_{t-1}\subseteq L_{t-1}$ (and its mirror image).
4. Lemma 3.4: $C_{R_t}=g_R(C_{R_{t-1}},M_1,\dots,M_{dp})$ for $dp$ messages of $B$ bits sent from $L_{t-1}$, with $g_R$ and the message edges fixed before the inputs; and symmetrically for $C_{L_t}$.

Significance

The theorem turns any lower bound $R^{cc-pub}_\epsilon(f)=\Omega(b)$, such as those for set disjointness and equality, into a round lower bound on $G(\Gamma,d,p)$: an algorithm with $T<(d^p-1)/2$ rounds forces $T\ge R^{cc-pub}_\epsilon(f)/(2dpB)$. Choosing the parameters gives the paper's bounds of order $\sqrt{n/(B\log n)}$ rounds for verification and approximation problems (§§4–7), and the same reduction underlies a large body of later CONGEST lower bounds.

The result has been proved since 2011. A machine-checked version would provide the first formal model of synchronous bandwidth-limited message passing and of public-coin two-party protocols on the platform, together with a verified reduction between them. No formalization of the theorem, of the B model, or of two-party communication protocols is known to exist in Mathlib or on the platform.

Difficulty

The informal proof is short; the work lies in making the information flow precise. The naive simulation, in which Alice simulates the vertices near $s$ and Bob those near $r$, fails because the cut between the two halves contains $\Gamma$ path edges plus the spokes, and $\Gamma$ can be large: sending every message across it costs $\Gamma B$ bits per round. The argument must instead let both parties' simulated regions shrink by one path position per round, so that the only messages crossing into Bob's region come from $p$ tree vertices with $d$ children each. Making this rigorous requires a careful accounting of which vertices belong to $R_t$, which edges leave $V\setminus R_{t-1}$, and why the functions that update the configurations do not depend on the other party's input.

Formalization scope

• Network. Vertices are (Fin Γ × Fin (d^p)) ⊕ Σ ℓ : Fin (p+1), Fin (d^ℓ); paths are numbered from $0$. The children of $u^\ell_i$ are $u^{\ell+1}_{di+k}$, $0\le k<d$. $L_i,R_i$ are Finsets defined for every $i$, with the paper's special case at $i=0$. The nodes $s,r$ require $d^p\ge1$.
• Messages are exactly $B$ bits (Fin B → Bool) on every directed edge in every round. Optional or variable-length messages would let silence carry information and make the theorem false (e.g. at $B=0$).
• Algorithms. Inputs enter only through the initial states of $s$ and $r$; a vertex receives a fixed dummy from non-neighbours. Running time is a fixed number $T$ of rounds, outputs read after round $T$; this is equivalent to the paper's worst-case time.
• Randomness is a PMF on an arbitrary type, shared by all vertices (resp. both parties); $\epsilon$-error requires both outputs to be correct on the same random string, and $\epsilon\ge0$.
• Protocols send one bit per round, so cost equals bits exchanged. Alice's moves read only $x$ and the transcript, Bob's only $y$. Modelling the two-party side as a two-vertex B-model network would carry two bits per round and weaken the constant $2dpB$ by a factor of $2$; the formalization does not do this.
• Lemma 3.4 is stated with the functions $g_L,g_R$ and the message edges chosen before the inputs. A version where they may depend on $(x,y)$ is trivially true and is ruled out.
• The "in other words" inequality between the minimal complexities is not posed through sInf, which would be $0$ on an empty set; the goal is stated for every algorithm.

Contributions welcome: proofs of the milestones, and reusable infrastructure for executions of message-passing algorithms (locality lemmas such as Observation 3.3 hold on any graph).

Selected references

• A. Das Sarma, S. Holzer, L. Kor, A. Korman, D. Nanongkai, G. Pandurangan, D. Peleg, R. Wattenhofer, Distributed Verification and Hardness of Distributed Approximation, SIAM J. Comput. 41(5), 2012, 1235–1265. https://doi.org/10.1137/11085178X
• M. Elkin, An Unconditional Lower Bound on the Time-Approximation Trade-off for the Distributed Minimum Spanning Tree Problem, SIAM J. Comput. 36(2), 2006, 433–456. https://doi.org/10.1137/S0097539704441848
• D. Peleg, V. Rubinovich, A Near-Tight Lower Bound on the Time Complexity of Distributed Minimum-Weight Spanning Tree Construction, SIAM J. Comput. 30(5), 2000, 1427–1442. https://doi.org/10.1137/S0097539700369740
• D. Peleg, Distributed Computing: A Locality-Sensitive Approach, SIAM, 2000. https://doi.org/10.1137/1.9780898719772
• E. Kushilevitz, N. Nisan, Communication Complexity, Cambridge University Press, 1997. https://doi.org/10.1017/CBO9780511574948

Motivation

A non-interactive zero-knowledge (NIZK) proof lets a prover convince a verifier that a statement is true by sending a single message, computed from a common reference string $\sigma$ that both parties share, without revealing anything beyond the truth of the statement. NIZK proofs were introduced by Blum, Feldman and Micali (STOC 1988) and are a building block of chosen-ciphertext secure encryption, signatures and secure multi-party computation. For a long time every NIZK proof for all of NP was zero-knowledge only computationally: a simulator produced proofs that no efficient adversary could tell apart from real ones.

Groth, Ostrovsky and Sahai (J. ACM 59(3), 2012; conference versions at Eurocrypt 2006 and Crypto 2006) gave the first NIZK argument for all of NP whose zero-knowledge is perfect: real and simulated proofs have exactly the same distribution, so even an unbounded adversary learns nothing. The construction is the Circuit SAT proof of their Figure 3, run on a perfectly hiding key of a homomorphic proof commitment scheme. Its zero-knowledge is Lemma 8 of the paper, and it is the zero-knowledge half of their Theorem 11.

Setting

A homomorphic proof commitment scheme has a message space $M$ (a finite cyclic group with generator $1$, here $\mathbb Z/N$), a randomizer space $R$ and a commitment space $C$, all finite abelian groups, and a commitment function $\mathrm{com}_{ck}(m; r)$. A hiding key generator $K_{\mathrm{hiding}}$ outputs a commitment key $ck$ together with a trapdoor $tk$. The scheme is assumed to have:

1. the homomorphic property, $\mathrm{com}(m_1+m_2; r_1+r_2) = \mathrm{com}(m_1; r_1)\,\mathrm{com}(m_2; r_2)$;
2. perfect trapdoor opening: $\mathrm{Topen}_{tk}(m_1, r_1, m_2)$ returns $r_2$ with $\mathrm{com}(m_2; r_2) = \mathrm{com}(m_1; r_1)$;
3. perfect trapdoor opening indistinguishability: for uniform $r_1$, the opening $\mathrm{Topen}_{tk}(m_1, r_1, m_2)$ is distributed, jointly with $ck$, as a fresh uniform randomizer;
4. perfect witness indistinguishability of a proof $P_{01}(ck, m, r; \rho)$ that a commitment contains $0$ or $1$: if $\mathrm{com}(0; r_0) = \mathrm{com}(1; r_1)$, the proofs made from $(0, r_0)$ and from $(1, r_1)$ have the same law.

A NAND circuit on $n$ wires is a list of gates $(i, j, k)$ and an output wire $\mathrm{out}$; a witness $w \in \{0,1\}^n$ satisfies it, $C(w) = 1$, if $w_k = \neg(w_i \wedge w_j)$ for every gate and $w_{\mathrm{out}} = 1$. The prover $P(\sigma, C, w)$ of Figure 3, with $\sigma = ck$, commits to every wire, $c_i = \mathrm{com}(w_i; r_i)$ with $c_{\mathrm{out}} = \mathrm{com}(1; 0)$, proves that each commitment contains $0$ or $1$, and for each gate proves that $c_i c_j c_k^2\,\mathrm{com}(-2; 0)$ contains $0$ or $1$.

The simulator is $S_1 = K_{\mathrm{hiding}}$, returning $\sigma = ck$ and $\tau = tk$, and $S_2(\sigma, \tau, C)$, which commits to $0$ on every wire except the output wire, and makes all the 0/1 proofs from openings it knows or obtains with the trapdoor. In the zero-knowledge game an adaptive adversary $A$ reads $\sigma$, submits pairs $(C, w)$ to an oracle one at a time, sees each answer before choosing the next, and outputs a bit. The real oracle answers with $P(\sigma, C, w)$, the simulation oracle with $S_2(\sigma, \tau, C)$; both answer failure when $C(w) \neq 1$.

Formalization targets

Goal: Lemma 8, perfect zero-knowledge

For every adaptive adversary $A$,

$$\Pr\big[\sigma \leftarrow S_\sigma : A^{P(\sigma,\cdot,\cdot)}(\sigma) = 1\big] = \Pr\big[(\sigma, \tau) \leftarrow S_1 : A^{S(\sigma,\tau,\cdot,\cdot)}(\sigma) = 1\big],$$

where $S_\sigma$ is $K_{\mathrm{hiding}}$ restricted to its first output.

Milestones, in the order the proof uses them

1. Gate witness (proof of Lemma 8, p. 15): with $c_i, c_j, c_k$ commitments to $0$ and $r'_k = \mathrm{Topen}_{tk}(0, r_k, 1)$,

$$c_i c_j c_k^2\,\mathrm{com}(-2; 0) = \mathrm{com}(0; r_i + r_j + 2r'_k).$$

2. Trapdoor-opened wires: $\mathrm{com}(w_i; \mathrm{Topen}_{tk}(0, r_i, w_i)) = \mathrm{com}(0; r_i)$, and the simulated commitments $(\mathrm{com}(0; r_i))_i$ have the law of the honest commitments $(\mathrm{com}(w_i; r_i))_i$.
3. Witness indistinguishability for two 0/1 openings: 0/1 proofs made from any two openings $(m, r)$, $(m', r')$ of the same commitment, $m, m' \in \{0,1\}$, have the same law.
4. One query: for every hiding key and every $(C, w)$ with $C(w) = 1$, $P(ck, C, w) \overset{d}{=} S_2(ck, tk, C)$.

Significance

Lemma 8 makes the Circuit SAT argument of Section 7 the first perfect NIZK argument for every language in NP. Combined with the computational indistinguishability of binding and hiding keys it also gives the computational zero-knowledge of the proof of Figure 3 (Theorem 6), and it is the template for the perfect zero-knowledge of the universally composable NIZK of the paper's Section 8. The same simulation pattern, commit to $0$ everywhere and use the trapdoor where an opening is needed, recurs in later pairing-based proof systems such as Groth–Sahai proofs.

The result is proved in the paper; to our knowledge it has not been machine-checked. A formal proof fixes the simulator completely, including the cases the paper leaves to the reader, and makes the adaptive multi-query argument explicit: the paper's proof treats one proof at a time and does not spell out why answering many adaptively chosen queries preserves equality of distributions.

Difficulty

The real and simulated proofs never use the same randomizers, so the proof cannot compare outputs value by value; it must compare laws. Two gaps in the printed argument need to be closed. First, witness indistinguishability is assumed only for one opening to $0$ against one opening to $1$, while comparing a simulated gate proof with a real one compares two openings that may carry the same message; the trapdoor supplies the missing intermediate opening. Second, the printed gate recipe gives the gate commitment the message $0$ only when no input of the gate is the output wire; when the output wire is an input, the message is $1$ or $2$, and $2$ has no 0/1 opening, so the simulator must open the gate commitment itself with the trapdoor. The adaptive adversary adds a third point: equality of laws must survive an arbitrary interaction in which later queries depend on earlier answers.

Formalization scope

• The message space is ZMod N with $N \ge 4$ (the paper describes Figure 3 for order at least 4, p. 14); $R$ and $R_{\mathrm{proof}}$ are finite nonempty types, $C$ a commutative group. Key generators and the 0/1 prover's randomness are probability mass functions; the coins are uniform.
• Probability-one properties are stated for every key in the support of $K_{\mathrm{hiding}}$; equalities of probabilities for all adversaries are stated as equalities of laws. Trapdoor opening indistinguishability is the joint law with $ck$, since the adversary does not see $tk$.
• The adversary is a well-founded tree of fair coin tosses and adaptive oracle queries that reads $\sigma$. Quantifying over all such trees is stronger than quantifying over polynomial-time adversaries. No running-time bound is imposed on the simulator.
• The simulator is the specific $S_2$ defined in the mission, a function of $ck$, $tk$, the circuit and fresh coins. A "simulator" that runs the honest prover on the witness would make the statement trivial and is ruled out by this definition. Each gate commitment is opened to $0$ with $\mathrm{Topen}_{tk}$, which covers the output-wire case.
• Out of scope: key indistinguishability and every computational statement (computational soundness of Theorem 11, adaptive culpable soundness, the UC results); the second sentence of Lemma 8 (perfect non-erasure zero-knowledge); the verifier of Figure 3, which zero-knowledge does not involve.
• Reusable beyond this mission: the query-tree adversary with its output law, and the abstract homomorphic proof commitment with its perfect properties. Contributions welcome: proofs of the milestones, and a general lemma that oracles with equal laws give equal output laws to every adaptive adversary.

Selected references

• J. Groth, R. Ostrovsky, A. Sahai, New Techniques for Noninteractive Zero-Knowledge, Journal of the ACM 59(3), Article 11, 2012. https://doi.org/10.1145/2220357.2220358
• J. Groth, R. Ostrovsky, A. Sahai, Perfect Non-interactive Zero Knowledge for NP, EUROCRYPT 2006, LNCS 4004. https://doi.org/10.1007/11761679_21
• J. Groth, R. Ostrovsky, A. Sahai, Non-interactive Zaps and New Techniques for NIZK, CRYPTO 2006, LNCS 4117. https://doi.org/10.1007/11818175_6
• M. Blum, P. Feldman, S. Micali, Non-Interactive Zero-Knowledge and Its Applications, STOC 1988. https://doi.org/10.1145/62212.62222
• U. Feige, D. Lapidot, A. Shamir, Multiple NonInteractive Zero Knowledge Proofs Under General Assumptions, SIAM J. Comput. 29(1), 1999. https://doi.org/10.1137/S0097539792230010
• J. Groth, A. Sahai, Efficient Non-interactive Proof Systems for Bilinear Groups, EUROCRYPT 2008, LNCS 4965. https://doi.org/10.1007/978-3-540-78967-3_24