Результаты
Главные утверждения черновика с их статусом. Номера — по версии статьи на этом сайте;
ссылка на номер открывает статью на этом утверждении, ссылки в тексте ведут к вычислению, коду и данным (коммит
a3ce929), файлам Lean и открытым вопросам.
компьютер — проверено точным вычислением (решётки по модулю $p^E$ в форме Хауэлла или усечённая
алгебра Магнуса, с сертификатом точности); на бумаге — доказано; Lean — формально проверено.
| Статус | Утверждение | Где |
|---|---|---|
| на бумаге | Сведение: $D_5(G)\subseteq\gamma_4(G)$ для всех групп $\iff$ $D_5(Q)=1$ для всех конечных $2$-групп ступени $3$. Для конечных $G$ порядок не растёт: достаточно $2$-групп порядка не больше $2$-части $|G|$. В Lean доказано при явных гипотезах: теоремы Пасси ($D_4^2\subseteq\gamma_4$), Грюнберга и $D_3=\gamma_3$ (для конечных $G$ теорема Грюнберга не нужна). | Предл. 2.1, Зам. 2.3; в Lean при гипотезах |
| Lean | Для колец Ли $D_5(L)\subseteq\gamma_4(L)$ (Ионин, Михайлов, Петров, 2026); формализация проверена, групповой вопрос сформулирован в Lean рядом. | §3, §4 |
| компьютер + бумага | $D_5(G)\subseteq\gamma_4(G)$ для всякой конечной $G$ с силовской $2$-подгруппой порядка $\le2^{10}$, в частности для всех групп порядка $<2048$. | Теор. 5.4(1) |
| компьютер + бумага | Порядок $2^{11}$, ступень $3$: $D_5=1$ при рангах $2$, $3$, $4$ и $\ge8$; ранги $5$–$7$ открыты. | Предл. 5.7, §5 |
| Lean | Центральные произведения: $D_n(H\circ E)=D_n(H)$ при $E\in\{D_8,Q_8\}$ и $t\in\gamma_2(H)$, а для $E=M_{2^{k+2}}$ — при условии на $g^{-2}s$ (например, $s=g^2$). Все $386$ кандидатов порядков $2^6$–$2^9$ ему удовлетворяют, так что разложимость $H\circ E$ с $E\in\{D_8,Q_8,M_{16}\}$ контрпримера не даёт. Склейка по собственной подгруппе $Z(E)$ закрыта при $\sigma=g^{2^{j+1}}$ (центральный корень любой степени; остальное открыто); у каждого из $20$ раскладывающихся кандидатов есть разложение, покрытое предложением 5.8. Предложение 5.8 и лемма 5.9 доказаны в Lean; проверка кандидатов — вычислением. | Предл. 5.8, Лемма 5.9 |
| компьютер | $D_n(G)=\gamma_n(G)$ при всех $n$ для всякой конечной группы порядка $<512$. | Теор. 5.4(2) |
| компьютер + бумага | Нет $3$-кручения в $D_5(G)/\gamma_5(G)$, если силовская $3$-подгруппа $G$ имеет порядок $\le3^9$; $D_5=\gamma_5$ для всех $3$-групп порядка $\le3^9$. | Теор. 6.12 |
| Lean по модулю Тахары | $D_5(G)=\gamma_5(G)$, если $G/\gamma_2(G)$ конечна и имеет экспоненту $3$ — при любом ранге и порядке. В Lean доказано при теореме 6.1 Тахары как явной гипотезе. | Теор. 6.6; Lean |
| Lean по модулю Тахары | Более общо: $D_5(G)=\gamma_5(G)$, если $G/\gamma_2(G)\cong C_{3^a}\times C_3^{s-1}$, т.е. у неё не больше одного инварианта больше $3$ (в том числе $C_9\times C_3^{s-1}$). Проверено независимой рецензией; в Lean доказано при теореме 6.1 Тахары как явной гипотезе. | Теор. 6.8; Lean |
| Lean | $p$ нечётно, $|\gamma_3/\gamma_4|=p$, у $\gamma_2/\gamma_3$ не больше двух порождающих $\Rightarrow$ $[\gamma_2,\gamma_2]\subseteq\gamma_5$. Отсюда: неметабелева $p$-группа ступени $4$ ранга $d$ имеет порядок $\ge p^{d+5}$. | Лемма 6.3, Предл. 6.5; Lean |
| на бумаге | $p$ нечётно, $P$ ступени $3$ с $|\gamma_2/\gamma_3|=p^2$, $|\gamma_3|=p$ $\Rightarrow$ у $p$-накрывающей группы $P^{*\prime\prime}=1$: все шаг-$1$ потомки метабелевы. | Теор. 6.10 |
| компьютер | Факторы ступени $3$ групп рипсовского типа порядков $2^{40}$–$2^{107}$: везде $D_5=1$, в трёх из них $D_4\ne1$ (с сертификатом точности). | §7, вопрос 1 |
| компьютер | Групповой аналог теоремы C при $c=4$: у группы плато $D_6\ne1$, но $D_7=1$, так что $2c-2$ достигается и аналог, если верен, точен (открытый вопрос). | §7, вопрос 3 |