The finite basis problem for matrix semirings $\mathbf{M}_n(S_7)$

We first prove an embedding theorem for matrix semirings $\mathbf{M}_n(S)$ over an additively idempotent semiring $S$: for all $n \geq 2$, $\mathbf{M}_n(S)$ embeds into $\mathbf{M}_{n+1}(S)$. This yields an ascending chain of varieties $\mathsf{V}(\mathbf{M}_2(S)) \leq \mathsf{V}(\mathbf{M}_3(S)) \leq \cdots$, which is strictly ascending when $S$ is the two-element distributive lattice. We then show that every variety in the interval $[\mathsf{V}(S_c(abc)), \mathsf{V}(\mathbf{M}_n(S_7))]$ is nonfinitely based (i.e., has no finite basis for its identities), where $S_c(abc)$ is an eight-element flat semiring and $S_7$ is the unique nonfinitely based three-element additively idempotent semiring. Consequently, $\mathbf{M}_n(S_7)$ is nonfinitely based, yielding an ascending chain $\mathsf{V}(\mathbf{M}_2(S_7)) \leq \mathsf{V}(\mathbf{M}_3(S_7)) \leq \cdots$; moreover, every variety in $[\mathsf{V}(S_7), \mathsf{V}(\mathbf{M}_n(S_7))]$ is also nonfinitely based, and this interval contains at least countably infinitely many distinct varieties. Although we do not know whether $\mathsf{V}(\mathbf{M}_n(S_7)) = \mathsf{V}(\mathbf{M}_{n+1}(S_7))$ holds, we show that the multiplicative reduct of $\mathbf{M}_n(S_7)$ without the constant matrix $[1]_n$ is $5$-nilpotent, which strongly suggests that the equality may indeed hold for all $n \geq 2$.