21. Дихотомия регенерации¶

← 20. NOPSL · Оглавление · 22. Residuals →

Источник: old_peel_regeneration_formal_proof_ru_2026-06-30.md (Лемма 6.1 о регенерации). Lean: Engine/Regeneration.lean (5 теорем, стандартные аксиомы, без sorry). Опирается на Engine/OldPeel.lean (old_peel_height_drop) и питает Engine/NOPSL.lean (поле regenerate).

В 20 NOPSL мы свели всю программу к одному структурному факту — предпосылке regenerate абстрактного OldPeelLedger: любое не-стоковое состояние обязано иметь old-peel преемника, то есть поток quotient-центров «некуда деть, кроме как вниз или в twin». Замыкание было доказано машинно, но само regenerate осталось входом — честно названным недоказанным утверждением, гейтом в смысле словаря.

В этой главе мы вскрываем его изнутри: показываем, что за абстрактным словом «регенерирует» стоит элементарная и безусловная дихотомия любого центра t на три класса, и честно локализуем, какая ровно часть регенерации остаётся структурным входом, а не следствием алгебры.

Постановка: что классифицируем¶

После шага old-peel из 19 мы получаем quotient-центр — натуральное число $t>0$, кодирующее пару активных соседей $6t-1$ и $6t+1$. Вопрос регенерации: что происходит с этим центром дальше — есть ли из него исходящее ребро спуска, или он оказывается корректным стоком (twin-центром). Мы хотим показать, что третьего — «висячего терминала», в котором поток застревает без ребра и без twin, — при элементарном разборе не возникает.

Зафиксируем порог $A$ (масштаб уже снятых «старых» простых) и введём два предиката.

Определение 21.1 (old-free центр). Центр $t$ называется old-free относительно порога $A$, если ни одно простое $q$ с $5\le q\le A$ не делит ни одну из сторон $6t\pm1$:

\[ \mathrm{OldFree}(A,t)\ :\Longleftrightarrow\ \forall q\ \text{prime},\ 5\le q\le A\ \Longrightarrow\ \neg\bigl(q\mid 6t-1\ \lor\ q\mid 6t+1\bigr). \]

В Lean это def OldFree (A t : ℕ) : Prop. Содержательно $\mathrm{OldFree}(A,t)$ — это принадлежность центра «чистой зоне» $\Omega_A$: он не ловится ни одним из уже пройденных простых.

Определение 21.2 (twin-центр). Центр $t$ — twin, если обе стороны простые:

\[ \mathrm{Twin}(t)\ :\Longleftrightarrow\ (6t-1)\ \text{prime}\ \land\ (6t+1)\ \text{prime}. \]

В Lean это def Twin (t : ℕ) : Prop. Это единственный сорт корректного стока: пара простых-близнецов $(6t-1,6t+1)$.

Заметим сразу: нижняя граница $q\ge5$ не случайна. Простые $2$ и $3$ по построению carrier'а никогда не делят $6t\pm1$ (эти числа взаимно просты с $6$), поэтому «старыми» кандидатами на деление служат ровно простые $\ge5$. Именно с них начинается решето, и именно их порог $A$ отслеживает.

Разбор случая (3): не-old-free даёт old-peel edge¶

Начнём с логически простейшего звена — отрицания old-free.

Теорема 21.3 (not_oldfree_gives_peel). Если $\neg\,\mathrm{OldFree}(A,t)$, то существует старый делитель, порождающий old-peel: $$\neg\,\mathrm{OldFree}(A,t)\ \Longrightarrow\ \exists\,q\ \text{prime},\ 5\le q\le A\ \land\ \bigl(q\mid 6t-1\ \lor\ q\mid 6t+1\bigr).$$

Доказательство здесь — чистое разворачивание определения: $\neg\forall$ даёт $\exists$, и мы извлекаем свидетеля $q$ — конкретный объект, удостоверяющий утверждение (см. словарь). Никакого счёта, никакого распределения простых — только логическая структура квантора в определении $\Omega_A$. Формально в Lean это unfold OldFree с последующим simp only [not_forall, not_not] и извлечением пятёрки ⟨q, hq, h5, hA, hdvd⟩.

Почему это важно содержательно. Найденное $q\le A$ — «старое» простое: оно уже входит в пройденный масштаб, и деление $q\mid 6t+\eta$ означает, что сторона $6t+\eta$ раскладывается как $q\cdot(6t_1+\eta_1)$ с меньшим центром $t_1$. Это ровно конфигурация old-peel из 19, а значит по old_peel_height_drop мы имеем ребро спуска $t_1<t$. То есть случай (3) не просто классифицирует центр — он немедленно поставляет исходящее ребро вниз с доказанным падением высоты.

Разбор случая (1)+(2): old-free даёт twin или составную сторону¶

Теперь противоположная ветвь: центр old-free. Здесь нужен разбор по простоте сторон.

Теорема 21.4 (oldfree_twin_or_composite). Для любого $t$ $$\mathrm{Twin}(t)\ \lor\ \neg\,(6t-1)\ \text{prime}\ \lor\ \neg\,(6t+1)\ \text{prime}.$$

Это конструктивная тавтология: по закону исключённого третьего для простоты каждой стороны либо обе простые (тогда $\mathrm{Twin}(t)$), либо хотя бы одна составна. В Lean — двойной by_cases по (6*t-1).Prime и (6*t+1).Prime. Сформулировано без гипотезы $\mathrm{OldFree}$: сама дизъюнкция безусловна, а old-free подключается только для того, чтобы прочитать «составная сторона» как active descent (следующая теорема).

Примечание. Разделение (1) и (2) — это разделение «стока» и «спуска» внутри чистой зоны. Twin — терминал-приёмник, к которому мы и стремимся. Составная old-free сторона — не терминал: у неё, как мы сейчас покажем, обязан быть делитель выше порога $A$, то есть новое ребро.

Active descent: составная old-free сторона имеет большой делитель¶

Ключ к тому, что случай (2) — спуск, а не тупик, в следующем наблюдении.

Теорема 21.5 (composite_oldfree_has_big_divisor). Пусть сторона $side=6t+\eta\ge2$ составна и old-free (ни одно простое $q\le A$ её не делит). Тогда у неё есть простой делитель $b$ с $b>A$: $$\exists\,b\ \text{prime},\ A<b\ \land\ b\mid side.$$

Доказательство прозрачно и не апеллирует ни к какому анализу. Составное число $side\ge2$ имеет минимальный простой делитель $b=\mathrm{minFac}(side)$ (Nat.minFac_prime, Nat.minFac_dvd). Если бы было $b\le A$, то $b$ — простое $\le A$, делящее $side$, что прямо противоречит old-free. Значит $b>A$. В Lean это by_contra hle; exact holdfree side.minFac hb (by omega) hbd — доказательство от противного в одну строку.

Почему это и есть «активный евклидов спуск». Делитель $b>A$ раскладывает сторону как $6t+\eta=b\cdot U$ с новым фактором $U<side$. Это старт нового шага решета уже на большем масштабе: центр перерабатывается, а не исчезает. Тем самым обе не-twin ветви чистой зоны — снабжены исходящим ребром.

Примечание. Здесь видно, зачем нужна именно old-free-гипотеза. Без неё «составная сторона» ничего не говорит о величине делителя — он мог бы быть маленьким и уже пройденным. Old-free исключает все малые простые, поэтому минимальный делитель составного числа вынужденно оказывается новым (>A). Это чисто пороговый аргумент, без единого обращения к плотности простых.

Знаковый закон повторного old-peel¶

Отдельное, но необходимое для склейки цепочки звено — как ведёт себя знак $\eta$ при переходе к меньшему центру. Он фиксирует, что переработка центра сохраняет «полярность» соседа предсказуемо.

Теорема 21.6 (peel_sign). Пусть $6t+\eta=q\,(6t_1+\eta_1)$ с $\eta,\eta_1,\omega\in\{\pm1\}$ и $q\equiv\omega\pmod 6$. Тогда $$\eta_1=\omega\cdot\eta.$$

Доказательство — модулярная алгебра. Из $q\equiv\omega\pmod6$ пишем $q=\omega+6k$, подставляем в peel-уравнение и получаем $6t+\eta-\omega\eta_1\equiv0\pmod6$. Поскольку $\eta,\eta_1,\omega$ пробегают только $\pm1$, конечный перебор восьми знаковых комбинаций (rcases ... <;> omega) замыкает тождество $\eta_1=\omega\eta$. Никакой аналитики — только вычет по модулю $6$.

Содержательно это закон согласования знаков (7.1): при делении на старое простое $q$ его класс $\omega=q\bmod6\in\{\pm1\}$ переносит знак активной стороны с родителя на потомка. Это тот же по духу факт, что old_peel_sign ($\delta=-\pi\varepsilon$) в 19, но записанный на языке quotient-центров. Он гарантирует, что цепочка old-peel'ов не «теряет» ориентацию сторон, — необходимое условие корректности всей rigid-подписи ledger'а.

Сборка: полная дихотомия центра¶

Три элементарных звена собираются в одну безусловную теорему — сердцевину Леммы 6.1 о регенерации.

Теорема 21.7 (regeneration_dichotomy). Для любого центра $t$ и порога $A$ имеет место ровно один из исходов:

\[ \mathrm{Twin}(t) \ \lor\ \Bigl(\neg\,\mathrm{OldFree}(A,t)\ \land\ \exists\,q,\ q\ \text{prime},\ 5\le q\le A,\ q\mid 6t\pm1\Bigr) \ \lor\ \Bigl(\mathrm{OldFree}(A,t)\ \land\ \bigl(\neg(6t-1)\ \text{prime}\ \lor\ \neg(6t+1)\ \text{prime}\bigr)\Bigr). \]

Доказательство — by_cases hof : OldFree A t, и каждая ветвь закрывается уже доказанным звеном:

если центр не old-free — берём случай (3) через Теорему 21.3 (not_oldfree_gives_peel) (есть old-peel edge);
если центр old-free — через Теорему 21.4 (oldfree_twin_or_composite) либо он twin (сток), либо одна сторона составна (случай (2), где Теорема 21.5 (composite_oldfree_has_big_divisor) даёт active-descent edge).

Итог: Теорема 21.7 (regeneration_dichotomy) — полная и безусловная (стандартные аксиомы, без sorry). Каждый quotient-центр попадает ровно в один из трёх элементарных классов, и в двух из них — (2) и (3) — мы явно предъявили исходящее ребро спуска, а в третьем — (1) — корректный twin-сток. Это именно то элементарное ядро, ради которого затевалась вся редукция: классификация центра без счёта, без распределения, без PNT.

Примечание. Подчеркнём, что доказано, а что нет. regeneration_dichotomy доказывает классификацию $t$. Из неё же сразу вытекает наличие ребра в случаях (2), (3): для (3) падение высоты $t_1<t$ — это old_peel_height_drop из 19, уже доказанное; для (2) ребро $6t+\eta=b\cdot U$ существует по Теореме 21.5 (composite_oldfree_has_big_divisor), а его строгое падение высоты — отдельная элементарная лемма евклидова спуска (того же типа, что height drop, и не требующая счёта). Ни в (1), ни в (2), ни в (3) висячего терминала нет.

Где остаётся вход: случай (4), fan-in¶

Дихотомия исчерпывает три класса. Но полная картина регенерации в NOPSL включала четвёртый исход — тот, что мы честно не выводим из определения $\Omega_A$.

Гипотеза 21.8 (fan-in / Hall, аудит §13.C). На bounded-масштабе, где carrier-scale масса родословных сгущается в ограниченное множество центров, возможен fan-in defect: много различных родословных отображаются в один и тот же центр $t$. Это утверждение о множестве родословных, а не о делимости одной стороны, и потому не выводится из предиката $\mathrm{OldFree}(A,t)$.

Именно этот случай (4) остаётся полем regenerate абстрактного OldPeelLedger из 20. Разница принципиальна: случаи (1)–(3) — Теорема 21.7 (regeneration_dichotomy, доказана компилятором), а случай (4) — структурная предпосылка payment-ledger'а, требующая, чтобы rigid-цикл из 09/11 был настоящим двигателем — тем самым запрещённым объектом бесконечного спуска (см. словарь) — с жёсткой (rigid) подписью (аудит §13.D).

План закрытия. Естественно предположить, что fan-in контролируется не счётом, а условием Холла на двудольном соответствии «родословная — центр»: если carrier-масса нигде не превышает ёмкость приёмных центров, дефекта fan-in нет и regenerate выполнено структурно. Это ведёт к Product/Hall-конструкции (см. позднее 29) и к отделяющему масштабу, но уже вне элементарного алгебраического ядра этой главы.

Наблюдение из чисел (19, RESULTS_oldpeel.md): регенерация $t>0$, sign law и height drop подтверждаются на 100% из 3000 реальных rank-1 catch'ей — то есть механизм регенерации наблюдается, и открытым остаётся ровно контроль его кратности, а не самого существования.

Итог и мост к следующей главе¶

Мы вскрыли предпосылку regenerate изнутри. Авторская Лемма 6.1 формализована: элементарное ядро — полная дихотомия центра (Теорема 21.7, regeneration_dichotomy), знаковый закон (Теорема 21.6, peel_sign) и active-divisor-лемма (Теорема 21.5, composite_oldfree_has_big_divisor) — доказано в Lean без распределения.

Вывод. Регенерация в случаях (1)–(3) — настоящая теорема, а не редукция: twin-сток либо явное ребро спуска в каждом центре. Нетривиальный остаток локализован ровно в случае (4) — fan-in/Hall — и в требовании rigid-цикла; он остаётся явным структурным входом, как и заявляет сам источник (§13: «при выполнении A–E регенерация доказана»). Дихотомия закрывает пункты A, B аудита; C, D — вход.

Тем самым fan-in — единственное, что теперь отделяет нас от полной регенерации, — оказывается вопросом кратности отображения родословных в центры, то есть вопросом о плотности заполнения приёмных центров. В 22 мы делаем следующий шаг: показываем, как снять предположение о плотности — перевести контроль fan-in с гипотезы о массе на структурное условие покрытия, — и тем приблизить случай (4) к тому же элементарному режиму, в котором уже живут случаи (1)–(3).

← 20. NOPSL · Оглавление · 22. Residuals →