algebra precalculus - Conjecture about polynomials $f_ninmathbb Q[X_1,dots,X_n]$ defining bijections $mathbb N^ntomathbb N$

This is inspired by an answer of a question of mine:

Bijective polynomials $f\in\mathbb Q[X_1,\dots,X_n]$

There is a polynomial $f_1\in\mathbb Q[X_1]$ which define a bijection $f_1:\mathbb N\to\mathbb N$, $f_1(X_1)=X_1$.

There is a polynomial $f_2\in\mathbb Q[X_1,X_2]$ which define a bijection $f_2:\mathbb N^2\to\mathbb N$,

$\displaystyle f_2(X_1,X_2)=\frac{(X_1+X_2)(X_1+X_2+1)}{2}+f_1(X_1)$.

And as far as I understand and have tested there is a polynomial $f_3\in\mathbb Q[X_1,X_2,X_3]$ which define a bijection
$f_3:\mathbb N^3\to\mathbb N$

$\displaystyle f_3(X_1,X_2,X_3)=\frac{(X_1+X_2+X_3)(X_1+X_2+X_3+1)(X_1+X_2+X_3+2)}{6}+f_2(X_1,X_2)$.

This seems possible to generalize as

$\displaystyle f_{n+1}(X_1,\dots ,X_{n+1})=f_{n}(X_1,\dots ,X_{n})+\frac{1}{(n+1)!}\prod_{k=1}^{n+1}\Big(k-1+\sum_{i=1}^{n+1}X_i\Big)$.

This is a generalisation of the diagonalization in case of $n=2$ with "triangularization", "tetraederization" or higher. Now the conjecture is

$\displaystyle f_n(X_1,\dots,X_n)$ define a bijection $\mathbb N^n\to\mathbb N$ for all $n>0$.

Induction seems natural but how to prove that $f_n$ is a bijection implies that $f_{n+1}$ is a bijection?

What I want are proofs, parts of proofs or counter proofs.

Answer

The diagonalization argument can indeed be generalized. Roughly, one can see all elements of $\mathbb{N}$ appear in order by going through all hyperplanes $X_1+\ldots+X_n = s$.

Now for the proof. Let $s=X_1+...+X_n$. Then your function $f_n$ can be written as
$$ f_n(X_1, ..., X_n) = \binom{s+n-1}{n} + f_{n-1}(X_1, \ldots, X_{n-1}), $$
with the conventions that $f_n(0,\ldots, 0) = 0$ and $f_0 = 0$.

Claim: Fix $s\in \mathbb{N}$. Then $f_n$ induces a bijection
$$ \Big\{ (X_1, \ldots, X_n)\in \mathbb{N}^n \ | \ s=X_1+...+X_n \Big\} \xrightarrow{f_n} \Big[ \binom{s+n-1}{n}, \binom{s+n}{n} -1\Big], $$

where $[x,y]$ is the set of integers from $x$ to $y$, and if $s=0$, then the set on the right is $[0,0]$ by convention.

Proof of the claim. It is obviously true for $n=1$. Assume it is true for $n-1$. Let us show it is true for $n$.
For a fixed $s=X_1+...+X_n$, the value $t=X_1 + \ldots + X_{n-1}$ can be anything from $0$ to $s$, depending on the value of $X_n$. Thus, by the hypothesis on $f_{n-1}$, it induces a bijection
$$ \Big\{ (X_1, \ldots, X_n)\in \mathbb{N}^n \ | \ s=X_1+...+X_n \Big\} \xrightarrow{f_{n-1}} \Big[ 0, \binom{s+n-1}{n-1} -1\Big] $$
defined by $(X_1, \ldots, X_n) \mapsto f_{n-1}(X_1, \ldots, X_{n-1})$.
Thus $f_n$ induces a bijection from the set on the left to the interval $\Big[\binom{s+n-1}{n}, \binom{s+n-1}{n} + \binom{s+n-1}{n-1}-1\Big]$. Since $\binom{s+n-1}{n} + \binom{s+n-1}{n-1} = \binom{s+n}{n}$, the claim is proved.

The fact that $f_n$ is a bijection from $\mathbb{N}^n$ to $\mathbb{N}$ then follows immediately from the claim.