Нет хода назад на двух точках¶

← 05. Необратимость · Оглавление · 07. Короткий train →

Lean-источник: Engine/NoBackward.lean (exclusive_diag_zero, exclusive_no_backward).

Где мы¶

В главе 05 мы установили необратимость двигателя Евклида — той самой бесконечной строго убывающей цепи, главного запрещённого объекта программы (см. словарь): высота H строго убывает вдоль спуска (StrictAnti H), время не обратимо, а перпетуум-мобиль невозможен. Стрела времени задаёт направление на одной координате — на высоте центра.

Теперь мы спрашиваем о более тонком: что происходит, когда двигатель рассматривается сразу на двух точках — на левой стороне 6m-1 и на правой стороне 6m+1. Оказывается, здесь есть свой запрет на ход назад, и он имеет чисто арифметическую природу. Именно этот запрет станет источником отрицательной ассоциации, которую позже эксплуатирует four-corner (глава 12).

Исходное наблюдение: эксклюзивность двойки¶

Напомним факт из главы 02 (Carrier). Две стороны твина отличаются на 2: $$(6m+1)-(6m-1)=2.$$ Поэтому любой общий делитель обеих сторон делит их разность, откуда $$\gcd(6m-1,\,6m+1)\mid 2.$$ Следствие, зафиксированное в Lean как Carrier.no_large_shared_divisor: простой p>2 не делит обе стороны одновременно — он делит не более одной из них. Назовём это свойство эксклюзивностью: на каждом нечётном простом ровно один из двух исходов (или ни одного), но никогда оба сразу.

Определение 6.1 (индикаторы, ранги, эксклюзивность). Для простого $p$ с индексом $i$ из конечного множества $s$ определим индикаторные веса $X, Y : \iota \to \mathbb{N}$ равенствами $$X_p=\mathbf{1}[\,p\mid 6m-1\,],\qquad Y_p=\mathbf{1}[\,p\mid 6m+1\,]$$ — «вклад слева» и «вклад справа». Ранги (числа простых делителей каждой стороны): $$r_-=\sum_{p\in s}X_p,\qquad r_+=\sum_{p\in s}Y_p.$$ Условие эксклюзивности — гипотеза hexcl в Lean: $$X_p\cdot Y_p=0\quad\text{для каждого }p\in s.$$

Примечание. В Lean это условие вынесено в гипотезу hexcl : ∀ i ∈ s, X i * Y i = 0. Величины X, Y : ι → ℕ берутся в натуральных числах, а не строго в {0,1}: доказательства ниже используют только X_p·Y_p=0, поэтому справедливы для любых неотрицательных весов с исчезающим произведением. Это делает результат абстрактной алгебраической леммой, а не привязанным к конкретным индикаторам утверждением.

Диагональ исчезает¶

Первое утверждение — простое, но опорное. Оно говорит, что сумма «self»-членов, где один и тот же простой сидит на обеих сторонах, равна нулю.

Теорема 6.2 (exclusive_diag_zero). Для конечного множества $s$ и весов $X, Y : \iota \to \mathbb{N}$, если $X_p \cdot Y_p = 0$ при всех $p \in s$, то $$\sum_{p\in s}X_p\cdot Y_p=0. \tag{6.1}$$

Доказательство в Lean — одна строка (Finset.sum_eq_zero hexcl): сумма нулей есть нуль. Но содержательный смысл важнее краткости. Величина $\sum_p X_p Y_p$ — это диагональ: она подсчитывает случаи, когда простой p делит и левую, и правую сторону, то есть «движение назад на одной точке» — self-переход, при котором двигатель на данном простом возвращается в самого себя, касаясь обеих сторон одновременно. Эксклюзивность стирает эту диагональ полностью: $\text{DIAG}=0$.

Примечание. Диагональ здесь — не метафора, а конкретный член разложения. В матричном языке, если N_{ij} — счёт центров с рангами (r_-,r_+)=(i,j), то ненулевые диагональные вклады на уровне простых отвечали бы корреляции «оба делят». Эксклюзивность обнуляет их поточечно, ещё до всякого суммирования по центрам.

Двигатель не работает назад на двух точках¶

Второе утверждение — главное. Оно превращает поточечное обнуление диагонали в структурное свойство произведения рангов.

Теорема 6.3 (exclusive_no_backward). Для конечного множества $s$ с разрешимым равенством индексов $[\mathrm{DecidableEq}\; \iota]$ и весов $X, Y : \iota \to \mathbb{N}$, при эксклюзивности $X_p \cdot Y_p = 0$ для всех $p \in s$, $$\Bigl(\sum_{i\in s}X_i\Bigr)\cdot\Bigl(\sum_{j\in s}Y_j\Bigr)=\sum_{i\in s}\ \sum_{j\in s\setminus\{i\}}X_i\cdot Y_j. \tag{6.2}$$

То есть произведение рангов $r_-\cdot r_+$ целиком внедиагонально: в двойной сумме отсутствуют члены i=j, остаются только пары $i\neq j$.

Почему так. Раскроем произведение сумм. Дистрибутивность (Finset.sum_mul, затем Finset.mul_sum) даёт $$\Bigl(\sum_i X_i\Bigr)\Bigl(\sum_j Y_j\Bigr)=\sum_{i\in s}\sum_{j\in s}X_i\,Y_j.$$ Внутреннюю сумму по $j\in s$ разобьём, выделив член j=i (лемма Finset.add_sum_erase): $$\sum_{j\in s}X_i\,Y_j=X_i\,Y_i+\sum_{j\in s\setminus\{i\}}X_i\,Y_j.$$ Выделенный член X_i Y_i есть в точности $X_i\cdot Y_i$, а по эксклюзивности $X_i\cdot Y_i=0$ для $i\in s$ (hexcl i hi). После zero_add остаётся только внедиагональная часть. Суммирование по i завершает доказательство.

Структурно это и есть «нет хода назад на двух точках». Произведение $(\sum X)(\sum Y)$ описывает совместное поведение двигателя на левой и правой стороне. Диагональ i=j отвечала бы одновременному ходу «в себя» на обеих точках — self-переходу $2\to 2$. Эксклюзивность запрещает его на каждом простом, и потому запрещает во всей сумме: остаются лишь перекрёстные переходы $i\neq j$, когда левый делитель и правый делитель — разные простые.

Примечание. Требование [DecidableEq ι] нужно лишь технически: чтобы s.erase i было определено (нужно уметь решать j=i). Математического содержания оно не несёт — для конечных множеств простых равенство всегда разрешимо.

Что это значит: источник отрицательной ассоциации¶

Соберём два факта вместе. Разложим ковариацию рангов. Для совместного распределения (r_-,r_+) по центрам $$\mathrm{Cov}(r_-,r_+)=\underbrace{\text{CROSS}}_{\text{внедиагональная связь}}-\underbrace{\text{DIAG}}_{\sum_p P_p^-P_p^+}, \tag{6.3}$$ где $\text{DIAG}$ собирает вклады «оба делят на одном простом».

Теорема 6.2 (exclusive_diag_zero) обнуляет поточечную диагональ, а Теорема 6.3 (exclusive_no_backward) показывает, что вся структура произведения рангов внедиагональна. Именно отсюда берётся знак: исчезнувшая диагональ — это «теплота», убранная необратимостью, и она смещает ассоциацию (r_-,r_+) в сторону отрицательной.

Численная разведка (tools/RESULTS_rank2.md) это подтверждает робастно: матрица счётов N_{ij} близка к рангу 1 (ранги почти независимы, $sv_2/sv_1\approx 0.001$), а знак ранг-2 поправки — той самой, что видит four-corner — отрицателен на всех проверенных масштабах, потому что $\mathrm{Cov}(r_-,r_+)<0$ всюду.

Вывод. Источник этого знака — не плотность простых и не статистика, а точная арифметическая эксклюзивность: простой делит не более одной стороны (shared gcd ∣ 2).

Примечание. Подчеркнём границу честности. Теорема 6.3 (exclusive_no_backward) доказывает структуру (произведение рангов внедиагонально) и обнуление $\text{DIAG}$ как поточечного члена (уравнение (6.1)). Это ещё не сам знак $\mathrm{Cov}(r_-,r_+)<0$ для реальных счётов: там присутствует конкурирующий член $\text{CROSS}$ (конечно-диапазонная корреляция), и требуется $\text{DIAG}>\text{CROSS}$. Эксклюзивность даёт нам первое слагаемое разложения (6.3) — необходимую, но не достаточную часть. Само неравенство $\text{DIAG}>\text{CROSS}$ (эквивалент $D=N_{03}N_{30}-N_{00}N_{33}>0$) остаётся открытым узлом программы.

Гипотеза 6.4 (отрицательная ассоциация рангов). Ранги $(r_-, r_+)$ отрицательно ассоциированы на всех масштабах: $$N_{00}N_{33}\le N_{03}N_{30}, \tag{6.4}$$ эквивалентно $\text{DIAG}\ge\text{CROSS}$.

План закрытия. Эксклюзивность (Carrier.no_large_shared_divisor, Теорема 6.2 (exclusive_diag_zero)) даёт поточечную структуру «произведение per-prime без перекрёстного $xy$-члена» — это в точности продуктовая CRT-модель $\prod_p(c_p+a_p x+b_p y)$ без члена $xy$ (глава 12). Для такой модели отрицательная ассоциация доказуема элементарно (Маклорена).

Остаётся контроль остатка модель→реальность: показать, что реальный $\text{CROSS}$ не превосходит $\text{DIAG}$. Это distribution-free кандидат, но численно $1-R_{fc}\to 0$ (knife-edge), что указывает на близость к стене чётности. Ни один из имеющихся приёмов пока не даёт распределённо-независимого закрытия; поэтому здесь узел объявлен открытым, а не закрытым (о статусах узлов см. словарь).

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

Мы получили запрет на ход назад на двух точках — арифметический механизм, обнуляющий диагональ и делающий совместную структуру рангов чисто внедиагональной. Это ограничение действует на ширину хода двигателя (совместное поведение сторон).

В следующей главе 07 мы обратимся к ограничению на длину хода: алгебраический кубический зажим $12(h+6h^2)<A\Rightarrow 72h^2<A$, то есть $h<\sqrt{A/72}$, показывает, что валидный сегмент train'а — число реально достижимых центров вдоль аффинной линии — короток, даже когда сама линия и топливо +1 бесконечны.

Итог раздела. Необратимость по высоте, запрет назад по ширине и короткий train по длине вместе сжимают двигатель со всех сторон.

← 05. Необратимость · Оглавление · 07. Короткий train →