Второй закон: необратимость и стрела времени¶

← 04. Спуск и boundary-law · Оглавление · 06. Нет хода назад →

Lean-источник: EuclidsPath/Engine/Irreversibility.lean (поверх EuclidsPath/Engine/EPMI.lean). Ключевые теоремы главы: engine_never_returns, no_infinite_engine_descent, fuel_ascent_strictMono, turned_engine_halts. Без анализа, распределения и сита — только порядковая полнота ℕ.

Откуда мы пришли¶

В предыдущей главе 04 Descent мы установили механику одного шага двигателя: если у центра m∈Ω_A одна сторона пары $(6m-1,\,6m+1)$ составна и вскрывается активным множителем a>A, то высота строго падает — новый центр n удовлетворяет $A\cdot n < m$, а двойка переносится на противоположную сторону через boundary-law. Тогда мы смотрели на спуск как на локальное событие: один поворот руля, один толчок вниз.

Теперь мы поднимаемся на уровень выше и спрашиваем о глобальной динамике: что происходит с траекторией двигателя как с целым? Ответ — два утверждения, которые вместе образуют второй закон термодинамики для двигателя Евклида: необратимость (двигатель не возвращается) и конечность спуска (двигатель всегда останавливается).

Обе половины доказаны машинно, без единой аксиомы сверх стандартных.

Высота как термодинамическое время¶

Напомним модель состояния. Состояние двигателя целиком кодируется одним натуральным числом — его высотой.

Определение 5.1 (высота). Состоянию S, содержательно отвечающему центру m пары $(6m-1,\,6m+1)$, сопоставляется высота $H(S) := m \in \mathbb{N}$. Траектория двигателя — это последовательность высот $H : \mathbb{N} \to \mathbb{N}$, где аргумент t играет роль дискретного времени, а H(t) — состояние в момент t.

В Lean состояние формализовано структурой State с единственным полем height : Nat (EuclidsPath/Engine/EPMI.lean); всё содержательное богатство пары свёрнуто в этот скаляр, потому что для второго закона важна только монотонность по высоте, а не арифметическая природа центра.

Один успешный чистый спуск (clean-descent) — это шаг, уменьшающий высоту не менее чем в A раз.

Определение 5.2 (шаг спуска). Для $A,h,h' \in \mathbb{N}$

\[ \mathrm{DescentStep}(A,h,h') \;:\Longleftrightarrow\; A\cdot h' < h. \tag{5.1} \]

Содержательно: из состояния высоты h двигатель переходит в состояние высоты h', причём $A\cdot h' < h$, то есть высота падает по крайней мере в A раз (Engine/EPMI).

Ключевая лемма, на которую опирается всё дальнейшее, — что при $A\ge 1$ такой шаг строго понижает высоту.

Лемма 5.3 (descent_strict, Engine/EPMI). Если $1 \le A$ и $\mathrm{DescentStep}(A,h,h')$, то h' < h.

Почему. При $A\ge 1$ имеем $h' \le A\cdot h'$ (умножение на положительный множитель не уменьшает), а по определению шага $A\cdot h' < h$; цепочка $h' \le A\cdot h' < h$ даёт h' < h.

Именно строгость h' < h, а не только $A\cdot h' < h$, превращает высоту в стрелу времени: каждый шаг двигателя необратимо сдвигает его в новое, более низкое состояние.

Необратимость: двигатель не повернёт назад¶

Локальная строгость («каждый следующий шаг ниже предыдущего») интегрируется в глобальное утверждение о всей траектории.

Теорема 5.4 (engine_never_returns). Пусть $1 \le A$ и $H : \mathbb{N} \to \mathbb{N}$ — траектория, в которой каждый шаг есть успешный спуск: $\forall t,\; \mathrm{DescentStep}(A,\,H(t),\,H(t+1))$. Тогда H строго антимонотонна:

\[ \mathrm{StrictAnti}\,H \;:\Longleftrightarrow\; \bigl(\forall s\,t,\; s < t \Rightarrow H(t) < H(s)\bigr). \tag{5.2} \]

Что доказано. Не просто «соседние состояния убывают», а что любое более позднее состояние строго ниже любого более раннего. Двигатель никогда не возвращается ни в одно из уже пройденных (более высоких) состояний — ни на следующем шаге, ни через миллион шагов.

Почему так. Доказательство в Lean — одна строка: strictAnti_nat_of_succ_lt поднимает локальную строгую убываемость H(n+1) < H(n) (которую для каждого n даёт Лемма 5.3 (descent_strict)) до глобальной строгой антимонотонности. Это стандартный факт о $\mathbb{N}$: убываемость на каждом единичном шаге эквивалентна убываемости на любом интервале, потому что порядок на натуральных числах дискретен и транзитивен. Содержательно: необратимость на одном шаге, накопленная по всем шагам, есть необратимость траектории.

Что это значит. Высота H — это координата термодинамического времени, а $\mathrm{StrictAnti}\,H$ — формальное выражение стрелы времени: направление «вниз по высоте» выделено физически, и обратного хода по нему нет. Двигатель Евклида, однажды тронувшись в спуск, не может восстановить прежнее состояние — в точности как замкнутая система не может самопроизвольно понизить свою энтропию.

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

Конечность спуска: двигатель всегда останавливается¶

Вторая половина закона утверждает, что бесконечного спуска не бывает. Это — абстрактная форма невозможности вечного двигателя (EPMI — ядро программы, доказанное на голом ядре Lean; см. словарь), доказанная в соседнем модуле, и здесь мы применяем её к чистой монотонности.

Теорема 5.5 (no_infinite_engine_descent). Не существует строго убывающей последовательности натуральных чисел: если $f : \mathbb{N} \to \mathbb{N}$ и $\mathrm{StrictAnti}\,f$, то $\bot$ (противоречие).

Почему так. Строго убывающая f — это спуск с параметром A=1: условие $\mathrm{StrictAnti}\,f$ даёт f(t+1) < f(t), что и есть $\mathrm{DescentStep}(1,\,f(t),\,f(t+1))$ после $1\cdot h' = h'$. Тогда применима базовая теорема no_infinite_descent (Engine/EPMI), доказательство которой — чистая порядковая полнота $\mathbb{N}$: величина f(t) + t не возрастает вдоль цепочки (каждый шаг теряет минимум 1 в высоте и приобретает 1 во времени), значит $f(t) + t \le f(0)$ для всех t; но при t = f(0)+1 это даёт $f(t) + f(0) + 1 \le f(0)$ — невозможно.

Формально: $$H(S_t) \;<\; \frac{H(S_0)}{A^{\,t}} \;<\; 1 \quad\text{для больших } t,$$ а высота — положительное целое, меньше 1 быть не может. Спуск обязан оборваться.

Что это значит. Двигатель Евклида всегда останавливается. Нет вечного двигателя: невозможна бесконечная последовательность успешных чистых спусков. Это ровно бесконечный спуск Ферма, переписанный как термодинамика: система не может вечно понижать высоту, потому что высота ограничена снизу нулём.

Направленная асимметрия: вверх бесконечно, вниз конечно¶

Здесь проступает сама суть стрелы времени — асимметрия двух направлений. Вниз двигатель проехать вечно не может (только что показано). Вверх — может.

Теорема 5.6 (fuel_ascent_strictMono). Отображение $n \mapsto n+1$ строго монотонно: $\mathrm{StrictMono}\,(\lambda n.\,n+1)$.

Почему так. Тривиально: n < n+1 для всех n, и прибавление +1 сохраняет строгий порядок. Но тривиальность формы не должна скрывать содержательность утверждения. Successor-цепочка $0,1,2,3,\dots$ — это бесконечная строго возрастающая траектория. Прибавление +1 — «топливо»: бо́льших центров всегда хватает, и вверх двигатель может ехать без остановки.

Наблюдение. Из интуиции: +1 — это топливо, +2 — это груз (сохраняемая двойка, первый закон, 03 TwoGap). Естественно предположить, что именно эта разность направлений и есть источник необратимости: вверх пространство состояний неограниченно (no_infinite_engine_descent неприменима, потому что цепочка не убывает), вниз оно упирается в дно (no_infinite_engine_descent запрещает бесконечность). Двигатель едет бесконечно только в одном направлении — вверх; всякий спуск конечен.

Вывод. Сопоставление двух теорем — no_infinite_engine_descent и fuel_ascent_strictMono — и есть строгое выражение того, что термодинамическая ось имеет выделенное направление. Вверх и вниз не взаимозаменяемы: одно бесконечно, другое обрывается. Это асимметрия, а не симметрия, — и потому есть стрела.

Свернуть значит остановиться: точная оценка¶

Последняя теорема главы количественно уточняет «всегда останавливается»: она даёт явную границу на длину любого спуска.

Теорема 5.7 (turned_engine_halts). Пусть $H : \mathbb{N} \to \mathbb{N}$ и двигатель сделал k строгих шагов вниз, то есть H(t+1) < H(t) для всех t < k. Тогда

\[ k \;\le\; H(0). \tag{5.3} \]

Что доказано. Если двигатель свернул в спуск, он остановится не более чем за H(0) шагов — ровно столько, какова его начальная высота. Спуск не просто конечен, он конечен с явной, легко вычислимой оценкой сверху.

Почему так. Индукцией по t доказывается инвариант $$\forall\, t \le k,\qquad H(t) + t \;\le\; H(0).$$ База (t=0): H(0)+0 = H(0). Шаг: из H(n+1) < H(n), то есть $H(n+1)+1 \le H(n)$, и из предположения $H(n)+n \le H(0)$ получаем $H(n+1)+(n+1) \le H(n)+n \le H(0)$. Подставив t=k и отбросив неотрицательное $H(k)\ge 0$, имеем $k \le H(k)+k \le H(0)$. Это тот же баланс «высота плюс время не растёт», что и в no_infinite_descent, но прочитанный как конечная оценка, а не как выход на противоречие.

Что это значит. «Свернёт — остановится», причём с чеком: цена спуска ограничена стартовой высотой. Никакого анализа, распределения или сита — только порядковая полнота $\mathbb{N}$. Именно поэтому второй закон в этой программе атомарен и доказан безусловно: он живёт целиком в комбинаторике порядка на натуральных числах.

Итог главы¶

Второй закон термодинамики для двигателя Евклида состоит из двух безусловно доказанных половин и их асимметрии:

необратимость — engine_never_returns ($\mathrm{StrictAnti}\,H$): двигатель не возвращается ни в одно более раннее состояние;
конечность спуска — no_infinite_engine_descent (нет бесконечной строго убывающей цепи): двигатель всегда останавливается, с явной оценкой turned_engine_halts ($k \le H(0)$);
асимметрия направлений — fuel_ascent_strictMono против no_infinite_engine_descent: вверх бесконечно, вниз конечно; это и есть стрела времени.

Всё это доказано машинно, без sorry, только на стандартных аксиомах и без обращения к распределению простых.

Мост к следующей главе¶

Мы установили, что двигатель не поворачивает назад во времени — вдоль своей траектории по высоте. В следующей главе 06 NoBackward мы обнаружим родственную, но иную необратимость — пространственную, на уровне двух точек пары.

Там источником запрета хода назад окажется носитель двойки 02 Carrier: один и тот же простой не может сидеть на обеих сторонах пары ($\text{shared gcd} \mid 2$), из-за чего диагональ $\sum_p X_p Y_p$ исчезает, а произведение рангов — ранг здесь, как всегда, «высота» состояния, падающая вдоль разрешённых шагов (см. словарь) — оказывается целиком внедиагональным.

Если в этой главе необратимость запрещала возврат по стреле времени, то в следующей эксклюзивность запретит «работу назад» на паре — и именно эта исчезнувшая диагональ станет точным источником отрицательной ассоциации (r_-,r_+), которую позднее эксплуатирует four-corner 12.

← 04. Спуск и boundary-law · Оглавление · 06. Нет хода назад →