Old-peel: catch как шаг спуска¶

← 18. SNOL · Оглавление · 20. NOPSL →

Lean-источник: EuclidsPath/Engine/OldPeel.lean (теоремы catch_is_opposite, old_peel_sign, old_peel_height_drop, no_infinite_old_peel, old_peel_terminates). Числа: tools/RESULTS_oldpeel.md (3000 реальных rank-1 catch'ей, A=200).

Где мы¶

В главе 18 SNOL вся программа была сведена к единственному машинно-зафиксированному узлу — терминальному shifted-neighbour препятствию на carrier-масштабе: если близнецов конечно, то у активного простого a > A соседняя сторона $a-2\varepsilon$ систематически ловится малым простым $p \le A$, что записывается как делимость $$p \mid a - 2\varepsilon,\qquad p \le A.$$

SNOL остановилась ровно на слове терминальное: узел был честной редукцией, но выглядел тупиком — делимость есть, а что с ней делать, оставалось открытым. Настоящая глава закрывает этот вопрос.

Мы покажем, что catch — не терминал, а шаг спуска: он раскрывается алгебраически, порождает новый меньший центр и строго уменьшает высоту. Тем самым финальный узел SNOL замыкается на уже доказанную в [EPMI / Irreversibility] невозможность двигателя Евклида — без всякого счёта и распределения.

Фрактал пути Евклида — лес old-peel

Фрактал пути Евклида · лес old-peel: дерево спусков, где каждый catch — шаг вниз по ветви. Ветви не разрастаются наружу, а сходятся к корню: всякая ветвь конечна и обрывается о дно — это и есть no_infinite_descent в картинке.

Алгоритм генерации (рис. 19.1). Источник: tools/fractal/euclid_fractal.py::old_peel_tree. Зафиксируем $A=200$ и просеем все простые до $4A^2$; пул пойманных простых — простые $p$ с $3 < p \le A$. Разместим горизонтальный ряд из $460$ корней с абсциссами $x$, равномерно распределёнными по $[-30,30]$; $i$-й корень несёт центр $n = \lfloor A^2/6\rfloor + 7i$. Из каждого корня запускается рекурсивный спуск $\mathrm{peel}(n,\varepsilon,d,x)$ для обоих знаков $\varepsilon=\pm1$: он останавливается при глубине $d>7$ или $n<2$; требует, чтобы сторона $a=6n+\varepsilon$ была простым с $a>A$; берёт противоположную сторону $6n-\varepsilon$, находит первое простое $p$ из пула, делящее её, образует частное $q=(6n-\varepsilon)/p$, читает его знак $\delta$ по $q\bmod 6$ ($\delta=+1$ при $q\equiv1$, $\delta=-1$ при $q\equiv5$, иначе обрыв) и задаёт дочерний центр $t=(q-\delta)/6$ (обрыв при $t\le0$). Шаг рисует отрезок из $(x,\ \log_{10}(n+1))$ в $(x+\varepsilon\cdot 0.55/(d+1),\ \log_{10}(t+1))$, затем рекурсивно заходит в $t$ с обоими знаками на глубине $d+1$. Вертикальная ось — высота $\log_{10}(\text{центр})$; горизонтальный сдвиг кодирует знак спуска $\varepsilon$. Отрезки рисуются коллекцией линий, окрашенной по глубине спуска $d$ через цветовую карту turbo, на почти чёрном фоне.

Catch — это вторая сторона клина¶

Начнём с элементарного наблюдения, которое переводит SNOL-делимость в язык двигателя. Активное простое приходит из клинового центра n: одна сторона клина есть само простое, $$6n + \varepsilon = a,\qquad \varepsilon \in \{\pm 1\}.$$ Противоположная сторона того же центра — это $6n - \varepsilon$. Прямая выкладка даёт

Определение 19.1 (перенос двойки). Для центра n со стороной $a = 6n+\varepsilon$ противоположная сторона равна $$6n - \varepsilon = (6n+\varepsilon) - 2\varepsilon = a - 2\varepsilon.$$

Этот перенос формально фиксируется так.

Теорема 19.2 (catch_is_opposite). Для целых $n,a,\varepsilon$, если $6n+\varepsilon = a$, то $6n-\varepsilon = a - 2\varepsilon$ (в Lean — одним шагом omega). Значит SNOL-делимость $p \mid a - 2\varepsilon$ — буквально есть делимость противоположной стороны клина: $$p \mid a - 2\varepsilon \iff p \mid 6n - \varepsilon.$$

Примечание. Отсюда сразу видно, почему SNOL нельзя опровергнуть счётом (что и было отмечено в 18): $p \mid 6n - \varepsilon$ — это не редкое совпадение, а норма для составной стороны клина. Ловля соседа — обычное дело; содержательным должно быть не попадание, а то, что происходит после него. Ниже мы извлекаем из попадания структуру, а не вероятность.

Раскрытие catch в old-peel¶

Раз p делит $6n - \varepsilon$, частное можно записать в той же клиновой форме $6t + \delta$. Это центральная запись главы.

Определение 19.3 (old-peel). Old-peel активного центра n вдоль пойманного простого p — это разложение противоположной стороны $$6n - \varepsilon = p\,(6t + \delta),\qquad p \le A,\ \varepsilon,\delta \in \{\pm 1\},$$ порождающее новый центр t (quotient-центр) и его знак $\delta$. Простое p здесь — старое (уже присутствующее в ledger — леджере, бухгалтерии потоков программы, см. словарь; $p \le A$); отсюда название old-peel: мы «сдираем» старый слой p и обнажаем под ним меньший центр t.

Таким образом делимость перестаёт быть тупиком: она сама поставляет объект спуска — центр t, меньший n. Осталось доказать три вещи: что запись согласована по знакам (sign law), что она действительно меньше (height drop) и что поток из таких шагов не может быть бесконечным (termination).

Закон знаков: δ = −π·ε¶

Знак нового центра не произволен — он жёстко определён знаками входа. Пусть $p \equiv \pi \pmod 6$, $\pi \in \{\pm 1\}$ (всякое простое > 3 даёт $\pi = \pm 1$).

Теорема 19.4 (old_peel_sign). Если $6n - \varepsilon = p(6t+\delta)$, $p \equiv \pi \pmod 6$ и $\varepsilon,\delta,\pi \in \{\pm 1\}$, то $$\boxed{\ \delta = -\,\pi\,\varepsilon\ }.\tag{19.1}$$

Почему. Приведём разложение по модулю 6. Из $p \equiv \pi$ пишем $p = \pi + 6k$, тогда $$p(6t+\delta) = \pi\delta + 6\big(\pi t + k(6t+\delta)\big) \equiv \pi\delta \pmod 6.$$ С другой стороны $6n - \varepsilon \equiv -\varepsilon \pmod 6$. Значит -\varepsilon \equiv \pi\delta \pmod 6, а поскольку все три знака в $\{\pm 1\}$, сравнение по модулю 6 превращается в равенство $\delta = -\pi\varepsilon$. Именно так устроено доказательство в Lean: подстановка $p = \pi + 6k$, выделение множителя 6 (hexp), редукция по модулю 6 (hmod6) и перебор восьми знаковых комбинаций через omega.

Примечание. Sign law — не косметика. Он говорит, что новый центр t рождается с предсказуемой ориентацией, согласованной с ориентацией родителя и с классом p по модулю 6. Это делает old-peel детерминированным шагом ledger, а не случайным разложением: следующий узел заранее «знает», какую сторону клина занимает. Численно закон выполняется на 3000/3000 = 100% реальных catch'ей (RESULTS_oldpeel.md).

Спуск высоты: t < n¶

Теперь ключевое — что old-peel опускает высоту. Высотой центра естественно взять сам n (порядок клина).

Теорема 19.5 (old_peel_height_drop). Если $6n - \varepsilon = p(6t+\delta)$ с $p \ge 5$, $\varepsilon,\delta \in \{\pm 1\}$, $t \ge 1$ и $n \ge 2$, то $$t < n.\tag{19.2}$$

Почему. Всё простое $p \le A$, пойманное на carrier-масштабе, есть простое > 3, значит $p \ge 5$. Тогда $6t + \delta = (6n - \varepsilon)/p \le (6n+1)/5$, откуда при $n \ge 2$ немедленно t < n. В Lean это перебор знаков $\varepsilon,\delta$ с последующим nlinarith по неравенствам $p \ge 5$, $t \ge 1$, $n \ge 2$ и самому разложению hpeel.

Численно спуск даже резче формулировки теоремы: харнесс даёт t < n/5 на 3000/3000 = 100% (фактор $p \ge 5$ съедает не меньше пятой части высоты за один шаг). Теорема доказывает мягкую, надёжную границу t < n; наблюдение t < n/5 — её эмпирическое усиление.

Примечание. Здесь и происходит превращение терминала в спуск. SNOL-делимость p \mid a - 2\varepsilon — не «стена», о которую разбивается активное простое, а ступенька вниз: каждый catch отправляет нас в строго меньший центр t. Регенерация потока (что t > 0, поток продолжается, а не обрывается в ноль) тоже подтверждена на 3000/3000 = 100%.

Почему спуск — это противоречие: старый двигатель¶

Соберём три закона в один динамический вывод. Предположим противное SNOL: терминала нет, то есть у каждого активного центра его catch раскрывается old-peel'ом (regenerate — см. 20). Тогда из любого старта строится последовательность центров $$z_0 > z_1 > z_2 > \cdots,\qquad z_{k+1} = t\big(z_k\big),$$ где каждое неравенство z_{k+1} < z_k дано Теоремой 19.5 (old_peel_height_drop). Это бесконечная строго нисходящая цепь натуральных высот — а её мы уже запретили в двигателе Евклида.

Теорема 19.6 (no_infinite_old_peel). Для любой $z : \mathbb{N} \to \mathbb{N}$ со свойством StrictAnti z следует False. В Lean это буквально no_infinite_engine_descent z hdesc — old-peel-высота используется как та же Ляпунова-цепь, которая приводит в противоречие движение двигателя вниз.

Теорема 19.7 (old_peel_terminates). Если $\forall k,\ z(k+1) < z(k)$, то False (через strictAnti_nat_of_succ_lt и Теорему 19.6 (no_infinite_old_peel)).

Что доказано и что это значит. Машинно-проверено ядро замыкания: любая бесконечная строго-нисходящая old-peel цепь центров даёт False. Контрапозиция читается прямо: поток old-peel обязан где-то остановиться — упереться в twin sink или вернуться в ledger чистым возвратом. Иначе он ехал бы вниз вечно, что невозможно в $\mathbb{N}$ и запрещено уже доказанной невозможностью двигателя (no_infinite_engine_descent, [EPMI / Irreversibility]).

Вывод. Финальный узел SNOL замыкается не на новую теорему о распределении, а на старый двигатель — в этом весь выигрыш главы.

Честный аудит: где остаётся вход¶

Доказаны в Lean: - вся алгебра old-peel — перенос двойки catch_is_opposite, закон знаков old_peel_sign, спуск высоты old_peel_height_drop; - ядро замыкания — бесконечный строгий спуск ⟹ False (no_infinite_old_peel, old_peel_terminates).

Численно на 3000 реальных rank-1 catch'ей все три эмпирических закона держатся на 100%: sign law $\delta = -\pi\varepsilon$, height drop t < n/5, регенерация t > 0. Old-peel — реальный механизм, а не гипотеза: он наблюдается на каждом проверенном узле.

Открытым остаётся один структурный (не счётный) вход — в терминах программы гейт: честно названное недоказанное утверждение, которого не хватает до цели (см. словарь). Чтобы превратить контрапозицию в полное доказательство, нужно знать, что quotient-центр t всегда классифицируется — попадает в одну из разрешённых категорий, а не в скрытый «несclassifiable терминал»:

Гипотеза 19.8 (регенерация old-peel, NOPSL). Для любого не-sink центра t его catch раскрывается в корректный old-peel-преемник, то есть t принадлежит одной из категорий:

clean-возврат ($t \in \Omega_A$; при t < A^2 — twin sink);

следующий old-peel ($t \notin \Omega_A \Rightarrow \exists\, q \le A,\ q \mid 6t + \eta$);

fan-in / Hall (несколько родословных сходятся в один t);

уже классифицированный defect.

План закрытия. Показать, что расширенный rigid-ledger замкнут относительно old-peel quotients: применение old-peel не выводит центр за пределы классификации и не вводит скрытый цикл в t-узле (центральная точка аудита). Это принципиально не счётный вход — в отличие от прежнего four-corner H, он не зовёт Мертенса и распределение делителей сдвига, а лежит в той же логике невозможности двигателя: «поток некуда деть, кроме как вниз или в twin».

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

Мы раскрыли финальный узел 18 SNOL в строгий спуск и замкнули его ядро на доказанный двигатель. Осталась ровно одна предпосылка — регенерация regenerate: что old-peel-поток не может вечно избегать корректного sink. В главе 20 NOPSL мы формализуем эту предпосылку абстрактной структурой OldPeelLedger (высота, sink, шаг, step_drops, regenerate) и докажем машинно полное замыкание $OldPeelLedger \Rightarrow \mathrm{TwinLowers.Infinite}$ через ту же логику строгого спуска — тем самым переведя всю редукцию SNOL/NOPSL из прозы в верифицированный вывод.

← 18. SNOL · Оглавление · 20. NOPSL →