20. NOPSL: нет sink значит twin¶

← 19. Old-peel · Оглавление · 21. Регенерация →

Источник: snol_old_peel_closure_ru_2026-06-30.md (§5–14). Lean: Engine/NOPSL.lean (OldPeelLedger, no_old_peel_sink, snol_of_nopsl, twin_primes_of_nopsl; стандартные аксиомы).

В [19 Old-peel] мы раскрыли последний узел программы: carrier-scale catch $p\mid a-2\varepsilon$ оказался не терминалом, а шагом спуска — old-peel порождает новый, строго меньший центр $t<n$, и доказанная алгебра (old_peel_sign, old_peel_height_drop) гарантирует строгое падение высоты.

Осталось превратить это локальное падение в глобальное утверждение: поток old-peel обязан где-то остановиться, и остановка эта — twin. Именно это замыкание мы и формализуем здесь под именем NOPSL (No Old-Peel Sink Lemma): показываем, что абстрактное ядро — строгий спуск с регенерацией — само по себе, без единого обращения к распределению, влечёт бесконечность близнецов.

Абстракция: что именно мы фиксируем¶

Прежде чем доказывать, нужно честно выделить структуру, которую поставляет old-peel, и отделить её от всего наглядного антуража. Из интуиции старого спуска естественно вычленить ровно четыре данных: высоту состояния, предикат корректной остановки, отношение шага и два закона, связывающие их. Мы собираем это в одну структуру.

Определение 20.1 (OldPeelLedger). Old-peel ledger над типом состояний $\sigma$ — это набор

\[ L=\bigl(h,\ \mathrm{Sink},\ \mathrm{Step},\ \texttt{step\_drops},\ \texttt{regenerate}\bigr), \tag{20.1} \]

где - $h:\sigma\to\mathbb N$ — высота состояния (масштаб текущего центра); - $\mathrm{Sink}:\sigma\to\mathrm{Prop}$ — предикат корректной остановки (twin-центр либо остановившийся clean-возврат, который не продолжается вниз); - $\mathrm{Step}:\sigma\to\sigma\to\mathrm{Prop}$ — отношение old-peel преемника; - $\texttt{step\_drops}:\ \mathrm{Step}\,s\,s'\Rightarrow h(s')<h(s)$ — закон old-peel: каждый шаг строго уменьшает высоту; - $\texttt{regenerate}:\ \neg\,\mathrm{Sink}(s)\Rightarrow\exists\,s',\ \mathrm{Step}\,s\,s'$ — регенерация: любое не-sink состояние имеет old-peel преемника.

В Lean это буквально structure OldPeelLedger с полями h, Sink, Step, step_drops, regenerate. Заметим, что структура ничего не знает ни о простых, ни о делимости, ни о конкретном виде catch — она чисто комбинаторна. Это принципиально: вся арифметика old-peel уже израсходована на то, чтобы обеспечить два поля-закона, а дальнейшее рассуждение ведётся исключительно на языке «высота падает» и «поток не висит».

Разберём, откуда берётся каждый закон.

Поле step_drops — это прямая упаковка теоремы OldPeel.old_peel_height_drop из предыдущей главы: old-peel quotient удовлетворяет $t<n/5<n$, то есть высота нового центра строго меньше высоты старого. Здесь нет гипотезы — это доказанная алгебра, подтверждённая на 100% реальных rank-1 catch'ей.

Поле regenerate — содержательный узел NOPSL. Оно утверждает: у состояния, которое не является корректной остановкой, обязательно есть исходящее ребро спуска. Наглядно это дихотомия §10–11: любой не-twin центр $t$ попадает в один из классов —

clean-возврат в rigid-ledger ($t\in\Omega_A$, но $t\ge A^2$, то есть ещё не twin sink);
следующий old-peel ($t\notin\Omega_A$: есть $q\le A$ с $q\mid 6t\pm1$);
fan-in / Hall (много родословных сходятся в один $t$);
уже классифицированный defect,

— и в каждом из них есть корректный преемник. Ключевое отрицательное утверждение: нет пятого класса — нет «висячего» терминала, у которого нет ни sink-статуса, ни преемника. Именно несуществование такого висячего терминала мы и кодируем как regenerate.

Примечание. Разделение на два поля не косметическое: step_drops — доказанная арифметика (её нельзя ослабить), а regenerate — структурная гипотеза о замкнутости ledger. Абстракция OldPeelLedger нужна затем, чтобы точно локализовать: всё, что осталось обосновать вне Lean-ядра, сидит в одном поле regenerate и больше нигде.

NOPSL: поток достигает sink¶

Теперь главное утверждение. Оно говорит, что абстрактная структура сама себя замыкает.

Теорема 20.2 (no_old_peel_sink, §11.1/13.1). Для любого old-peel ledger $L$ над $\sigma$ и любого старта $\mathrm{start}\in\sigma$ существует состояние $s$ с $\mathrm{Sink}(s)$:

\[ \forall L,\ \forall\,\mathrm{start},\quad \exists\,s,\ L.\mathrm{Sink}(s). \tag{20.2} \]

Покажем, почему это верно, и одновременно проследим за Lean-доказательством — оно короткое и в нём нет ни одной лазейки.

Рассуждаем от противного. Предположим, sink'а нет вовсе: $\neg\,\exists s,\ \mathrm{Sink}(s)$. Тогда каждое состояние — не-sink, и по regenerate у каждого $s$ есть преемник: $$\forall s,\ \exists s',\ \mathrm{Step}\,s\,s'.$$ В Lean это строка have hstep : ∀ s, ∃ s', L.Step s s', где не-sink-статус любого $s$ получается из отрицания существования sink'а.

Функцией выбора (choose next hnext) превращаем «для каждого $s$ есть преемник» в конкретную функцию $\mathrm{next}:\sigma\to\sigma$ с $\mathrm{Step}\,s\,(\mathrm{next}\,s)$ для всех $s$. Из неё рекурсией строим бесконечную траекторию $$z(0)=\mathrm{start},\qquad z(k+1)=\mathrm{next}\,(z(k)), \tag{20.3}$$ у которой каждое звено — настоящий old-peel шаг: $\mathrm{Step}\,(z\,k)\,(z\,(k{+}1))$.

Применяя step_drops к каждому звену, получаем строго убывающую последовательность высот: $$\forall k,\quad h\bigl(z(k+1)\bigr)<h\bigl(z(k)\bigr). \tag{20.4}$$ Это последовательность натуральных чисел, убывающая на каждом шаге бесконечно долго. Такого не бывает — и ровно это утверждает OldPeel.old_peel_terminates, которая, в свою очередь, есть переупаковка no_infinite_engine_descent (нет бесконечного строгого спуска в $\mathbb N$ = невозможность вечного двигателя Евклида, EPMI; см. словарь). Противоречие, и предположение об отсутствии sink'а ложно. $\qquad\blacksquare$

Почему именно так, а не иначе: содержательная сила теоремы — не в выборе преемника (это стандартная техника), а в том, что тот же самый факт «нет бесконечного строгого спуска», которым мы раньше запрещали вечный двигатель, теперь запрещает вечное уклонение от sink'а. Двигатель и NOPSL — две проекции одного запрета. Поэтому замыкание не требует новой математики: оно наследует уже доказанную невозможность.

Примечание. Обратите внимание, что в доказательстве не используется ни IsTwinCenter, ни делимость, ни $\Omega_A$ — только step_drops, regenerate и терминальность спуска в $\mathbb N$. NOPSL — теорема о высоте и регенерации, а не о простых числах. Простые войдут лишь на следующем шаге, когда мы скажем, что именно есть sink.

SNOL как немедленное следствие¶

Прежде чем связывать sink с близнецами, зафиксируем формально исчезновение прежнего препятствия. В 18 SNOL финальным узлом был «terminal shifted-neighbour obstruction»: гипотетический carrier-scale catch, который никуда не ведёт. Теперь мы можем сказать, почему его нет.

Теорема 20.3 (snol_of_nopsl, §13). Для любого old-peel ledger $L$ и старта существует sink:

\[ \exists\,s,\ L.\mathrm{Sink}(s). \tag{20.5} \]

Формально snol_of_nopsl — это в точности Теорема 20.2 (no_old_peel_sink) применённая к $L$ и start; отдельное имя нужно, чтобы подчеркнуть содержательное прочтение. Если бы terminal SN-obstruction существовал, его состояния были бы одновременно не-sink (нет twin) и без регенерации (некуда идти) — а это прямо противоречит полю regenerate. Значит obstruction невозможен, и поток гарантированно достигает корректной остановки. То есть SNOL — не самостоятельная гипотеза, а тень NOPSL: как только мы приняли regenerate, «нет висячего терминала» доказывается автоматически.

Финальное замыкание: нет sink значит twin¶

Осталось назвать sink близнецом. Здесь абстракция встречается с гипотезой Полиньяка. Мы навешиваем на каждый масштаб $N$ свой ledger и требуем, чтобы его корректные остановки были twin-центрами выше $N$.

Теорема 20.4 (twin_primes_of_nopsl, §14.1). Пусть даны - семейство ledger'ов $L(N)$ и стартов $\mathrm{start}(N)$ для каждого масштаба $N\in\mathbb N$; - функция центра $\mathrm{center}(N,\cdot):\sigma\to\mathbb N$; - условие остановки-на-близнеце

$$\texttt{sink\_is\_twin}:\quad \forall N,s,\ \ L(N).\mathrm{Sink}(s)\ \Rightarrow\ N<\mathrm{center}(N,s)\ \wedge\ \mathrm{IsTwinCenter}\bigl(\mathrm{center}(N,s)\bigr). \tag{20.6}$$

Тогда $\mathrm{TwinLowers.Infinite}$ — простых-близнецов бесконечно много.

Доказательство разворачивается за три хода, буквально как в Lean. Сводим цель к неограниченности twin-центров через infinite_of_unbounded_centers (мост §NonCover: если для любого $N$ есть twin-центр $m>N$, то множество близнецов бесконечно). Далее фиксируем произвольный $N$ и применяем Теорему 20.2 (no_old_peel_sink) к ледгеру $L(N)$ со стартом $\mathrm{start}(N)$ — получаем sink $s$. Наконец, по sink_is_twin этот sink даёт центр $\mathrm{center}(N,s)$, который лежит выше $N$ и является twin-центром. Значит на каждом масштабе есть близнец выше него — то есть их неограниченно много. $\qquad\blacksquare$

Итог раздела. Логическая цепочка программы полностью замкнута. Каждое звено —

\[\underbrace{\texttt{step\_drops}}_{\text{доказанная алгебра}}\ +\ \underbrace{\texttt{regenerate}}_{\text{структурный вход}}\ \xRightarrow{\ \texttt{no\_old\_peel\_sink}\ }\ \text{sink}\ \xRightarrow{\ \texttt{sink\_is\_twin}\ }\ \text{twin-центр}>N\ \xRightarrow{\ \texttt{infinite\_of\_unbounded\_centers}\ }\ \text{бесконечность близнецов}\]

— проверено компилятором. Единственный вход в теорему («вход» — честно названное, пока не доказанное допущение, см. словарь) — структура OldPeelLedger, а не распределение простых.

Что доказано и что предполагается — честно¶

Разделим строго верифицированное и оставшийся вход, не выдавая редукцию за доказательство.

Доказано машинно. Полная импликация $\texttt{OldPeelLedger}\ \Rightarrow\ \mathrm{TwinLowers.Infinite}$ на чистой логике строгого спуска, без единого счётного или распределительного аргумента. Это переводит SNOL/NOPSL из прозы в верифицированную редукцию: если поставить ledger с двумя его законами, бесконечность близнецов следует автоматически.

Осталось обосновать. Ровно две предпосылки структуры OldPeelLedger, и обе — не счётные:

step_drops — доказана алгеброй old-peel (old_peel_height_drop, числа 100%). Здесь вопрос закрыт.
regenerate — структурная гипотеза NOPSL: quotient-центр $t$ всегда классифицируется (clean-возврат / next-peel / fan-in / known-defect), то есть расширенный rigid-ledger замкнут относительно old-peel quotients без несclassifiable терминала.

Гипотеза (regenerate). Расширенный rigid-ledger замкнут по old-peel quotients: у всякого не-twin центра $t$ есть корректный преемник в одном из четырёх классов §10–11. Эквивалентно: не существует висячего carrier-scale терминала.

План закрытия. Дихотомия классов (1)–(3) уже формализована в следующей главе как теорема regeneration_dichotomy (безусловно, стандартные аксиомы). Нетривиальный остаток локализован в классе (4) — fan-in / Hall — и в требовании, что цикл из §11 несёт настоящую rigid-подпись двигателя. Именно этот остаток и есть содержательное наполнение поля regenerate; его закрытие ведётся не через распределение, а через payment-ledger аргумент carrier-scale массы (аудит §13.C–D источника).

Примечание. Ключевое отличие regenerate от всех прежних входов программы (например, от счётного H): он лежит в логике двигателя, а не распределения. Наглядно: «потоку некуда деться, кроме как вниз или в twin». Это единственная точка, оставшаяся вне Lean-ядра, и она же — центральная точка аудита.

Мост к следующему¶

Итак, финал сжат до одного структурного факта: поле regenerate, замкнутость ledger по old-peel quotients. Всё остальное — от строгого падения высоты до бесконечности близнецов — проверено компилятором. Естественно спросить: а можно ли доказать сам regenerate, хотя бы по частям? В [21 Дихотомия] мы формализуем Лемму 6.1 о регенерации и покажем, что её элементарное ядро — полная дихотомия quotient-центра плюс sign law — доказывается в Lean без распределения, оставляя явным входом лишь fan-in/Hall и rigid-подпись цикла.

← 19. Old-peel · Оглавление · 21. Регенерация →