I don't think $I_{\mathbb N}$ (which is often denoted something like $\operatorname{FSym}(\mathbb N)$) has the universal property you say. For example every finite group embeds into $\prod_{n=1}^\infty S_n$, but there is no injective homomorphism from $\operatorname{FSym}(\mathbb N)$ to $\prod_{n=1}^\infty S_n$.

Here is a self-contained argument getting roughly the same bound and related to OP's argument. Suppose $A^n \ne A^{n-1}$. Then there is some $g_0 \in A$ such that $g_0 A^{n-1} \ne A^{n-1}$. Let $g_1 \in A^{n-1} \setminus g_0 A^{n-1}$. Then $g_1A$ and $g_0A^{n-2}$ are disjoint subsets of $A^n$, so $|A^n| \ge |A| + |A^{n-2}|$.

Were paragraphs 4 and 7 accidentally separated from each other?

I guess you mean the sets $R^{-1}(y)$ form a $t$-design for any $t$, which does seem to follow from inclusion--exclusion. So yes I agree it seems there are no other examples.

Why do you say the sets $R(x)$ form a $t$-design? E.g., if $Y = X \times [2]$ with $x \in X$ joined to $(x,1)$ and $(x,2)$ for all $x$, then the $R(x)$'s are not a $2$-design.

I was just about to comment the same thing. Note that $k=1$ gives the matching example. One can also take $Y$ to be the disjoint union of any number of levels $[n]^{(k)}$ (including copies of the same level), so this includes the complete bipartite case too. This might be all examples?

for example if $R$ is a matching

It is easy to see that $|G| \ge |B(\ell/2)| \ge (2n-1)^{\ell/2}$ (this is essentially the Moore bound from graph theory).

Although the phrasing of the question in the last paragraph is odd and doesn't seem to reflect the intention of the previous paragraphs. $F_n$ Is "$\ell$-SRF" for all $\ell$, so $\ell(n) = \infty$ I guess. It makes more sense to ask for a bound for $|G|$ in terms of $\ell$ and $n$.

This is not exactly about quantitative residual finiteness in the usual sense (which is about bounding the index of a subgroup not containing one element of length $\ell$). Actually this question is about girth of Cayley graphs. The question is exactly asking how large $G$ must be if it has a Cayley graph on $n$ generators with girth at least $\ell+1$. Random Cayley graphs of $\mathrm{SL}_2(p)$ have girth $c \log p$.

I don't understand the final density calculation. If you have a union of arithmetic progressions containing $0$ with pairwise coprime common differences $d_1, \dots, d_k$ then it is true that their union has density $(1-1/d_1) \cdots (1-1/d_k)$, by CRT. The converse is true too: if the union has density given by the product then $d_1, \dots, d_k$ are pairwise coprime, and the integers $q(q-1)$ are not pairwise coprime!

@DavidESpeyer I believe $m(1,a_n,0)$ should be $m(1,0,a_n)$. Also $m_n^{a_n^2+1} = m(a_n^2+1, 0, a_n (a_n^2+1))$.

@DerekHolt But those subgroups don't have finite index