Проверяемость расхождения с Тодой
Главный вывод сравнения — хищное правило оставляет больше классов, чем таблица Тоды 2003 года. Чтобы в этом не пришлось верить нашей программе, для пяти первых расхождений мы сделали доказательство, которое проверяется независимо.
Утверждение. Если применить хищное правило (стрелки $d_r\colon(n,s,c)\to(n-1,s+r,c+1)$, $r\ge2$, максимальный ранг на каждой странице) к настоящему листу $E^2$ метабиблиотеки, то над $\pi_n(S^2)$ остаётся
| n | правило (оба порядка заполнения) | Тода 2003 |
|---|---|---|
| 49 | 2 | 1 |
| 50 | 3 | 1 |
| 51 | 1 | 0 |
| 59 | 2 | 1 |
| 60 | 1 | 0 |
Значения Тоды не доказываются, а цитируются.
Как устроено
- Локальность. Правило проводит стрелки только между ненулевыми клетками $E^2$, поэтому идёт отдельно на каждой компоненте связности графа возможных стрелок. Для данных столбцов достаточно точных размерностей клеток этих компонент и того, что все соседние клетки и все прочие клетки столбцов нулевые: 89 клеток (100 блоков дифференциала) для $\pi_{49}$–$\pi_{51}$ и 86 клеток (111 блоков, самый большой — 308 910 × 269 346) для $\pi_{59}$–$\pi_{60}$.
- Сертификаты пишет программа, которой доверять не нужно.
- Ранг блока $\ge r$: векторы $y_1,\dots,y_r$ из слов-источников, у которых $d(y_i)$ имеют попарно разные старшие члены (матрица треугольная). Проверка — только вычисление $d$, без исключения Гаусса; в среднем 1,5 слова на вектор.
- Ненулевая клетка размерности $h$: $h$ циклов $z$ ($dz=0$) и $h$ коциклов $\varphi$ ($\varphi\circ d=0$) с обратимой матрицей $\varphi_j(z_i)$.
- Вместе с оценками рангов это даёт точную размерность каждой клетки.
- Проверялка написана заново по §2 статьи Иванова–Михайлова–Ву (соотношения, $\partial$, допустимость, перечисление слов) и не использует код, которым считался $E^2$. Она проверяет сертификаты, полноту набора клеток и сама прогоняет правило. Испорченный сертификат она отвергает (проверено четырьмя видами порчи).
- Lean 4 — третья независимая реализация алгебры и тех же проверок. Теорема о числе выживших классов доказывается
вычислением (
native_decide, то есть с доверием к компилятору Lean); неверное значение Lean отвергает.
Прогоны
| столбцы | генератор | проверялка (Python) | Lean |
|---|---|---|---|
| π49–π51 | 3 с | 34 с, 1,1 ГБ | 4,6 мин, 1,6 ГБ |
| π59–π60 | 72 с | 8 мин, 4,3 ГБ | 3 ч 28 мин, 7,7 ГБ |
Сертификаты занимают 1,5 и 19 МБ (сжатые).
Чего здесь нет
- Значения Тоды не проверяются.
- Что $E^2$ этого комплекса — $E^2$ спектральной последовательности из статьи, и что лямбда-алгебра задана формулами §2 верно, — математика статьи. Проверялки проверяют $d^2=0$ на малых клетках как тест соглашений.
- Само правило — наше прочтение лекции (дифференциалы).
- В Lean не доказано, что вычислительные проверки влекут утверждения линейной алгебры: Lean здесь — независимая программа с теоремой о результате её работы.
Код генератора, проверялки, Lean-проекта и сами сертификаты доступны по запросу.