# (Very) effective bounds on Nullstellensatz proofs for injectivity

Given $$m$$ multilinear polynomials $$f_1,f_2,\ldots,f_m \in \mathbb{F}_2[x_1,x_2,\ldots,x_n]$$ of total degree at most $$2$$, I want to efficiently determine if the mapping $$\vec{x} \to (f_1(\vec{x}),f_2(\vec{x}),\ldots,f_m(\vec{x}))$$ is injective from $$\mathbb{F}_2^n$$ to $$\mathbb{F}_2^m$$. I want to do this by solving a system of linear equations, via the following approach.

It suffices to determine if the polynomial equations \begin{align*} \forall i, f_i(\vec{x}) - f_i(\vec{y}) &= 0 \\ \forall j, x_j^2 - x_j &= 0 \\ \forall j, y_j^2 - y_j &= 0 \\ \end{align*} imply $$x_k-y_k=0$$ for $$1 \leq k \leq n$$. By the Finite Field Nullstellensatz, this implication happens if and only if, for each $$k$$, there exist polynomials $$Q_{i,k},R_{j,k},S_{j,k}$$ where $$1 \leq i \leq m$$ and $$1 \leq j \leq n$$ such that $$$$x_k - y_k = \sum_{i=1}^n Q_{i,k}(\vec{x},\vec{y})(f_i(\vec{x}) - f_i(\vec{y})) + \sum_{j=1}^m R_{j,k}(\vec{x},\vec{y})(x_j^2-x_j) + \sum_{j=1}^m S_{j,k}(\hat{x},\hat{y})(y_j^2-y_j)$$$$

Are there any effective Nullstellensatz bounds that would give a strong conclusion for these structured systems? Doing experiments in Sage leads me to believe that the degrees of $$Q_{i,k}$$'s, $$R_{j,k}$$'s and $$S_{j,k}$$'s can be upper bounded by a constant; that constant might even be $$1$$.