Двигатель Евклида: невозможность вечного спуска¶
← 00. Обзор · Оглавление · 02. Носитель двойки →
Lean-источник:
EuclidsPath/Engine/EPMI.lean,EuclidsPath/Engine/Irreversibility.lean.
Где мы¶
В обзоре мы свели гипотезу о простых-близнецах к вопросу о поведении одного динамического объекта — цепи самоподобных евклидовых уравнений, которую мы назвали двигателем Евклида. Обзор дал карту; настоящая глава вводит центральный объект этой карты и доказывает его определяющее свойство: двигатель не может работать вечно. Всё остальное здание — носитель двойки, законы сохранения, редукция к близнецам — опирается на этот единственный факт, поэтому мы формулируем его с полной строгостью и с точными именами машинно-проверенных теорем.
Мотивация: контрпример как вечный двигатель¶
Начнём с интуиции. Предположим, что близнецов-простых лишь конечное число. Тогда, начиная с некоторого масштаба, каждая пара (6m−1, 6m+1) обязана содержать составную сторону, а её разложение — активный делитель, удаление которого порождает структурно такое же евклидово уравнение меньшего центра. Повторяя удаление, мы получаем бесконечную цепь спусков, ни на одном шаге не выходящую из «чистого» ядра (clean-core). Такую бесконечно работающую цепь естественно назвать вечным двигателем: она бесконечно совершает нетривиальную работу спуска, ничего при этом не теряя.
Наша задача — показать, что подобный двигатель невозможен. Это в точности бесконечный спуск Ферма, переформулированный на языке центров евклидовых пар. Ключевое наблюдение состоит в том, что состояние двигателя целиком описывается одним натуральным числом — его высотой, а один успешный шаг спуска строго и мультипликативно уменьшает эту высоту. Дальше работает не физика, а арифметика натурального ряда.
Фрактал пути Евклида · ландшафт спуска: высота каждого центра как рельеф — двигатель катится вниз
по нему и обязан достичь дна за конечное число шагов. Полная галерея из шести видов —
в tools/fractal/.
Алгоритм генерации (рис. 1.1). Источник:
tools/fractal/euclid_fractal.py::descent_landscape. Для каждого центра \(m = 0, 1, \dots, S^2-1\), разложенного на растр \(S\times S\) (\(S = 620\), построчно по \(m\)), вычисляется малопростая нагрузка\[ L(m) \;=\; \Omega_B(6m-1) + \Omega_B(6m+1), \]где \(\Omega_B(x)\) — число простых делителей \(x\), считаемых с кратностью и ограниченных первыми \(B = 12\) простыми \(\ge 5\) (то есть \(5, 7, 11, \dots, 41\)). Цвет ячейки задаётся значением \(L(m)\) (палитра
inferno, отсечка по 99-му перцентилю). Центры-близнецы — где обе стороны \(6m\pm1\) просты — имеют \(L(m) = 0\) и образуют тёмные долины; самоподобный рельеф есть китайско-остаточная периодичность малых простых.
Определение шага спуска и высоты¶
Абстрагируемся от арифметической начинки и оставим только то, что нужно для доказательства невозможности. Состояние двигателя несёт единственную числовую характеристику — высоту h ∈ ℕ; содержательно это центр m пары (6m−1, 6m+1).
Определение 1.1 (шаг спуска). Пусть A ∈ ℕ — фиксированный масштабный порог (нижняя граница активных множителей). Один успешный clean-спуск с высоты h на высоту h' есть выполнение неравенства
$\(\mathrm{DescentStep}\,A\,h\,h' \;:=\; A\cdot h' < h. \tag{1.1}\)$
В Lean это буквально def DescentStep (A h h' : Nat) : Prop := A * h' < h. Определение фиксирует не абы какое, а мультипликативное убывание: новая высота не просто меньше старой, она меньше в A раз (с точностью до строгого неравенства). Именно множитель A, а не разность, задаёт скорость спуска и делает конечность неизбежной за конечное число шагов.
Примечание. Высота — это резервуар «топлива» двигателя. В содержательной картине программы её роль играет гармоническая высота состояния \(H(C,D) = CD/(C+D)\), монотонность которой вдоль хода вытекает из детерминантного закона перехода; но для доказательства невозможности достаточно её дискретной абстракции — натурального индекса центра. Мы сознательно работаем на минимальном ядре Lean 4, без mathlib, чтобы
no_infinite_descentпроверялся быстро и без внешних зависимостей.
Первое, что мы замечаем: при A ≥ 1 мультипликативный шаг влечёт обычное строгое убывание.
Теорема 1.2 (descent_strict). Если 1 ≤ A и выполнен DescentStep A h h', то h' < h.
Доказательство одношаговое: из 1 ≤ A следует h' ≤ A·h' (умножение на положительный множитель не уменьшает), а A·h' < h — по определению шага; транзитивность даёт h' < h. Почему это важно как отдельное утверждение: оно отделяет направление спуска (высота падает) от его скорости (падает в A раз). Направление понадобится во второй главе о необратимости; скорость — прямо сейчас, для конечности.
Невозможность бесконечного спуска¶
Теперь центральный результат в его чистой, абстрактной форме.
Теорема 1.3 (no_infinite_descent). Пусть 1 ≤ A. Не существует последовательности высот H : ℕ → ℕ, для которой каждый шаг был бы успешным A-спуском, то есть
$\(\forall\, t,\quad \mathrm{DescentStep}\,A\,(H\,t)\,(H\,(t+1)). \tag{1.2}\)$
Из существования такой последовательности выводится False.
Почему это верно. Идея доказательства элементарна и полностью конструктивна. Рассмотрим величину H t + t. На каждом шаге высота H t падает как минимум на 1 (по теореме 1.2, descent_strict), а счётчик t растёт на 1; значит сумма H t + t не возрастает, и по индукции
$\(\forall\, t,\qquad H\,t + t \;\le\; H\,0. \tag{1.3}\)$
Формально шаг индукции использует два факта: A·H(n+1) < H n (звено цепи) и H(n+1) ≤ A·H(n+1) (положительность A), откуда H(n+1) + (n+1) ≤ H n + n ≤ H 0. Подставим теперь t = H 0 + 1:
$\(H\,(H\,0 + 1) + (H\,0 + 1) \;\le\; H\,0. \tag{1.4}\)$
Левая часть строго больше H 0 (в ней уже слагаемое H 0 + 1), а должна быть не больше H 0 — противоречие. В Lean весь этот аргумент закрывается индукцией и тактикой omega; #print axioms подтверждает, что теорема не зависит ни от каких аксиом — она полностью конструктивна и без sorry.
Что это значит. Мультипликативное убывание \(H_t < H_0/A^{t}\) уводит высоту ниже 1 за конечное число шагов, а положительное целое не может быть меньше 1. Иначе говоря, натуральный ряд имеет дно, и дискретный спуск обязан этого дна достичь. Заметим, что для самого противоречия достаточно даже A = 1 (порядковая полнота ℕ); множитель A ≥ 1 лишь даёт количественную оценку скорости, к которой мы вернёмся ниже.
Примечание (сильнее второго закона термодинамики). Физический второй закон говорит об асимптотическом росте энтропии: система стремится к равновесию, но формально может приближаться к нему бесконечно долго. Наш дискретный аналог сильнее. Поскольку высота — целое число со строгим дном, спуск не просто «затухает», а останавливается за конечное число шагов — не более чем за
H 0(см. теорему 1.11,turned_engine_halts, в главе о необратимости). Дискретность дна превращает асимптотику в жёсткую конечность: двигатель не замедляется до нуля, он выключается.
Структурная форма: состояние и boundary-exit¶
Абстрактная теорема говорит о последовательности чисел. Чтобы связать её с содержательной картиной, введём явное состояние и оператор шага, различающий два исхода удаления активного множителя.
Определение 1.4 (состояние). structure State where height : Nat — состояние двигателя с единственным полем высоты; содержательно это центр m текущей евклидовой пары.
Определение 1.5 (шаг с двумя исходами). Частичный clean-descent оператор D_a над состоянием s даёт один из двух результатов, что в Lean кодируется индуктивным типом
$\(\mathrm{Step}\,A\,s \;=\; \begin{cases} \texttt{clean}\ s'\ (A\cdot s'.\mathrm{height} < s.\mathrm{height}), & \text{успешный спуск в clean-состояние},\\[2pt] \texttt{boundary}, & \text{поглощающий выход } \bot. \end{cases}\)$
Ветвь clean несёт свидетельство мультипликативного убывания высоты; ветвь boundary фиксирует выход descended-центра из clean-ядра на границу, откуда нет возврата.
С этим определением центральная теорема переформулируется на языке траекторий состояний.
Теорема 1.6 (no_perpetual_engine). Пусть 1 ≤ A. Нет траектории run : ℕ → State, в которой каждый шаг — успешный clean-спуск, то есть A·(run (t+1)).height < (run t).height для всех t.
Доказательство — прямое приведение к абстрактной форме: берём последовательность высот t ↦ (run t).height и применяем теорему 1.3 (no_infinite_descent). Это и есть «нет вечного двигателя Евклида»: бесконечная цепочка successful clean-descents не существует.
Наконец, зафиксируем, что других исходов шага, кроме двух названных, нет.
Теорема 1.7 (boundary_dichotomy). Для любого шага st : Step A s выполнено ровно одно из двух: либо st есть clean s' h для некоторых s' и свидетельства h, либо st = boundary:
$\(\bigl(\exists\, s'\,h,\ st = \texttt{clean}\ s'\ h\bigr)\ \lor\ \bigl(st = \texttt{boundary}\bigr).\)$
Доказательство — разбор случаев по конструктору индуктивного типа. Содержательно это типовая фиксация дихотомии из boundary-exit law: descended-центр либо остаётся clean (и тогда высота строго упала в A раз), либо выходит на поглощающую границу ⊥. Из boundary нет clean-продолжения той же ветви — такое продолжение потребовало бы успешного clean-шага, которым boundary по построению не является. Граница поглощает: ⊥ ↛ S.
Необратимость и асимметрия направлений¶
Теорема 1.3 (no_infinite_descent) отвечает на вопрос «всегда ли двигатель останавливается?». Второй естественный вопрос — «может ли он повернуть назад?» — закрывается в соседнем модуле Irreversibility.lean, дающем полный дискретный аналог второго закона термодинамики для двигателя. Мы кратко фиксируем его результаты, поскольку они опираются напрямую на введённые выше определения.
Теорема 1.8 (engine_never_returns). Если каждый шаг — успешный A-спуск (A ≥ 1), то высота строго антимонотонна: s < t ⟹ H t < H s. Двигатель никогда не возвращается в более раннее (более высокое) состояние. Доказательство собирает пошаговое убывание descent_strict в глобальную StrictAnti через strictAnti_nat_of_succ_lt.
Вместе теорема 1.8 (engine_never_returns, «не повернёт назад») и теорема 1.3 (no_infinite_descent, «всегда остановится») составляют весь второй закон: куда бы двигатель ни поехал, он не повернёт назад и остановится. К этому добавляется направленная асимметрия ресурса.
Теорема 1.9 (no_infinite_engine_descent). Любая строго убывающая f : ℕ → ℕ даёт False — вниз двигатель ехать вечно не может (это в точности no_infinite_descent при A = 1).
Теорема 1.10 (fuel_ascent_strictMono). Отображение n ↦ n+1 строго возрастает — вверх, к бо́льшим центрам, топлива всегда хватает: двигатель едет без остановки. Асимметрия резкая: бесконечное движение возможно только в одном направлении — вверх.
Теорема 1.11 (turned_engine_halts). Если двигатель свернул в спуск и сделал k строгих шагов вниз (H(t+1) < H(t) при t < k), то k ≤ H 0. Это количественная форма конечности: любой поворот вниз — конечный путь длиной не более начальной высоты. Именно эта оценка делает наш результат сильнее асимптотического второго закона: указано точное число шагов до остановки.
Роль в каркасе и открытый узел¶
Соберём смысл главы. Мы ввели центральный объект программы — двигатель Евклида как цепь clean-спусков — и доказали, машинно и без аксиом, что бесконечно он работать не может (теоремы 1.3, 1.6), не поворачивает назад (теорема 1.8) и, свернув вниз, останавливается за конечное число шагов (теорема 1.11). Дихотомия теоремы 1.7 фиксирует, что единственная альтернатива продолжению спуска — поглощающий выход на границу.
Честно очертим границу доказанного. Всё перечисленное — это невозможность бесконечного локального clean-спуска вдоль одной ветви. Отсюда не следует автоматически глобальный результат о непокрытии.
Гипотеза и план закрытия. Комбинаторно мыслимо конечное дерево ограниченной глубины, каждая ветвь которого честно обрывается absorbing boundary-leaf, — и при этом покрывает все центры. Локальная невозможность двигателя такого сценария сама по себе не исключает. Наблюдение состоит в том, что запрет вечного спуска нужно поднять с ветви на всё дерево. План закрытия: переоформить фронт как multi-rank non-cover с редукцией ранга (4→3→2→1) к rank-1 обструкции соседа, где счётные аргументы запрещены по построению. Этот единственный оставшийся узел разбирается в поздних главах (см. 10. NonCover, 18. SNOL); двигатель же поставляет для него локальный закон конечности, на котором стоит вся редукция.
Мост к следующей главе¶
Мы установили, что спуск не может продолжаться вечно, но пока ничего не сказали о том, что именно переносится вдоль спуска и удерживает пары «разделёнными». Ответ — число 2: стороны 6m−1 и 6m+1 отличаются ровно на двойку, и эта двойка есть носитель, сохраняющийся при каждом ходе двигателя. К нему — общему делителю сторон, делящему их разность, — мы переходим в следующей главе о носителе двойки.