Results
The main statements of the draft with their status. Numbers refer to the version of the paper on this site;
a number opens the paper at the statement, and the links in the text lead to the computation, the code and data (commit
a3ce929), the Lean files and the open questions.
computer: checked by an exact computation (lattices modulo $p^E$ in Howell form, or the truncated
Magnus algebra, with the exactness certificate); paper: proved; Lean: formally verified.
| Status | Statement | Where |
|---|---|---|
| paper | Reduction: $D_5(G)\subseteq\gamma_4(G)$ for all groups $\iff$ $D_5(Q)=1$ for all finite $2$-groups of class $3$. For finite $G$ the order does not grow: $2$-groups up to the $2$-part of $|G|$ suffice. Proved in Lean with explicit hypotheses: the theorems of Passi ($D_4^2\subseteq\gamma_4$) and Gruenberg and $D_3=\gamma_3$ (for finite $G$ Gruenberg's theorem is not needed). | Prop. 2.1, Rem. 2.3; in Lean with hypotheses |
| Lean | For Lie rings $D_5(L)\subseteq\gamma_4(L)$ (Ionin, Mikhailov, Petrov, 2026); the formalization audited, the group question stated in Lean next to it. | §3, §4 |
| computer + paper | $D_5(G)\subseteq\gamma_4(G)$ for every finite $G$ with Sylow $2$-subgroup of order $\le2^{10}$, in particular for all groups of order $<2048$. | Thm. 5.4(1) |
| computer + paper | Order $2^{11}$, class $3$: $D_5=1$ for ranks $2$, $3$, $4$ and $\ge8$; ranks $5$–$7$ open. | Prop. 5.7, §5 |
| Lean | Central products: $D_n(H\circ E)=D_n(H)$ for $E\in\{D_8,Q_8\}$ and $t\in\gamma_2(H)$, and for $E=M_{2^{k+2}}$ under a condition on $g^{-2}s$ (e.g. $s=g^2$). All $386$ candidates of orders $2^6$–$2^9$ satisfy it, so splitting off $E\in\{D_8,Q_8,M_{16}\}$ gives no counterexample. Gluing along a proper subgroup of $Z(E)$ is closed when $\sigma=g^{2^{j+1}}$ (a central root of any degree; the rest is open); each of the $20$ split candidates has a splitting covered by Prop. 5.8. Prop. 5.8 and Lemma 5.9 are proved in Lean; the check of the candidates is by computer. | Prop. 5.8, Lemma 5.9 |
| computer | $D_n(G)=\gamma_n(G)$ for all $n$ and every finite group of order $<512$. | Thm. 5.4(2) |
| computer + paper | No $3$-torsion in $D_5(G)/\gamma_5(G)$ when the Sylow $3$-subgroup of $G$ has order $\le3^9$; $D_5=\gamma_5$ for all $3$-groups of order $\le3^9$. | Thm. 6.12 |
| Lean modulo Tahara | $D_5(G)=\gamma_5(G)$ whenever $G/\gamma_2(G)$ is finite of exponent $3$, of any rank and order. Proved in Lean with Tahara's Theorem 6.1 as an explicit hypothesis. | Thm. 6.6; Lean |
| Lean modulo Tahara | More generally: $D_5(G)=\gamma_5(G)$ whenever $G/\gamma_2(G)\cong C_{3^a}\times C_3^{s-1}$, i.e. it has at most one invariant larger than $3$ (including $C_9\times C_3^{s-1}$). Checked by an independent review; proved in Lean with Tahara's Theorem 6.1 as an explicit hypothesis. | Thm. 6.8; Lean |
| Lean | $p$ odd, $|\gamma_3/\gamma_4|=p$, $\gamma_2/\gamma_3$ with at most two generators $\Rightarrow$ $[\gamma_2,\gamma_2]\subseteq\gamma_5$. Hence a non-metabelian $p$-group of class $4$ and rank $d$ has order $\ge p^{d+5}$. | Lemma 6.3, Prop. 6.5; Lean |
| paper | $p$ odd, $P$ of class $3$ with $|\gamma_2/\gamma_3|=p^2$, $|\gamma_3|=p$ $\Rightarrow$ the $p$-covering group has $P^{*\prime\prime}=1$: all step-$1$ descendants are metabelian. | Thm. 6.10 |
| computer | Class-$3$ quotients of Rips-type groups of orders $2^{40}$–$2^{107}$: $D_5=1$ in all, $D_4\ne1$ in three of them (with the exactness certificate). | §7, question 1 |
| computer | The group analogue of Theorem C at $c=4$: the plateau group has $D_6\ne1$ but $D_7=1$, so $2c-2$ is attained and the analogue, if true, is sharp (an open question). | §7, question 3 |