Спуск и граничный закон¶

← 03. Сохранение двойки · Оглавление · 05. Необратимость →

Lean-источник: EuclidsPath/Engine/Descent.lean Теоремы главы: two_carry_opposite, no_small_divisor, obstruction_on_opposite.

В предыдущей главе мы установили носитель двойки: стороны близнечного центра 6m−1 и 6m+1 отличаются ровно на 2, поэтому их общий делитель делит эту разность, а всякий простой p>2 делит не более одной стороны. Двойка — это то, что стороны разделяет.

Теперь мы покажем, куда эта двойка девается, когда двигатель — запрещённая бесконечная цепь строгого спуска (см. словарь) — делает шаг: спуск не уничтожает зазор, а переносит его на противоположную сторону спущенного центра. Из этого переноса и рождается граничный закон (boundary-law) — единственная делимость, которой может нарушиться чистота descended-состояния.

Установка: чистый спуск и высота¶

Напомним рабочую конфигурацию. Центр m лежит в чистом ядре Ω_A, когда обе его стороны раскладываются в произведение простых, строго больших порога A. Пусть одна сторона — скажем, 6m+σ с σ∈{±1} — оказалась составной внутри слоя и несёт активный множитель a>A: $$6m+\sigma = a\,(6n+\varepsilon),\qquad a>A,\ \varepsilon\in\{-1,+1\}.\tag{4.1}$$ Удаляя активный множитель a, мы объявляем спущенным центром то n, для которого остаток 6n+ε равен второй скобке. Это и есть один такт двигателя: из масштаба m мы переходим к масштабу n.

Первое наблюдение — строгий спуск по высоте (высота — это ранг состояния, конечное топливо двигателя; см. словарь). Поскольку a>A и 6m+σ = a(6n+ε), множитель a съедает по крайней мере фактор A от величины стороны, а значит и от центра: $$n < \frac{m}{A}.\tag{4.2}$$

Примечание. Высотой H мы называем сам центр m (эквивалентно — величину стороны в логарифмической шкале). Строгое неравенство n<m/A — не оценка «в среднем», а поэлементная арифметика делимости: если a·(6n+ε) = 6m+σ и a>A, то 6n+ε ≤ (6m+σ)/A. Именно это неравенство в следующей главе даёт необратимость: спуск не может длиться бесконечно, ибо m/A^t<1 для больших t, а положительный целый центр <1 невозможен.

Перенос двойки на противоположную сторону¶

Спустившись к n, мы получаем новый центр с двумя сторонами: 6n+ε (та скобка, что осталась после удаления a) и противоположная 6n−ε. Ключевое тождество главы говорит, что противоположная сторона отличается от оставшейся ровно на удвоенный знак — то есть на ту самую двойку, что несёт зазор.

Введём для краткости U := 6n+ε — сторону-остаток спущенного центра.

Теорема 4.1 (two_carry_opposite). Если $U = 6n+\varepsilon$, то $$6n-\varepsilon = U - 2\varepsilon.\tag{4.3}$$

Доказательство в Lean занимает одну строку (linear_combination -hU) и полностью алгебраично: $$6n-\varepsilon = (6n+\varepsilon) - 2\varepsilon = U - 2\varepsilon.$$

Содержательно это означает следующее. Зазор 2 между сторонами близнеца инвариантен при спуске: он не появляется и не исчезает, а лишь меняет носителя. Была разность (6n+ε)−(6n−ε)=2ε между сторонами спущенного центра — и она в точности воспроизводит удвоенный знак 2ε. Мы говорим, что двойка «перенесена вперёд»: активный множитель a унесён из стороны-произведения, а разделяющая двойка перекочевала на противоположную сторону U−2ε.

Примечание. Знак ε — это чётностный «спин» стороны-остатка (+1 для верхней скобки, −1 для нижней). Величина переноса 2ε∈{−2,+2} совпадает по модулю с носителем двойки из предыдущей главы. Так спуск сшивается с носителем: то, что стороны разделяет наверху (gcd ∣ 2), — то же самое, что переносится вниз (U−2ε).

Малый простой не портит сторону-произведение¶

Теперь спросим: чем вообще может нарушиться чистота спущенного центра? Чистота требует, чтобы обе его стороны состояли из простых >A. Сторона-остаток U унаследована из разложения 6m+σ, и её множители по построению больше A — удаление активного a>A оставляет остаток U=b·v из простых b,v>A. Значит опасность может исходить только от старого малого простого p≤A. Следующее утверждение исключает такой простой из стороны-произведения.

Теорема 4.2 (no_small_divisor). Пусть $b, v$ — простые числа, $A < b$, $A < v$, и пусть $p$ — простое число с $p \le A$. Тогда $$p \nmid (b\cdot v).\tag{4.4}$$

Доказательство прямое (в Lean — через Nat.Prime.dvd_mul и Nat.prime_dvd_prime_iff_eq): если бы p ∣ b·v, то по лемме Евклида p∣b или p∣v; но делимость простого на простое означает равенство, p=b либо p=v, что противоречит p≤A<b и p≤A<v (в Lean оба случая закрывает omega).

Смысл этой леммы — разграничение ответственности. Сторона-произведение U=b·v не может быть испорчена никаким старым простым p≤A: её множители лежат выше порога, вне досягаемости малых простых. Поэтому если чистота descended-центра всё же нарушается неким p≤A, виновата не сторона-остаток, а только противоположная сторона.

Примечание. Здесь важна не просто «двухфакторность» U=b·v, а именно то, что оба множителя прошли фильтр >A. Это гарантировано родословной: U есть скобка из разложения исходной стороны, все простые которого по определению Ω_A больше A. Малый простой в этой программе никогда не является дефектом исходного центра — он может появиться лишь как поглощающий выход спущенного центра из чистого ядра.

Граничный закон: обструкция живёт на противоположной стороне¶

Соберём два предыдущих наблюдения. Спущенный центр имеет сторону-произведение sideProd = U, которую малые простые не трогают, и противоположную сторону sideOpp = U−2ε — перенесённую двойку. Обструкцией мы называем событие «некий простой p делит одну из сторон» (выход на границу чистого ядра, boundary-exit). Следующая теорема показывает, что при p∤U эта дизъюнкция схлопывается в одну делимость.

Теорема 4.3 (obstruction_on_opposite). Пусть $\mathit{sideProd} = U$, $\mathit{sideOpp} = U - 2\varepsilon$ и $p \nmid U$. Тогда $$\bigl(p \mid \mathit{sideProd} \ \lor\ p \mid \mathit{sideOpp}\bigr)\ \Longleftrightarrow\ p \mid \mathit{sideOpp}.\tag{4.5}$$

Доказательство элементарно. Слева направо: если p∣sideProd, то p∣U (ибо sideProd=U) — противоречие с p∤U; значит остаётся p∣sideOpp. Справа налево тривиально (правый дизъюнкт). В Lean это rintro-разбор с absurd h hpU в невозможной ветви.

Соединяя с Теоремой 4.2 (no_small_divisor) (которая как раз даёт p∤U для малого p≤A, ибо U=b·v с b,v>A) и с Теоремой 4.1 (two_carry_opposite) (которая опознаёт sideOpp = U−2ε как перенесённую двойку), получаем граничный закон программы:

\[\boxed{\ p\mid 6n-\varepsilon\ }\qquad(\text{эквивалентно } p\mid U-2\varepsilon).\tag{4.6}\]

Вывод. Единственная делимость, способная выбить спущенный центр из чистого ядра, — это делимость противоположной стороны 6n−ε на старый простой p≤A. Обструкция не может сидеть на стороне-произведении: там все множители выше порога. Вся ответственность за выход на границу сосредоточена в одной точке — на перенесённой двойке.

Примечание. Отсюда и название «граничный закон» (boundary-law). Дихотомия чистого спуска предельно проста: либо спущенный центр остаётся в Ω_A и двигатель делает следующий такт, либо он выходит на границу — и тогда причина строго одна, p∣6n−ε. Никаких других механизмов выхода нет. Это редукция всей комбинаторики обструкции к единственной арифметической делимости, завязанной на перенос двойки.

Что доказано и что это значит¶

Три машинно-проверенные теоремы — Теорема 4.1 (two_carry_opposite), Теорема 4.2 (no_small_divisor) и Теорема 4.3 (obstruction_on_opposite) — вместе устанавливают, что один такт двигателя устроен так:

строгий спуск по высоте — из 6m+σ=a(6n+ε) с активным a>A следует n<m/A (арифметика делимости, без каких-либо распределительных допущений);
сохранение зазора — двойка не теряется, а переносится: $6n-\varepsilon = U-2\varepsilon$ (Теорема 4.1);
локализация обструкции — малый простой не портит сторону-произведение (Теорема 4.2), поэтому граница достигается ровно тогда, когда $p\mid 6n-\varepsilon$ (Теорема 4.3, уравнение (4.6)).

Всё доказательство элементарно — кольцо и делимость; ни анализа, ни распределения, ни сита. Это важно методологически: спуск и граничный закон — атомарные факты, на которых стоит вся дальнейшая конструкция, и они не зависят ни от одной открытой гипотезы.

Примечание (что здесь ещё открыто). Доказана невозможность бесконечного локального чистого спуска (следующая глава). Но конечное дерево спусков, где каждая ветвь оканчивается граничным листом (p∣6n−ε), комбинаторно возможно: локальный закон не даёт глобального non-cover. Это честная граница данной главы — она закрывает механику одного такта, но не глобальную структуру дерева. План закрытия глобального узла разворачивается позднее (multi-rank non-cover, а в пределе — rank-1 shifted-neighbour obstruction p∣a−2ε, прямой потомок граничного закона).

Итак, у нас есть чётко описанный такт: активный множитель уходит, высота строго падает, двойка переносится вперёд, а любой выход на границу опознаётся единственной делимостью противоположной стороны. Строгое неравенство n<m/A из первого пункта — это уже стрела: масштаб может только уменьшаться, и каждый такт умножает его на множитель меньше 1/A. В следующей главе мы превратим это наблюдение в закон необратимости — покажем, что двигатель Евклида не может ни вернуться назад, ни работать вечно.

← 03. Сохранение двойки · Оглавление · 05. Необратимость →