A direct-sum theorem for the non-deterministic communication complexity of inequality?

Question

A non-deterministic protocol for the inequality function is a protocol that behaves as follows: Alice and Bob get strings $x,y\in\{0,1\}^n$ respectively, and an untrusted prover is trying to convince them that $x \ne y$ by sending them some proof string $\pi$. The protocol accepts if both Alice and Bob accept $\pi$, and rejects otherwise. The prover should succeed in making the protocol accept if and only if indeed $x \ne y$.

It is well-known that in every such protocol, the string $\pi$ must be of length at least $\log n$. The easiest way to see it is to observe that if this lower bound did not hold, then there would be a deterministic protocol for the equality function that transmits less than $n$ bits. This lower bound is tight, since the prover can choose $\pi$ to be a coordinate $i\in [n]$ suh that $x_i \ne y_i$.

My question is whether the non-deterministic complexity of solving $k$ independent instances of inequality is at least $k\cdot\log(n)$? In other words, is there a direct-sum theorem for the non-deterministic communication complexity of inequality?

Relevant work: Feder et. al. [FKNN95] proved a general direct-sum theorem for non-deterministic communication complexity. Unfortunately, this theorem only applies to functions whose complexity is $\gg log(n)$, and therefore does not apply to the inequality function. Karchmer et. al. [KKN95] gave an alternative proof for this theorem, which suffers from the same limitation.

References:

[FKNN95] Tomás Feder, Eyal Kushilevitz, Moni Naor, Noam Nisan, "Amortized Communication Complexity". SIAM J. Comput. 24(4): 736-750 (1995)

[KKN95] Mauricio Karchmer, Eyal Kushilevitz, Noam Nisan, "Fractional Covers and Communication Complexity". SIAM J. Discrete Math. 8(1): 76-92 (1995)

Answer 1

I think this can be done with $\log n \cdot\log t + t \cdot\log\log t$ bits of nondeterministic communication.

By encoding all strings with an error correcting code, we may assume that whenever we have an input pair $(x,y)$ with $x\neq y$ the two strings differ in a constant fraction of coordinates. Suppose we are given $t$ pairs $(x^j,y^j)_{j\in[t]}$ that we want to certify are all nonequal. By averaging, there is some coordinate $i\in[n]$ that witnesses $x^j_i\neq y^j_i$ for a constant fraction of $j\in[t]$. Iterating this argument we may construct a set $S\subseteq[n]$ of about $|S|=\log t$ coordinates such that for every $j$ there is some $i\in S$ such that $x^j_i\neq y^j_i$. The nondeterministic proof consists of $S$ (which is $\log t\cdot \log n$ bits) and a mapping $[t]\to S$ (which is $t\cdot\log\log t$ bits) that indicates which coordinate in $S$ to use for each of the $t$ input pairs.