Путь Евклида

Одна невозможность — вечный двигатель Евклида, бесконечная строго убывающая цепь на вполне-упорядоченном ряду, которой не существует, — прочитана под восемью масками и целым арифметическим шлейфом. Одна программа, одна аксиома, машинная проверка в Lean 4.

Мы берём древнейший доказательный объект математики — бесконечный спуск Ферма, переписанный мультипликативно, — и показываем, что он запрещён строго и без всяких допущений. А затем читаем через этот единственный запрет одну задачу за другой: близнецы, Риман, P/NP, Янг–Миллс, Навье–Стокс, Ходж, Коллатц, Бёрч–Свиннертон-Дайер. Всюду «отклонение» от нормы оказывается замаскированным вечным двигателем — и запрет его убивает.

Ни одна задача тысячелетия здесь не решена. Доказано другое, и это, быть может, важнее: все они — одна задача.

Честность прежде всего

Программа держится на кардинальной дисциплине честности. Всё, что доказано машинно при стандартных аксиомах Lean/mathlib, помечено 🟢. Всё, что условно на единственную аксиому репозитория step00FirstCause (намеренное событие «0 → 1» с одной причинной границей — близнецы), помечено 🟡 — AXIOM-TAINTED, и верификатор пересчитывает каждую такую декларацию при каждой сборке. Всё открытое — 🔴.

Легенда статусов

• 🟢 — доказано машинно при стандартных аксиомах Lean/mathlib;
• 🟡 — AXIOM-TAINTED: условно на единственную аксиому step00FirstCause;
• 🔴 — открытый узел или именованный вход.

На момент сборки: ровно одна нестандартная аксиома, 16 зависящих от неё деклараций, один оставшийся sorry (сама цель twin_prime_conjecture). Утечек в зелёную линию нет — их отслеживает верификатор.

С чего начать

• Словарь программы — все ключевые понятия одним списком.
• Пролог и карта — что доказано, что декретировано, что открыто; карта всех частей.
• Двигатель Евклида (гл. 01) — сам запрет: почему вечного спуска не существует.
• Первопричина и главная теорема (гл. 33) — почему узел нельзя закрыть изнутри.
• Кода (гл. 50) — один запрет, семь масок, и пространство-время как его тень.

Приложения и поздние фронты

Дописаны, когда ядро уже сложилось, — расширения синтеза выше, и каждая стоит сама по себе:

• Численная опора (гл. 51) — числа и картинки за утверждениями.
• Дискретная модель жидкости (гл. 52) — Навье–Стокс, сведённый к диадическому скелету.
• Бёрч–Свиннертон-Дайер — восьмая маска (гл. 53) — тот же спуск на реальной эллиптической кривой.
• Соседи за горизонтом (гл. 54) — открытые арифметические задачи сразу за той же стеной.
• Коллатц (гл. 55) и Первопричина Коллатца (гл. 56) — проход по границе и декрет, снятый после машинного опровержения.

Исходники и машинная проверка — в репозитории на GitHub.

Двуязычие. Сайт готовится на двух языках — русском и английском. Русская версия — исходная; английский перевод появляется постранично, а до его готовности страница показывается по-русски.