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)