Словарь программы¶
Все ключевые понятия «Пути Евклида» в одном месте — коротко, с указанием главы, где понятие вводится по-настоящему. Главы напоминают термины при первом употреблении, но сюда можно возвращаться из любого места.
Машина и её законы¶
Вечный двигатель (Евклида) — бесконечная строго убывающая цепь на вполне-упорядоченном ряду;
главный запрещённый объект программы. Его не существует (no_infinite_descent) — это бесконечный
спуск Ферма, переписанный мультипликативно. Всё остальное — тени этого запрета. См. главу 01.
EPMI — ядро невозможности вечного двигателя (Engine Perpetual Motion Impossibility); доказано на голом ядре Lean, даже без mathlib. См. главу 01.
Ранг / lexRank — «высота» состояния: натуральное число, которое строго падает вдоль
разрешённых шагов. Конечность ранга — это «конечное топливо»: строгий спуск не может длиться вечно.
См. главы 01 и 24.
Двигатель как метод — контрапозиция через двигатель: чтобы доказать цель P, показываем
¬P ⟹ двигатель; двигателей нет — значит P. Общая стратегия всех ветвей. См. главу 00.
Пижонхол — принцип ящиков: конечный ключ не может инъективно пометить бесконечное семейство. Излюбленная форма противоречия в P/NP-ветви и эпистемике. См. главу 39.
Окно / бюджет окна — отрезок траектории длины k; бюджет окна — мультипликативная граница
на рост/спад значения за окно. Язык коллатцевской ветви. См. главу 55.
Дисциплина честности¶
🟢 / 🟡 / 🔴 — три статуса каждой декларации: 🟢 доказано машинно при стандартных аксиомах
Lean/mathlib; 🟡 AXIOM-TAINTED — условно на единственную аксиому step00FirstCause; 🔴 —
открытый узел или именованный вход. Легенда — в прологе.
Первопричина / step00FirstCause — единственная аксиома репозитория: намеренное событие
0 → 1 с одной причинной границей (близнецы; Риман и Навье–Стокс были отсоединены — Option A). Принимается извне, потому
что самозапуск изнутри стоил бы вечного двигателя. См. главу 33.
Граница (декрета) — содержательное поле первопричины: закон, принятый декретом под честно раскрытую цену. Границы падают от кованых опровержений — так пала четвёртая, коллатцевская. См. главы 33 и 56.
Декрет — намеренное принятие закона аксиомой (в отличие от доказательства). Честный декрет обязан пройти трилемму и раскрыть цену («декрет, возможно, переплачивает»).
Карантин — модуль Engine/CausalClosureAxiom.lean, единственное место, где живёт аксиома;
всё зависимое от неё машинно помечается.
Таинт / AXIOM-TAINTED — след аксиомы в списке зависимостей декларации. Верификатор
(scripts/VerifyAll.lean) пересчитывает заражённые декларации при каждой проверке; сейчас их 16,
и утечек в зелёную линию нет.
Растяжка — намеренный детектор взрыва: теорема вида «если закон границы опровергнут, False
выводится ровно здесь». Растяжки ставятся вместе с границей — и работают: коллатцевская сработала.
См. главу 56.
Трилемма — обязательная проверка кандидата в границы: универсальная форма не опровержима ли, экзистенциальная не доказана ли даром (вакуумность), не есть ли закон переименование цели. Провал любой ветви закрывает декретный путь. См. главы 39–42.
Кованое опровержение — машинно построенный контрпример к универсальной форме закона («ковка»). Наличие ковки означает: границу брать нельзя. Примеры: лестница Янг–Миллса, орбита 27 у Коллатца. См. главы 40 и 55.
Вакуумность — ситуация, когда кандидат-закон выполняется даром (свидетелем-заглушкой) и потому декретировать его бессмысленно: декрет был бы пуст. См. трилеммы глав 39–42.
Переименование цели — нечестная форма закона, равносильная самой цели без всяких гипотез;
машинно вскрывается iff-аудитом (образец — offCriticalBridge_iff_RH). Такой «закон»
декретировать нельзя: это не причина, а вывеска. См. главу 38.
Ex falso — вывод «из лжи что угодно»: теорема, чья сила — лишь в противоречивости посылки. Честность требует помечать такие маршруты и не выдавать их за содержательные.
Data-anchor (якорь в данных) — недостающий реальный объект (машина Тьюринга, оператор, аналитическое продолжение), без которого пропозициональный закон не привязан к настоящей задаче. Якоря именуются красными входами с раскрытием, что именно математика должна предъявить. См. главу 39.
Свидетели и манифестация¶
Свидетель — конкретный объект, удостоверяющий утверждение: пара близнецов, нуль вне прямой,
нечётное совершенное число. Проверить свидетеля обычно дёшево (иногда буквально decide);
предъявить — совсем другое дело.
Непредъявимый свидетель — свидетель, предъявление которого стоило бы вечного двигателя: опровержение «при законе и сведённых книгах» строит из него двигатель. Основание честных границ и фронтов-манифестаций. См. главу 43.
Свидетель-отсутствие — свидетель того, что выше порога объектов нет (например,
CousinAbsenceAbove); гейтирует законы манифестации в зоопарке. См. главу 44.
Манифестация / закон манифестации — принцип «отклонение обязано проявиться»: нуль вне прямой, нарушение Гольдбаха, отсутствие кузенов — каждый обязан оставить неоплатимый след (поставку) там, где книги сведены. См. главу 38.
Леджер / «книги сведены» — бухгалтерия потоков; «книги сведены» = проекция разрешает коллизии на данном масштабе (стабильная вселенная без свободной энергии). На сведённых книгах бесконечная поставка невозможна — из неё собирается двигатель. См. главу 24.
Поставка — бесконечная допустимая семья потоков/сертификатов: то, чем отклонение «расплачивается». Неоплатимая поставка на сведённых книгах = двигатель. См. главу 38.
Фронт — модуль-ветвь, читающий одну задачу через запрет двигателя: зелёная структурная половина + честный гейт (вход). Маска — одна из больших задач, прочитанных так; их семь плюс восьмая (БСД). См. коду.
Гейт / вход — именованное 🔴-утверждение, которого не хватает до цели: RopeCountingLaw
(пал), DescentLaw, EngineBridge. Гейт честно назван, не доказан и не спрятан.
Герой — центральная условная теорема ветви, доводящая закон до цели («дай закон — получишь
остановку»): reaches_one_of_countingLaw у Коллатца. Метка ГЕРОЙ в исходниках.
Эпистемика¶
«Узнать нельзя» / *Cause_unknowable — теоремы о невозможности внутреннего самообоснования:
доказать закон изнутри, пересекая собственную границу, — самоуничтожающаяся конструкция
(P ∧ ¬P), содержательно отождествлённая с уже сожжённым двигателем. НЕ Гёдель: это
модель-внутренняя эпистемика, а не теорема о неполноте. См. главу 33.
«Решение заперто за двигателем» — сводка-трёхразвилка: опровергнуть изнутри = построить двигатель; доказать изнутри = самообоснование; решает лишь внешняя проверка или декрет. См. главу 56.
«Проверка, а не вывод» — итоговая эпистемическая формула: ответ доступен только проверкой свидетеля, находимого ровно настолько далеко, насколько достаёт конечнотопливный взгляд (горизонт событий машины). См. главы 55–56.
Горизонт событий (машины) — предел досягаемости конечнотопливного наблюдателя: его ранговый бюджет. Дотянуться за горизонт изнутри = вечный двигатель. См. главу 56.