Хронология

Что и когда сделано, от последнего к первому.

1. 18 октября 2026
   • На бумаге: $D_5=\gamma_5$, если у $Q/\gamma_2$ не больше одного инварианта больше $3$ (в том числе $C_9\times C_3^{s-1}$); независимая рецензия ошибок не нашла.
   • Литература: что на самом деле анонсировал Тахара (с. 173) и поиск его отдельной работы.
   • Проверка вычислением для $C_9\times C_3^{s-1}$ и $C_{27},C_{81}\times C_3^{s-1}$: $2\,057$ групп, $4\,537$ элементов $z$, ни один не лежит в $D_5$.
   • Аудит ANUPQ (ispacex.github.io/gap): шаг порождения для $3^9$ повторён на исправленной версии, результат совпал побайтно.
   • На бумаге: $D_n(H\circ E)=D_n(H)$ для центральных произведений с $D_8$, $Q_8$ и $M_{2^{k+2}}$ (присоединение центрального квадратного корня); у всех $386$ кандидатов порядков $2^6$–$2^9$ условия выполнены. Две независимые рецензии.
   • На бумаге: склейка по собственной подгруппе $Z(E)$ — лемма о центральном корне любой степени (лемма 5.9). Перебор разложений $386$ кандидатов: $20$ раскладываются, у каждого есть разложение, покрытое предложением 5.8. Независимая рецензия и пересчёт другим методом.
   • Lean: лемма 5.9 (центральный корень любой степени) доказана в Lean, без sorry, только стандартные аксиомы; начата формализация остальных результатов «на бумаге».
   • Lean: предложение 5.8 доказано в Lean во всех случаях ($D_8$, $Q_8$, $M_{2^{k+2}}$), вместе с кольцевым утверждением $\mathbb Z[H]\cap\Delta(Q)^n=\Delta(H)^n$; $Q_8$ и $M_{2^{k+2}}$ сводятся к $D_8$ через одну надгруппу $(Q\times\mathbb Z)/\langle(s,-2)\rangle$.
   • Lean: сведение (предложение 2.1, замечание 2.3) доказано по модулю явных гипотез — теорем Пасси, Грюнберга и $D_3=\gamma_3$: от ступени $\le3$ к конечно порождённым группам и к конечным $2$-группам ступени $3$; для конечных групп теорема Грюнберга не нужна.
   • Lean: лемма 6.3 и предложение 6.5 ($[\gamma_2,\gamma_2]\subseteq\gamma_5$; неметабелева $p$-группа ступени $4$ ранга $d$ имеет порядок $\ge p^{d+5}$) доказаны в Lean без гипотез; вместо кольца Ли — группа $G/\gamma_5$ и тождество Холла — Витта.
   • Lean: теоремы 6.6 и 6.8 ($D_5=\gamma_5$ при $G/\gamma_2\cong C_{3^a}\times C_3^{s-1}$) доказаны в Lean по модулю теоремы 6.1 Тахары, записанной явной гипотезой и сверенной со сканом; оба подслучая, включая строку $s$ условия (E).
2. 17 октября 2026
   • Групповой аналог теоремы C: у группы плато $D_7=1$; первый поиск при $c=4$; при $c=5$ $D_7\ne1$, но $D_8\cap\gamma_5=1$.
   • Порядок $3^8$: полный перебор, $904$ неметабелевы группы, у всех $D_5=1$.
   • Порядок $3^9$: фильтр по $p$-накрытию, $62\,245$ кандидатов, у всех $D_5=1$; ранг $5$ исключён на бумаге.
   • На бумаге: $D_5=\gamma_5$ при $Q/\gamma_2$ экспоненты $3$; лемма о кольцах Ли; $P^{*\prime\prime}=1$. Две независимые построчные рецензии.
3. 16 октября 2026
   • Порядок $2^{10}$ закрыт: лемма о минимальном контрпримере, ANUPQ, $3400$ кандидатов.
   • Отсечение без потерь в дереве $2$-групп для $2^{11}$; ранги $2$–$3$ и $\ge8$ закрыты.
   • $2^{11}$, ранг $4$: $52\,568$ кандидатов, у всех $D_4=D_5=1$.
4. 15 октября 2026
   • Точное вычисление $D_n$ для малых $p$-групп: все $2$-группы до $2^7$, $2^8$ ступени $\ge3$, метабелевы $2^9$ ступени $3$, $3$-группы до $3^6$.
   • Оценка Тахары сверена с оригиналом; нет $3$-кручения до $3^7$ (Гупта–Тахара).
   • Усечённая алгебра Магнуса: факторы групп рипсовского типа, $D_4\ne1$ при $2^{84}$, $2^{90}$, $2^{107}$ доказано, $D_5=1$.
5. 14 октября 2026
   • Проверена формализация Ионина–Михайлова–Петрова в Lean (сборка, аксиомы).
   • Размерные подгруппы групп в Lean: $\gamma_n\subseteq D_n$, $D_2=\gamma_2$, вопрос о $D_5$ сформулирован.
   • Черновик статьи: сведение к $2$-группам ступени $3$; где не переносится доказательство для колец Ли.