For a finite module, the dimension is the least size of an ideal of definition, and such tuples are systems of parameters

Let $A:=R\mathrm{/}{\mathrm{Ann}}_R(M)$ and $\mathfrak{n}:=\mathfrak{m}\mathrm{/}{\mathrm{Ann}}_R(M)$. The ring $A$ is nonzero, Noetherian and local; $M$ is a faithful finite $A$-module. By [L5], ${\mathrm{Supp}}_A(M)=\mathrm{Spec}(A)$, and prime correspondence identifies this space with ${\mathrm{Supp}}_R(M)$, so $d=\dim A={\mathrm{ht}}_A(\mathfrak{n})$. The ideal $\mathfrak{n}$ has a finite generating list by [L3]; since it is maximal, it is minimal over its own generating ideal. Under the assumed AC, [L4] bounds its height by that list length. Thus $d<\mathrm{\infty }$ and [L1] applies to $A$.

A nonzero finite $A$-module $Q$ has finite length exactly when its support is $\{\mathfrak{n}\}$. In one direction, a finite composition series has simple factors $A\mathrm{/}\mathfrak{n}$: for a nonzero element of a simple factor, its annihilator is maximal, hence is the unique maximal ideal $\mathfrak{n}$. Thus ${\mathfrak{n}}^{s}Q=0$ for the series length $s$, and [L5] gives support contained in $\{\mathfrak{n}\}$; nonzero $Q$ has $\mathfrak{n}$ in its support by [L6]. Conversely, if support is $\{\mathfrak{n}\}$, [L5] gives $\sqrt{{\mathrm{Ann}}_A(Q)}=\mathfrak{n}$. Choose finite generators $t_1,\dots ,t_u$ of $\mathfrak{n}$ by [L3]. Each $t_i$ has a positive power annihilating $Q$, so some power ${\mathfrak{n}}^N$ annihilates $Q$. The finite filtration $Q\supseteq \mathfrak{n}Q\supseteq \cdots \supseteq {\mathfrak{n}}^{N}Q=0$ has finite $A\mathrm{/}\mathfrak{n}$-vector-space quotients: each ${\mathfrak{n}}^{i}Q$ is generated by products of finite generating lists for $\mathfrak{n}$ and $Q$. Refining each vector-space quotient by a basis flag gives a finite composition series.

Fix an ideal $J\subseteq \mathfrak{m}$ and put $Q=M\mathrm{/}JM$. By [L6], $Q\mathrm{\ne }0$. For each prime $\mathfrak{q}$ of $A$, if $JA⊈\mathfrak{q}$ then $Q_{\mathfrak{q}}=0$. If $JA\subseteq \mathfrak{q}$, then $M_{\mathfrak{q}}\mathrm{\ne }0$ by step 1.1 and $J{A}_{\mathfrak{q}}$ lies in the maximal ideal of the local ring $A_{\mathfrak{q}}$; [L6] applied there gives $Q_{\mathfrak{q}}\mathrm{\ne }0$. Hence ${\mathrm{Supp}}_A(Q)=V_A(JA)$. By [L5], this support is exactly $\{\mathfrak{n}\}$ if and only if $\sqrt{JA}=\mathfrak{n}$.

Combining steps 2.1 and 1.2, for ideals $J\subseteq \mathfrak{m}$ the quotient $M\mathrm{/}JM$ has finite length exactly when $\sqrt{JA}=\mathfrak{n}$. Applying [L1] in $A$, the least size of a generating tuple in $\mathfrak{n}$ with this property is $d$. Every such tuple in $A$ lifts to a tuple in $\mathfrak{m}$ because the quotient map $R\to A$ sends $\mathfrak{m}$ onto $\mathfrak{n}$; finite choices suffice. This proves part 1.

If $x_1,\dots ,x_d\in \mathfrak{m}$ satisfy that $M\mathrm{/}(x_1,\dots ,x_d)M$ has finite length, step 3.1 gives $\sqrt{(x_1,\dots ,x_d)A}=\mathfrak{n}$. Their images in $A$ therefore form a system of parameters by [L2]; this is the asserted module parameter condition. For $d=0$, the tuple is empty and the same argument says $M$ itself has finite length.

Steps 3.1 and 4.1 prove both claims.