24. Декомпозиция boundary и глобальный узел¶

← 23. Clean-граф · Оглавление · 25. Rigid-замыкание →

Источник: step00_boundary_exit_decomposition_global_absorber_fix_ru_2026-06-30.md, step00_labelled_fanin_patch_ru_2026-07-01.md. Lean: Engine/BoundaryDecomp.lean (декомпозиция доказана; глобальный узел — явная гипотеза), Engine/LabelledFanIn.lean (König доказан, SNOL сведён к более лёгкому закону) и Engine/AtomicSNOL.lean (атомизация SNOL — рефакторинг), Engine/ConcreteComponents.lean (active/old-peel компоненты доказаны; финальная density-редукция циркулярна), Engine/BadCoverDescent.lean (bad-cover descent — тоже циркулярна), Engine/ObstructionClosure.lean (abstract obstruction-двигатель — входы неинстанциируемы), Engine/ManyUnresolved.lean (массовая collision — циркулярна), Engine/HigherEnergy.lean (взвешенная энергия долга — реальный движок, но promotion мизориентирован = refuel), Engine/HigherTower.lean (инверсный предел — fixed-center башня вакуумна, moving = стена), Engine/EngineTower.lean (inverse-limit без traversal — обходит orientation-стену, но recurrence вакуумна, escape = counting), Engine/ParityBarrier.lean + Engine/ReverseTower.lean (стена чётности как теорема — негативный результат), Engine/AboveConflict.lean (конфликт в «Above» — order-логика тривиальна, force-вход в ловушке), Engine/JumpBarrier.lean (jump/cut-barrier — paid jump + cofinal cut-пиджонхол доказаны, force-ray/barrier = стена), Engine/PaidDynamics.lean (платная динамика — no free inertia/acceleration/cloning доказаны, regeneration-to-close = SNOL стена), Engine/ClosedUniverse.lean (двигатель не покидает вселенную — universe-preservation + closed-paid no-run доказаны, promotion_paid_or_closes = стена). Всё — редукции/рефакторинги/инструменты, не закрытие; см. разделы ниже. Числа: tools/RESULTS_global_absorber.

В 23. Rigid closure мы свели всё замыкание к одному конструктивному входу: у каждого не-twin центра делитель должен порождать валидный меньший центр (regenerates_needs_target_center), а clean_sink_is_twin из clean-графа отсекла от sink старые нечистые близнецы. Осталось честно разобрать выход из чистого графа — состояние BoundaryExit, где чистый центр m спускается к нечистому n. Именно здесь прежняя точечная гипотеза «boundary регенерирует» и ломается; в этой главе мы показываем, как ломается, и куда переезжает нагрузка.

Фрактал пути Евклида — линия центров с родословными

Фрактал пути Евклида · линия центров с родословными: twin-центры по обе стороны от линии, а на самой линии — генеалогии простых Евклида, спускающиеся к своим центрам. Именно эти родословные и их коллизии — предмет узла настоящей главы.

Алгоритм генерации (рис. 24.1). Источник: tools/fractal/euclid_fractal.py::twin_line_genealogy. Центры $m=1,\dots,M$ ($M=2400$) откладываются вдоль горизонтальной оси $y=0$. Сторона $6m+1$ отмечается точкой над линией на высоте $\mathrm{wing}(m)=0.9+0.25\sqrt{m/M}$, сторона $6m-1$ — симметричной точкой под линией, когда соответствующее число просто (решето primes_upto(6M+2)). Twin-центр (обе стороны просты) отмечается золотой вертикалью $[-\mathrm{wing},\,+\mathrm{wing}]$ с точками на концах. Вдоль линии для каждого $m$ вычисляется old-peel-шаг: если $6m\mp1 = p\cdot(6t\pm1)$ с простым свидетелем Евклида $p\in[5,97]$, рисуется полуокружностная дуга $m\to t$ высотой $h=0.06\,|m-t|^{0.85}+0.4$ (36 точек, $x=\tfrac{m+t}{2}+\tfrac{|m-t|}{2}\cos\theta$, $y=h\sin\theta$, $\theta\in[0,\pi]$), окрашенная по $\log p$ в палитре turbo. Twin-центры живут вне линии, генеалогия — на ней.

Почему точечная регенерация boundary неверна¶

Напомним конструкцию из 23: ребро m → n есть BoundaryExit A m n, если m чист, ребро активно (n < m), а цель n не чиста. Естественно было бы предположить точечный закон

\[\texttt{boundary\_exit\_regenerates}:\quad \mathrm{BoundaryExit}\,A\,m\,n \;\Rightarrow\; \exists\, k,\ \mathrm{Step}\,n\,k,\]

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

\[18 \;\longmapsto\; (107,\,109),\]

малый нечистый twin-центр, к которому неприменима clean_twin_above (он ниже порога $M_0$) и из которого никакой old-peel не выводит: обе стороны просты, делить нечем. Точечный закон здесь ложен — у состояния нет преемника, но и корректным sink оно не является (оно нечисто, а clean_sink_is_twin требует чистоты). Значит гипотезу нельзя чинить локально: нельзя гарантировать преемника у каждой отдельной нечистой цели.

Примечание. Это не мелкий изъян формулировки, а структурный факт. Pointwise-закон утверждал бы, что чистый граф самодостаточен как система переходов. Он не самодостаточен: 59% чистых центров (число RESULTS_clean_graph из 23) имеют все рёбра в boundary. Поток массово вытекает из чистого графа, и куда он утекает — вопрос не о точке, а о множестве.

Доказуемая часть: boundary декомпозируется¶

То, что доказуемо на уровне точки, — это не регенерация, а дихотомия исхода. Введём тип исхода.

\[\mathrm{BoundaryOutcome}\,A\,M_0\,n \;:=\; \underbrace{\bigl(\exists\, t<n\bigr)}_{\text{old-peel вниз}} \;\lor\; \underbrace{\bigl(n \le M_0\bigr)}_{\text{старый absorber}}.\]

В Lean это inductive BoundaryOutcome с двумя конструкторами: peel (t) (ht : t < n) — old-peel к строго меньшему центру — и absorber (h : n ≤ M0) — состояние уткнулось в старый absorber ниже порога. Ключевая теорема:

Теорема 24.1 (boundary_exit_decomposes). Пусть $1 \le n$, $\eta \in \{+1,-1\}$, малый простой $q$ с $q \ge 5$, $q \bmod 6 \in \{1,5\}$ делит сторону $6n+\eta$. Тогда существует валидный меньший центр:

\[ \exists\, t',\ (\exists\,\eta'\in\{\pm1\}) \ \land\ 0 \le t' \ \land\ t' < n. \]

Доказательство одношаговое: из cofactor_is_center (доказанной алгебраически в 23, 100% на 307010 случаях) делимость $q \mid 6n+\eta$ немедленно даёт кофактор $(6n+\eta)/q$ вида $6t'+\eta'$ с $\eta'\in\{\pm1\}$, $0 \le t' < n$. То есть если у нечистого $n$ вообще есть малый простой делитель стороны, то old-peel-ребро вниз существует и высота строго падает.

Дихотомия BoundaryOutcome разводит это по признаку $n \le M_0$: либо мы ещё выше порога и делитель гонит нас дальше вниз (ветка peel), либо мы уже провалились в конечное множество старых absorber'ов $n \le M_0$ (ветка absorber).

Что здесь доказано и почему. Доказана ровно та часть, которая держится на алгебре одного шага: наличие делителя $\Rightarrow$ наличие меньшего центра. Точечный контрпример $18 \mapsto (107,109)$ ей не противоречит — там делителя стороны нет (обе стороны простые), поэтому дихотомия относит такое $n$ не к peel, а к absorber: это конечный endpoint ниже $M_0$, а не терминал в открытом поле. Тем самым Теорема 24.1 (boundary_exit_decomposes) не притворяется регенерацией: она честно фиксирует, что нечистая цель либо продолжает спуск, либо садится в старый absorber. Второй исход — не преемник, а именно то место, где точечная логика бессильна.

Куда переезжает нагрузка: глобальный absorber-узел¶

Раз точечно каждый absorber-endpoint может не иметь преемника, вопрос переформулируется на уровне всего множества свежих стартов. Зафиксируем гипотезу конечности близнецов и её следствие.

\[\mathrm{NoNewTwinAbove}\,M_0 \;:=\; \forall\, m > M_0,\ \neg\,\mathrm{TwinCenterZ}\,m,\]

\[\mathrm{GlobalOldTwinAbsorption}\,A\,M_0 \;:=\; \text{«все свежие clean-старты выше } M_0 \text{ в итоге садятся в конечное множество старых absorber'ов } \le M_0\text{».}\]

(В Lean GlobalOldTwinAbsorption — структурный плейсхолдер-предикат; содержательно это утверждение о том, что поток всех чистых стартов выше порога поглощается конечным старым множеством.) Тогда финальный узел формулируется как импликация:

Определение 24.2 (GlobalAbsorberNode). (§4 — не доказан, явная гипотеза.)

\[ \mathrm{GlobalAbsorberNode}\,A\,M_0\,\mathsf{Engine} \;:=\; \mathrm{NoNewTwinAbove}\,M_0 \;\to\; \mathrm{GlobalOldTwinAbsorption}\,A\,M_0 \;\to\; \mathsf{Engine}. \tag{24.1} \]

Содержательно: «конечное множество старых twin-absorber'ов не может поглотить все свежие чистые старты выше $M_0$ без двигателя».

Смысл перехода. Точечно старый absorber $18$ безобиден — один endpoint без преемника. Но выше порога $M_0$ появляется бесконечно много свежих чистых стартов, а старых absorber'ов конечное число. Если новых близнецов нет (NoNewTwinAbove), то все эти старты обязаны сесть в конечное множество. Это и есть global absorption. Наблюдение из чисел RESULTS_global_absorber:

71.5% стартов доходят до чистого twin (корректный sink);
28.5% проваливаются в absorber'ы с огромным fan-in: до 570 родословных, сходящихся в один absorber (центр $0$).

Fan-in $570 \to 1$ — это счётная стена: массу $570$ различных родословных нельзя уложить в один конечный absorber инъективно, а неинъективность — это коллизия, которую Hall-узел обязан превратить в двигатель. Иными словами, глобальное поглощение при отсутствии новых близнецов вынуждает rigid- цикл (двигатель) через pigeonhole по волокну (пижонхол: конечный ключ не может инъективно пометить бесконечное семейство — см. словарь). Это ровно та красная линия, что зафиксирована в аудите NOPSL §11.

Примечание (закон оплаты). Стоимость одного «чистого» шага масштаба $A$ — налог порядка $\mathrm{tax} \sim 1/\ln A$ (закон оплаты из 17. PaymentLedger). При $A \to \infty$ налог стремится к нулю, но не суммируемо: чтобы удержать $570$-кратный fan-in в конечном множестве, поглощающая система должна оплачивать вход бесконечно, а бюджет старого конечного множества конечен. Это количественная тень того же pigeonhole: конечный кодомен не оплачивает бесконечный домен.

Сборка под EPMI¶

Глобальный узел собирается с законом невозможности вечного двигателя (EPMI, 01) в чистую логическую упаковку, не притворяющуюся доказательством узла:

Теорема 24.3 (no_global_absorption_under_epmi). Если глобальный узел верен (hnode : GlobalAbsorberNode A M0 Engine) и двигатель запрещён (no_engine : ¬ Engine), то глобальное поглощение невозможно: из NoNewTwinAbove M0 и GlobalOldTwinAbsorption A M0 следует False.

Доказательство — одна строка: no_engine (hnode hnoTwin habs). Смысл: раз absorption $\Rightarrow$ engine (узел), а engine запрещён (EPMI, доказан), то absorption при отсутствии новых близнецов ведёт к противоречию — значит выше $M_0$ обязан найтись новый twin. Вся честность здесь в том, что теорема условна на hnode: доказан переход узел + EPMI ⟹ новый twin, но сам GlobalAbsorberNode (Определение 24.2) подан как гипотеза, а не выведен.

Pigeonhole-скелет: где именно открыт Hall-узел¶

Чтобы точно локализовать, что осталось, глобальный узел раскрывается в комбинаторный скелет.

Теорема 24.4 (global_absorber_forces_engine). (Доказана комбинаторика.) Пусть $S$ — бесконечное множество свежих стартов (hInfStarts : S.Infinite), $\mathrm{Codom}$ конечен ([Finite Codom]), и $\mathrm{key} : \alpha \to \mathrm{Codom}$ — паспорт старта $\mathrm{key}\,\gamma = (\text{absorber}\,\gamma,\ \mathrm{NormSig}\,\gamma)$. Если дан узел-насос

\[ \mathrm{pump} : \forall\, \gamma_1\,\gamma_2,\ \gamma_1 \ne \gamma_2 \to \mathrm{key}\,\gamma_1 = \mathrm{key}\,\gamma_2 \to \mathsf{Engine}, \tag{24.2} \]

то $\mathsf{Engine}$.

Доказательство — честный pigeonhole: от противного, если engine нет, то pump запрещён, значит key инъективна на $S$ (Set.InjOn), значит образ бесконечного $S$ конечен, что невозможно (Set.Finite.of_finite_image). Бесконечный домен $\to$ конечный кодомен $\Rightarrow$ коллизия $\gamma_1 \ne \gamma_2$ с одинаковым паспортом — это доказанная часть.

Вся оставшаяся нагрузка — в pump. Именно pump утверждает: «две различные родословные с одним absorber'ом и одной норм-сигнатурой $\Rightarrow$ двигатель». Это и есть Hall-узел — превращение fan-in $570 \to 1$ в rigid-цикл. Он не доказан и подан как явная гипотеза внутри теоремы. Pigeonhole гарантирует коллизию; но что коллизия — это двигатель, а не просто два разных пути в одну точку, — отдельный содержательный факт.

Гипотеза (открытый узел). $\mathrm{pump}$: любые две различные родословные $\gamma_1 \ne \gamma_2$, попадающие в один absorber с совпадающей нормальной сигнатурой, порождают $\mathsf{Engine}$ (rigid-цикл, замыкающийся в вечный двигатель).

План закрытия. (1) Определить норм-сигнатуру $\mathrm{NormSig}$ как каноническую rigid- подпись родословной так, чтобы совпадение сигнатур означало совпадение rigid-структуры лифта, а не просто совпадение остатка $a \bmod P_A$. (2) Показать, что две различные родословные с общей rigid- подписью дают замкнутый цикл сохранения двойки (законы 03. TwoGap, 09. Cycle), высота которого не возвращается лишь по внешнему источнику топлива — то есть цикл несёт двигатель. (3) Свести это к уже доказанному EPMI (01), а не к новому определению Engine := … ∨ Steering (иначе самоликвидация, как в 29. ProductHall). Критическая развилка та же трилемма нормальной формы: сигнатура должна различать родословные (иначе pump тривиально ложен на совпадающих) и при этом склеивать их в один паспорт (иначе кодомен не конечен и pigeonhole пуст).

Патч labelled fan-in: попытка сменить counting-стену на structural¶

Естественно спросить: раз путь через product-core коллизию CoreCollision ⟹ Engine закрыт (separating scale делает CoreSig инъективным, 26. SeparatingScale — коллизии просто нет), нельзя ли обойти Hall-узел pump, заменив глобальный fan-in на локальную детерминированность метки ребра?

Идея (формализована в Engine/LabelledFanIn.lean): убрать примитивный конструктор AbsorberStep (он и давал произвольный many-to-one collapse), оставить только реальные арифметические шаги $\mathrm{RealStep} = \text{active} \lor \text{oldPeel} \lor \text{boundary} \lor \text{SNOL} \lor \text{corridor}$, а поглощение сделать path-свойством $\mathrm{Absorbed}(s) := \exists O,\ \mathrm{OldAbsorber}(O) \land \mathrm{Path}(\mathrm{RealStep}, s, O)$. Тогда цепь такова:

\[\mathrm{GlobalOldAbsorption} \;\Rightarrow\; \mathrm{LabelledFanIn} \lor \mathrm{InfiniteLegalDescent} \quad(\text{König}), \qquad \neg\,\mathrm{InfiniteLegalDescent}\ (\text{EPMI}),$$ $$\mathrm{LabelledFanIn} \;\Rightarrow\; \mathsf{Engine}\quad(\text{local label determinism}).\]

Здесь LabelledFanIn — два разных легальных предшественника одного $V$ с одинаковой меткой ребра $\mathrm{edgeSig}(U_1,V) = \mathrm{edgeSig}(U_2,V)$, а метка конечна при фиксированном $A$.

Что из этого доказано (машинно, LabelledFanIn.lean, стандартные аксиомы). Логический костяк: labelledFanIn_to_engine (из детерминизма метки, без аксиом); вся König-дихотомия absorption_labelled_dichotomy (preds_finite + manyRoute_pred + manyRoute_absorber + descent_from_manyRoute — state-level backward König, без mathlib-König); localLabelDeterminism (настоящая сборка через классификатор тега kind и согласованность $\mathrm{edgeSig}\leftrightarrow\mathrm{kind}$, а не переименование); SNOL-закрытие при regeneration (snolHallSeed_to_engine_of_regeneration, без аксиом) и no-go snolHallSeed_bare_no_go; и мост no_infiniteLegalDescent_of_height — что ветвь EPMI выводится из падения высоты через уже доказанный no_infinite_descent 01.

Примечание (König-ветвь доказана, v3; аудит 8 агентов, независимая перекомпиляция). В первой редакции обе ветви были входами. Затем König-ветвь из недоказанного входа стала теоремой absorption_labelled_dichotomy. Способ — state-level backward König: инвариант $\mathrm{ManyRoute}(V)$ (бесконечно много свежих источников доходят до $V$); при отсутствии labelled fan-in предшественники любого $V$ конечны (preds_finite — метка инъективна на них), поэтому из $\mathrm{ManyRoute}(V)$ пигонхолом получаем предшественника с $\mathrm{ManyRoute}(U)$ (manyRoute_pred); итерация (dependent choice, descent_from_manyRoute) даёт бесконечный спуск, запрещённый EPMI. Mathlib-König не нужен — только два инфинит-фиберных пигонхола. Наивная посылка «у каждого состояния есть предшественник» была ложной (absorber — корень, предшественника не имеет; пример $18 \mapsto (107,109)$) и устранена. Аудит независимо перекомпилировал и подтвердил: доказательство корректно и без контрабанды, красная линия цела, прогресс реальный.

Примечание (SNOL-стена сведена к более лёгкому закону, v4; аудит подтвердил + уточнил). Оставшийся SNOL-компонент доведён до точной сердцевины. Сначала — машинно-проверенный no-go (snolHallSeed_bare_no_go): голая неинъективность SNOL-метки не даёт engine (конкретная 3-состояний модель, где seed есть, а спуска нет). Затем — закон $\mathrm{SNOLHallSeedRegenerates}$ (seed $U_i\to V$ имеет возврат $V\to^+U_i$); вместе с ребром это цикл $U_i\to^+U_i$, запрещённый двигателем (no_cycle_of_height). Это строго легче старой стены «seed $\Rightarrow$ engine». Но аудит вскрыл важную оговорку (машинно-проверенную как regen_under_hdrop_kills_seed): под тем же $\mathrm{hdrop}$, которым закрывается всё остальное, seed и его regeneration взаимоисключающи (ребро + возврат = цикл). Значит $\mathrm{SNOLHallSeedRegenerates}$ выполняется лишь вакуумно, а реальное арифметическое содержание мигрирует в сам $\mathrm{hdrop}$ — существование строго-монотонной ко-высоты на графе $6m\pm1$ (= ацикличность/EPMI), которая здесь не предъявлена.

Итог патча (честно, после двух аудитов). Прогресс реальный: König-комбинаторика закрыта машинно (доказанный ранее вход стал теоремой), а SNOL-стена сведена к строго более лёгкому закону $\mathrm{SNOLHallSeedRegenerates}$ плюс машинно-проверенный no-go. Но это не закрытие Step00, и остаток нельзя сжимать до «одной леммы»: он честно делится минимум на (a) $\mathrm{SNOLHallSeedRegenerates}$; (b) $\mathrm{hdrop}$ — существование ко-высоты/ацикличность на реальном графе, истинный носитель арифметики; (c) четыре компонента инъективности метки (под $\mathsf{Engine}:=\bot$ не бесплатны); (d) сама инстанциация — $\sigma,\mathrm{RealStep},\mathrm{edgeSig}$ не привязаны к $\mathrm{TwinCenterZ}/\mathrm{CoreSig}/6m\pm1$, гипотеза $\mathrm{hAll}$ (всеобщая легальность) ложна на реальном графе, и ни один файл вне модуля эти теоремы не потребляет. Поэтому закрытие $\mathrm{SNOLHallSeedRegenerates}$ само по себе twin_prime_conjecture не закрыло бы. Step00 остаётся sorry.

Пост-аудиторская перестройка: атомизация SNOL (латеральный шаг)¶

Следующий заход (Engine/AtomicSNOL.lean) — структурный рефакторинг, принимающий замечания аудита. Два честных выигрыша: (1) устранена ложная гипотеза $\mathrm{hAll}$ — dichotomy_legal берёт $\mathrm{Legal}:=\top$, и $\mathrm{hAll}$ разряжается истинным термом (а не ложной посылкой); (2) SNOL перестаёт быть atomic-ребром — он становится индуктивной деривацией $\mathrm{SNOLDeriv}$, а SNOLDeriv_expand_or_closes (без аксиом) разворачивает её в atomic-путь или закрывает.

Примечание (аудит: прогресс латеральный, не арифметический). Третий адверсариальный аудит подтвердил корректность и красную линию, но честно оценил вклад как боковой. Во-первых, $\mathrm{hAll}$ снят как ложная гипотеза, но не как обязательство: с $\mathrm{Legal}:=\top$ теоремы говорят о полном типе без фильтра легальности, поэтому легальность переносится в требование, что $\mathrm{AtomicStep}$ построен legality-closed и что $\mathrm{hGlobal}$ легален — а legal-subtype нигде не построен. Во-вторых, SNOLDeriv_expand_or_closes структурно тавтологичен (дизъюнкты в биекции с конструкторами свободного индуктива; composition уже был бесплатен через ReflTransGen.trans) — вся SNOL-арифметика по-прежнему в bridge R8, который definitionally взаимозаменяем со старым входом. В-третьих, R8 — не гипотеза финальной теоремы twin_of_atomicDeterminism_and_absorption: её реальный остаток — $\mathrm{hDet}$ (несёт boundary/old-peel/SNOL-детерминизм, лишь без ярлыка «snol»), $\mathrm{hdrop}$ (ацикличность) и инстанциация. Итог: чистый рефакторинг переносит нагрузку в более аккуратные места, но не приближает к доказательству. Step00 остаётся sorry.

Попытка обойти counting-стену: bad-cover finite descent (оказалась циркулярной)¶

Канонический узел SNOL.SNOLInput — это counting-условие bad.card < carrier.card (плотность, sieve/ parity-стена). Следующий заход (Engine/BadCoverDescent.lean) пробовал обойти счёт динамикой: доказать не «good больше, чем bad», а невозможность bad-cover через конечный energy-спуск. Костяк доказан честно: bad_cover_absurd — если carrier конечен и непуст, а каждый bad имеет строго-меньший по энергии bad-преемник в carrier, то bad-cover невозможен (energy-минимум противоречит спуску). Это настоящий Euclidean-engine на конечном множестве.

Примечание (честно: обход не состоялся — редукция циркулярна). Я сначала заявил, что этот путь не циркулярен (в отличие от SmallCleanSupply). Адверсариальный аудит показал, что это была моя ошибка, и я её принял. Ключ: у конечного carrier есть energy-минимум $m_0$; в нём дизъюнкт «есть меньший по энергии преемник» ложен (ниже минимума ничего нет). Значит при $\neg$Engine вход $\mathrm{bad\_internal\_descent}$ в $m_0$ для каждого $N$ сводится к «$\exists\,t>N$, twin $t$» — то есть к самой цели. Мой довод про «escape через energy-спуск» верен лишь для НЕминимальных элементов и молча игнорировал минимум. Спуск в конечном множестве обязан терминировать на good/twin, поэтому counting/parity-стена перенесена в минимум carrier, а не обойдена. Это зафиксировано машинно: descent_reduction_is_circular + twin_prime_conjecture_of_descent дают $\mathrm{SNOLDescentInput} \Leftrightarrow \text{goal}$ — тот же статус, что SmallCleanSupply.

Итог (латерально). Костяк bad_cover_absurd — реальная малая лемма (пригодится, если появится настоящая инстанциация с energy, структурно убывающей на old-peel/active шагах). Но стена не обойдена: R3 as-hard-as-goal. Красная линия цела (чистая Finset-комбинаторика, никакой плотности в самом костяке). Step00 остаётся sorry.

Obstruction-двигатель: well-founded механика (входы неинстанциируемы, стена подтверждена)¶

Следующий кирпич методологически зрелее: он сам содержит no-go-критерии и ставит бинарный тест. Идея — искать двигатель в положительном obstruction-сертификате: Bad m ⟹ ∃ obs, ObsAt obs m и ObsAt obs m ⟹ Close ∨ меньший obs; тогда well-founded индукция по рангу даёт Bad m ⟹ Close. Абстрактная механика доказана (Engine/ObstructionClosure.lean, без аксиом): obs_closes, mem_bad_closes_of_obstruction_reduction, сборка exists_close_of_nonempty_carrier_and_bad_engine, снятие engine-ветки goal_all_of_exists_close_all. Чистая well-founded логика, без арифметики простых.

Примечание (главный аудитный тест кирпича — результат отрицательный, подтверждён аудитом). Кирпич сам формулирует no-go (§13, §16): двигатель работает только если SNOL.bad имеет положительную obstruction-семантику. Проверка кода (исчерпывающий grep): в базе нет def bad/ def good/def carrier/Obs/LocalObstruction. Реальный узел SNOL.SNOLInput использует bad, carrier : Finset ℕ как экзистенциально-квантифицированные множества с единственным содержательным условием bad.card < carrier.card (counting), а survivor тянется из survivor_of_not_covered — чистый счёт. Значит SNOL.bad — counting-объект, а не obstruction; по критерию §16 входы U1/U2 неинстанциируемы без цели/counting, двигатель на реальном узле не запускается.

Примечание (даже построенный obstruction циркулярен в терминале). Obstruction для 6m±1 уже частично построен: ObsAt = old-peel/active ребро с большим простым делителем, rank = высота-центр. Шаги редукции U2 доказуемы нециркулярно (cofactor_is_center, old_peel_height_drop, active_descent_height — catch есть ступенька вниз, не стена). Но в ранг-0 терминале (clean-центр с простыми сторонами) обе спускающие ветви regeneration_dichotomy исчезают, остаётся ровно «это twin» — U2-терминал Close ∨ меньший obs сводится к Close ∨ ничего = цель. Та же circularity-подпись, что машинно зафиксирована в BadCoverDescent.descent_reduction_is_circular и ConcreteComponents.smallCleanSupply_iff_goal (обе: вход ⟺ цель). Плюс orientation-стена Step00Close: спуск даёт twin ниже старта, а нужен выше N.

Итог (по §16 кирпича, честно). Абстрактный obstruction-двигатель корректен, axiom-free и переиспользуем, но его содержательные входы к SNOL.bad не привязываются. Двигатель добавляет реальную лемму спуска и более точную локализацию стены (она бьёт при построении ObsAt для clean prime-sided центра, ещё до запуска абстрактной машины), но ничего не закрывает. Итог аудита подтверждён: SNOL.SNOLInput — настоящая density/counting/parity стена. Красная линия цела. Step00 остаётся sorry.

Many-unresolved collision: массовое семейство вместо одного terminal (тоже циркулярно)¶

Следующий кирпич пробует не закрывать один terminal (это уже схлопывалось в цель), а закрыть массовое семейство unresolved terminals через pigeonhole на конечной подписи + local determinism: NoNewTwinAbove N ⟹ ∞ high starts ⟹ (many old-absorbed ∨ many unresolved) ⟹ Engine ∨ TwinAbove.

Абстрактный комбинаторный костяк доказан (Engine/ManyUnresolved.lean, std аксиомы, аудит подтвердил соундность): infinite_split, infinite_two_same_sig (pigeonhole: ∞ + конечная подпись ⟹ два разных с равной подписью), сборка close_of_highStarts → twin_prime_conjecture_of_engine. Чистая переиспользуемая комбинаторика.

Примечание (я переоценил — аудит поправил; маршрут циркулярен, как шесть предыдущих). Сначала я заявил, что нетерминальные случаи U4 (active/oldPeel collision) закрываются через active_component_determinism/oldPeel_component_determinism. Это ошибка, и я её принял: эти леммы доказывают другое — one-step детерминизм над общим base V (два предшественника одного V совпадают), они не берут два разных старта m₁≠m₂, не дают Close, и здесь даже не импортированы. Pigeonhole-collision общего base не даёт — направление противоположное. Значит U4 циркулярен везде, не только в терминале: машинно goal_implies_U4 (цель разряжает U4). Плюс U2 (split old-absorbed/unresolved) требует counting — знать, что unresolved-класс бесконечен, это ровно bad.card < carrier.card = SNOL.SNOLInput; а U1 (single clean-центр из carrier_nonempty_above) не даёт бесконечного семейства на фикс. масштабе.

Итог. Костяк — реальная комбинаторика, маршрут ещё точнее локализует стену (U2-split = caught/survivor = SNOLInput; U4-collision = цель). Но не закрывает: circular overall, как шесть предыдущих. SNOL.SNOLInput подтверждён как настоящая density/counting/parity стена. Красная линия цела. Step00 остаётся sorry.

Теорема высшей энергетической несовместимости (4 канала — соундная оболочка)¶

Восьмой кирпич обобщает предыдущий до четырёх энергетических каналов, добавляя явный DescentSeed (запрещённый бесконечный legal descent). Центральная теорема higher_energy_incompatibility_on_euclidean_path — чистая комбинаторная несовместимость: бесконечное семейство high-starts не может избежать всех четырёх каналов (Close / DescentSeed / OldAbsorbed / Unresolved) при ¬Close, ¬DescentSeed (EPMI) и закрытии обеих массовых веток. Доказано (std аксиомы), + Step00-специализация.

Примечание (соундно как утверждение, но стену не двигает — аудит подтвердил). Кирпич сам верно замечает (§9), что теорема «не циркулярна сама по себе» — оболочка честна. Но продвижения нет, и аудит это подтвердил вплоть до машинной проверки: (1) DescentSeed-канал декоративен — hNoDescent (EPMI) делает его тождественно пустым, он гасится мгновенно и не участвует в замыкании (аудит даже доказал, что 4-канальная теорема выводится из 3-канальной вычёркиванием мёртвого дизъюнкта); (2) содержательные входы hOutcome (U2) и hUnresolvedManyCloses (U4) — те же стены, что в прошлом аудите: U2 требует counting (= SNOL.SNOLInput), U4 циркулярен (goal_implies_U4).

Итог. Соундная комбинаторная оболочка несовместимости, ещё точнее раскладывающая исходы на каналы, но ничего не закрывает: DescentSeed пуст под EPMI, U2/U4 — прежние стены. SNOL.SNOLInput подтверждён. Красная линия цела. Step00 остаётся sorry.

Взвешенная энергия долга: реальный движок, но promotion мизориентирован¶

Девятый кирпич — самый математически содержательный из всех. Лексикографическая энергия $Energy(x) = (DebtEnergy(x), LocalFuel(x))$ со взвешенным долгом $DebtEnergy(D) = \sum_{a\in D}(B+1)^{rank(a)}$; internal-ход роняет $LocalFuel$, promote-ход роняет $DebtEnergy$ (замена focus-долга на kids строго меньшего суммарного веса). Оба уменьшают лекс-энергию, вечный путь запрещён well-foundedness.

Доказано (Engine/HigherEnergy.lean, std аксиомы; lexNat_wf и no_live_state_if_closes_or_moves_down вообще без аксиом): lexNat_wf, no_live_state_if_closes_or_moves_down, и — настоящая арифметика весов — debtEnergy_decreases_of_weightedReplacement, kids_weight_lt_focus_of_rank_bound ($B\cdot(B+1)^r < (B+1)^{r+1}$), главная теорема + позитивная форма. Это не пустая оболочка, а реальный переиспользуемый descent-каркас.

Примечание (аудит: движок реален, но вход мизориентирован — линия умирает честно). Единственное узкое место (§22 кирпича) — step00_promotion_is_weightedDebtReplacement. Аудит показал, что на графе $6m\pm1$ он не инстанциируем, и причина резкая: вся реально-арифметическая динамика идёт вниз по высоте/центру (active_descent_height $n<m$, old_peel_height_drop $t<n$, RankDescent $r\to r-1$), а PromotePass требует $A < A'$ — вверх. Forward-хода вверх у движка нет. Повышение $A\to A'$ растит множество старых простых (примориал монотонен) ⟹ promotion добавляет долг (refuel), а не гасит — а weight-увеличивающий ход не является replacement: тип структурно запрещает подделку (машинно проверено refuel_is_not_weightedReplacement). Любой $rank$, при котором ход вверх ронял бы вес, уже утверждает, что спуск оканчивается близнецами = цель (та же подпись, что smallCleanSupply_iff_goal). Плюс repeated_level_signature_closes — циркулярный labelled-fan-in, а LocalFuel-граница прячет counting = SNOL.SNOLInput.

Итог. Реальная weighted-energy математика и корректный well-founded запрет вечного пути — самый чистый каркас в дереве. Но нагрузка честно в одном месте, и оно мизориентировано: все долг-снижающие ходы идут вниз, а promotion — вверх; на графе $6m\pm1$ promotion лишь перезаправляет путь, не гасит долг. Линия «умирает честно» по собственному критерию кирпича (машинно зафиксировано). Net = та же стена в энергетической одежде. Красная линия цела. Step00 остаётся sorry.

Euclidean Tower: движок как инверсный предел (fixed-center вакуумен)¶

Десятый кирпич смотрит на движок концептуально по-новому: не конечный движок едет через ∞ уровней, а сам движок — бесконечная совместимая башня конечных теней (инверсный предел): уровень $A$ даёт тень $State\,A$, restriction $B\to A$ забывает информацию, башня — совместимый выбор состояния на каждом уровне.

Реальный арифметический факт доказан (Engine/HigherTower.lean, std аксиомы, не counting): allClean_forces_side_le_one — центр, чистый на всех уровнях ($\forall A,\ CleanZ\,A\,m$), не может иметь сторону $\ge 2$, потому что чистота-навсегда запрещает любой простой делитель (взять $A=q$), а число $\ge 2$ имеет $\mathrm{minFac}$. Это конечность множества простых делителей, не плотность.

Примечание (fixed-center башня вакуумна — вскрыто при формализации, аудит подтвердил). Кирпич сам подозревал (§16), что fixed-center «too strong». При формализации причина оказалась резче: no_badTower доказан, но вакуумно — поля bad-state clean ($\Rightarrow \forall A\,CleanZ$) и side_hi (сторона $\ge 2$) взаимно противоречивы. Противоречие не «clean-forever ⟹ twin» (как задумывал кирпич), а «clean-forever ⟹ side ≤ 1»; поле bad (не-twin) даже не используется (проверено grep'ом). При этом на отдельном уровне bad-state существует (машинно badState_inhabited_single_level: центр 4, стороны 23 и 25=5² — не twin) — пустота это свойство именно инверсного предела. Значит force-лемма NoTwin ⟹ BadTower не «too strong», а неверна (посылка недостижима: башни нет никогда).

Итог. Инверсно-предельный взгляд — правильный объект, а fixed-center факт реален (конечность простых делителей, красная линия цела) — но true-but-inert: «центров, чистых навсегда, не существует» несёт ноль twin-содержания. Реальная надежда (§17–19) — moving-center башня ($m_A \to \infty$) и недоказанная relTower_stabilizes_or_forces_twin; по §19 самого кирпича без стабилизации/collision это снова orientation/carrier стена (форсировать стабилизацию = инфинитарный pigeonhole = counting). Step00 остаётся sorry.

EngineTower без traversal: обходит orientation-стену, но recurrence тоже вакуумна¶

Одиннадцатый кирпич — архитектурно самый продуманный: он избегает orientation-стены, не требуя, чтобы конечный движок проезжал бесконечную башню (= вечный двигатель). Вместо traversal — inverse-limit через компактность конечных префиксов + moving-center дихотомия: NoTwin ⟹ все префиксы ⟹ (компактность) EngineTower ⟹ RecurrentCenter ∨ CrossLevelCollision. Реальный факт доказан (Engine/EngineTower.lean, std аксиомы, не counting): unboundedClean_forces_side_le_one.

Примечание (кирпич надеялся уйти от вакуумности — но recurrence тоже вакуумна; аудит подтвердил машинно). После прошлой башни кирпич надеялся, что recurrence (центр на неограниченных уровнях) слабее fixed-center clean-forever и потому не-вакуумна. Это не так. Для простого делителя $p$ стороны взять $B=p$, получить $A\ge p$ с $CleanZ\,A\,m$, и $p\le A$ ⟹ запрет. Значит unbounded-clean запрещает любой простой делитель ⟹ $side \le 1$ — та же ловушка. Поэтому no_recurrentEngineTower вакуумен: противоречие «recurrent ⟹ side ≤ 1», а не «recurrent ⟹ twin»; поле bad в доказательствах не используется (проверено grep'ом — ноль вхождений). Ослабление recurrence логически реально, но бесполезно: для $side \le 1$ хватает одного чистого уровня $A\ge q$ на каждый простой $q$, что recurrence и даёт через $B=q$.

Итог (честно, с частичным кредитом — аудит: net = прогресс формы). Traversal-avoidance — реальный выигрыш формы: маршрут genuinely избегает orientation-стены, которая убила weighted-debt движок (кирпич 7), и машинно доказывает, что recurrence-escape вакуумен (чего прошлая башня лишь подозревала). Но counting-стена не тронута: recurrence вакуумна, поэтому вся нагрузка в escape/collision входах (§18 C/D/E) — hRepeat (pigeonhole по конечной подписи = counting = SNOLInput), hCollisionClose (cross-level labelled-fan-in = та же fan-in стена, где snolHallSeed_bare_no_go уже показал ловушку), и hForce/компактность (finite branching + скрыто требует m<A²). Orientation-стена обойдена, counting-стена осталась. Красная линия цела. Step00 остаётся sorry.

Стена чётности как теорема (негативный результат, не доказательство близнецов)¶

Двенадцатый кирпич делает принципиально иное, чем предыдущие одиннадцать: он не пытается закрыть близнецов, а формализует саму стену как теорему (Engine/ParityBarrier.lean, минимальные аксиомы, часть — вообще без аксиом). Схлопнув пару в один объект TwinBlock и введя «сито-вид уровня $A$» ($\mathrm{view}\,A$), доказываем:

parityBlind_cannot_certify_twin — сердце стены: сертификат, зависящий лишь от конечного $A$-вида (parity-blind), корректный и при ambiguity (два $A$-эквивалентных блока, один twin, другой нет) ⟹ $\bot$. Конечный вид не может отличить twin от не-twin;
sound_cert_requires_cofinal_information — корректный сертификат при ambiguity на каждом уровне требует cofinal-информации (не факторизуется через конечный вид);
finite_sieve_engine_cannot_cross_barrier, parity_barrier_model_no_finite_view_decides_twin (модельная форма), finite_twins_contradiction_requires_cofinal_cert;
exists_clean_nonTwin_block — стена не вакуумна: clean-non-twin блок существует ($m=4$, сторона $25=5^2$). Мы не утверждаем существование clean-twin блока — это была бы контрабанда близнецов.

Плюс reverse-engine (Engine/ReverseTower.lean): no_reverseAncestorTree_of_barrier — абстрактное reverse-противоречие через pigeonhole повтора cut-подписи на обратном луче (König-ветвь).

Примечание (это доказательство ограничения, а не близнецов). Кирпич честно не утверждает twin primes. Он превращает стену чётности из интуиции в машинно-проверенную теорему и делает требование к её пересечению точным: любой Step00-сертификат, пересекающий стену, обязан предъявить cofinal-информацию (видеть бесконечно далеко), а не быть finite-sieve движком. Step00-инстанциация (step00_reverseBarrier = cross-level labelled-fan-in; noTwin_forces_reverseAncestorTree = где возвращается counting) — входы, не предъявлены. Step00 остаётся sorry.

Итог. Впервые за одиннадцать заходов — не провал очередного обхода, а позитивный негативный результат: стена чётности формализована как теорема, а точное требование к её пересечению (cofinal, не finite-sieve) — доказано и аудируемо. Это не приближает к близнецам, но делает границу невозможного строгой. Красная линия цела. Step00 остаётся sorry.

Above-конфликт порядков: искать противоречие в «Above», а не в «Twin»¶

Тринадцатый кирпич предлагает изящную идею: искать противоречие не в хвосте NoTwinAbove(max T), а в порядковом конфликте — engine-порядок $T_1 <_{\mathrm{eng}} T_2 <_{\mathrm{eng}} T_3$, но натуральный порядок центров $center(T_1) < center(T_3) < center(T_2)$ («Twin #3 оказался между Twin #1 и Twin #2»). Если это внутренние настоящие twin'ы, а engine-порядок независим — это не-хвостовое противоречие.

Доказано (Engine/AboveConflict.lean, минимальные аксиомы): вся логика порядка — no_above_conflict, contradiction_of_twin_order_conflict, twinGap_not_pierced, no_twin_between_consecutive, contradiction_of_finiteTwinOrderAttack.

Примечание (машинный диагноз ловушки — маршрут сам по себе не новый). Кирпич честно признаёт (§17), что вся order-логика тривиальна (следствие above_sound), а единственный содержательный вход — step00_forces_above_conflict (finite twins ⟹ конфликт), и он рискует схлопнуться в NoTwinAbove(max T). Я зафиксировал ловушку машинно: (1) definitional_above_conflict_impossible — если $\mathrm{Step00Above} := center X < center Y$, конфликт построить нельзя (маршрут мёртв); (2) above_conflict_route_is_trapped — для любого sound above-порядка AboveConflict невозможен. Значит step00_forces_above_conflict требует построить несуществующий объект: он либо ложен, либо его «конфликт» на деле предъявляет новый twin внутри интервала (= TwinAbove внутреннего gap = сама цель). В обоих случаях это переформулировка, а не обход.

Итог. Идея красивая (перенести противоречие в порядок), но машинно доказано, что при sound-порядке конфликта не существует, поэтому step00_forces_above_conflict не может быть новым ресурсом — он эквивалентен предъявлению twin в интервале. Красная линия цела. Step00 остаётся sorry.

Jump engine и cut-barrier: рассуждать по разрезам, а не по посещённым уровням¶

Четырнадцатый кирпич уточняет физику двигателя: он может тратить энергию быстрее и перепрыгивать уровни. Значит нельзя строить аргумент на требовании «посетить каждый уровень» ($\forall A\ \exists k:\ \mathrm{level}_k = A$) — оно ломается уже на $\mathrm{level}_k = 2k$ (cofinal, но нечётные уровни не посещаются).

Правильная замена: не посещать уровень, а проецироваться на каждый разрез (cut). Для high-level state на уровне $B$ и cut $A_0 \le B$ есть конечная подпись $\mathrm{CutSig}(A_0)$; если обратный луч уходит вверх (cofinal), проекций на $A_0$ бесконечно много, а $\mathrm{CutSig}(A_0)$ конечен — подпись повторяется, и повтор форсит $\mathrm{Close}$.

Доказано (Engine/JumpBarrier.lean, минимальные аксиомы): paidJump_decreases_energy (оплаченный скачок строго роняет энергию — больший расход лишь усиливает терминацию), no_infinite_strict_energy_descent, jump_breaks_visitsEveryLevel (контрпример $2k$ — машинный), repeated_cutSig_on_jumpReverseRay (jump-совместимый пиджонхол ∞→конечный тип), no_jumpReverseRay_of_cutBarrier (нет луча при cut-barrier и ¬Close), и no_jumpAboveGapConflict (скачок через twin-gap + возврат внутрь = порядковое противоречие, честно связано с TwinGap из above-раздела).

Примечание (машинный диагноз ловушки — red-tests §19 кирпича). Абстрактный no-go корректен и не вакуумен (луч cofinal с конечной подписью — реальный объект). Но Step00-инстанциация держится на двух недоказанных входах: step00_jumpReverseBarrier (повтор cut-подписи ⟹ Close) — это cross-level labelled fan-in, тот же trap, что snolHallSeed_bare_no_go; и noTwin_forces_jumpReverseRay — red-test #5 прямо запрещает опираться на SNOL.SNOLInput/CleanDensityBelowA2. Я зафиксировал это машинно: jump_route_is_trapped показывает, что противоречие выводимо лишь при обоих входах, а red_test_forceRay_is_supply разворачивает force-ray в чистую supply-форму «NoTwin → NoEngine → ∃ ray» — та же форма, что supply-теорема SNOL (это Iff.rfl-разворот формы, аналогия, а не импорт SNOL: машинно доказана эквивалентность форм, а не тождество объектов). Пиджонхол/энергия (доказанное) сами по себе не дают ни barrier, ни force-ray.

Итог. Кирпич даёт правильную форму рассуждения (разрезы вместо посещённых уровней) и реальные платные/пиджонхол-леммы, но два содержательных входа — та же counting/fan-in стена. Красная линия цела. Step00 остаётся sorry.

Скрытый двигатель и платная динамика: где может прятаться второй двигатель¶

Пятнадцатый кирпич задаёт аудит: если Step00 не закрывается локально, «второй двигатель» может прятаться в четырёх обличьях — (1) промоушен масштаба $A\to A'$, (2) регенерация carrier, (3) неучтённая инерция/кредит, (4) клонирование ветвей. Против каждого — платный закон: если всё оплачено из общего потенциала $\mathrm{Total}$, бесконечного/cofinal/клонирующего движения нет.

Доказано (Engine/PaidDynamics.lean, минимальные аксиомы): PaidDynamics c strict_drop, path_budget, steps_bounded, no_infinite_paid_run (нет бесплатной инерции); телескоп monotone_nat_telescope_sub_le_sum_sub (sorry кирпича закрыт) и no_cofinal_paid_jump_path (нет ускорения к cofinal-уровням оплаченными скачками); no_infinite_noFreeInertia_run (инерция/кредит внутри $\mathrm{Total}$); no_two_live_children_from_unit (один live-юнит с $\mathrm{Total}=1$ не становится двумя — запрет клонирования); и абстрактная сборка contradiction_from_regeneration.

Примечание (машинный диагноз ловушки — §6/§34/§36 кирпича). Платные законы реальны и доказаны, но они лишь локализуют скрытый двигатель. Любой бесконечный Step00-механизм обязан использовать regeneration_forces_close ($\text{InfiniteCarrierRegeneration} \Rightarrow \exists A,\ \mathrm{Close}$), и кирпич прямо говорит: этот вход = supply clean carrier at scale = SNOL.SNOLInput. Я зафиксировал это машинно: regeneration_to_close_is_supply разворачивает вход в чистую supply-импликацию, а paid_laws_do_not_close_regeneration строит нетривиальную бесконечную регенерацию (масштаб $k$) — значит платные законы её не запрещают (в InfiniteCarrierRegeneration нет поля $\mathrm{Total}$), запрет может дать лишь supply-вход.

Итог. Аудит правильный и полезный: он машинно доказывает, что скрытого двигателя нет в масштабе, инерции или клонировании — и что весь остаток сжат в одну регенерационную supply-теорему той же формы, что SNOL.SNOLInput (эквивалентность форм — Iff.rfl; тождество объектов не импортируется, это аналогия). Это не обход, а точная локализация стены. Красная линия цела. Step00 остаётся sorry.

ClosedUniverse: двигатель не покидает вселенную¶

Шестнадцатый кирпич формализует необходимую гигиену любого пути-аргумента: прежде чем применять энергия/cut/подпись-инвариант вдоль траектории, нужно доказать, что двигатель остаётся во вселенной ($\mathrm{Universe}\ x \to \mathrm{Step}\ x\ y \to \mathrm{Universe}\ y$). Если шаг меняет масштаб/вселенную и создаёт ресурс, он оплачивается ($\mathrm{Total}_B\ y + \mathrm{Work} + \mathrm{UniverseChangeCost} \le \mathrm{Total}_A\ x$) или наступает Close.

Доказано (Engine/ClosedUniverse.lean, минимальные аксиомы; universe_along_path без аксиом): universe_along_path (сохранение вселенной вдоль всего пути); ClosedPaidDynamics c strict_drop, path_budget, steps_bounded, no_infinite_closed_paid_run (остаётся во вселенной + оплачен ⟹ нет бесконечного run); scale-indexed closedPaidScale_strict_drop (с UniverseChangeCost); closed_paid_or_closes_no_infinite_run (дихотомия §25: под глобальным ¬Close paid-or-closes вырождается в paid); и universeRefuel_is_paid_violation (refuel = ровно отрицание paid, машинно).

Примечание (машинный диагноз ловушки — §36 кирпича). Абстрактные законы корректны и не вакуумны. Но Step00 инстанциирует no_infinite_closed_paid_run лишь если доказан paid для каждого шага, включая promotion и carrier-regeneration. Кирпич прямо (§36) называет step00_promotion_paid_or_closes «самой опасной теоремой» и «самым вероятным скрытым двигателем». Я зафиксировал это машинно: universe_preservation_alone_does_not_bound_run строит замкнутую динамику на $\mathbb{N}$ (шаг $x\mapsto x{+}1$, вселенная = всё, Total растёт) — бесконечный путь существует, значит сохранение вселенной само по себе бесполезно без платы; вся сила в paid. А promotion_paid_or_closes_is_the_wall разворачивает нужный вход в точности в поле paid_or_closes — тот же, что orientation-стена (HigherEnergy: promotion misoriented = refuel) плюс supply-стена (PaidDynamics.regeneration_to_close_is_supply).

Итог. Кирпич даёт корректную и важную гигиену (сначала докажи сохранение вселенной, потом инвариант) и реальные closed-paid законы, но единственный опасный вход — promotion_paid_or_closes — это ровно стена рефьюэла/supply. Красная линия цела. Step00 остаётся sorry.

Структурная аналогия P/NP: почему стена имеет природу «сертификат против поиска»¶

Конкретный граф 6m±1 (ConcreteStep00Graph: State = center/defect/absorber, RealStep = clean/boundary/peel/absorb) обнажает структуру, изоморфную одной грани P vs NP. Это аналогия, а не доказательство P ≠ NP и не доказательство близнецов; она формализована в §12 PvsNPAnalogy.

Прямой ход — сторона P (доказано). Шаг двигателя RealStep детерминирован, а lexRank строго падает на каждом ребре. Отсюда pathN_len_le_lexRank: любой путь длины $n$ из $X$ имеет $n \le \mathrm{lexRank}(X)$. Значит генеалогия «проверяется дёшево» — её длина ограничена координатой старта, а легальность проверяется пошагово (VerificationEasy, verificationEasy_always). Это ровно EPMI в вычислительной одежде: прямой двигатель терминирует за полином.
Обратный ход — сторона NP (доказано). Восстановить генеалогию назад — это поиск в ветвящемся дереве предков (ManyRoute, ReverseAncestorTree): у состояния много предков, и «путь двигателя» надо найти среди экспоненциально многих. Ключевой машинный факт: конечный (полиномиальный) ключ проекции на бесконечной семье не восстанавливает состояние — finite_key_cannot_determine_state_on_infinite (SearchNotCompressible). То есть сжать обратный поиск в сертификат нельзя без потери информации.
Аналогия как теорема, а не лозунг. verify_easy_but_search_not_compressible предъявляет обе стороны одновременно: каждая генеалогия проверяется дёшево и поиск не сжимается в конечный ключ. Асимметрия «проверка легка / поиск не сжимается» здесь — доказанный факт графа.

Узел PolyCertificateSuffices (= несводимый вход). Оставшаяся стена близнецов, переведённая в P/NP-термины: «конечный (полиномиальный) сертификат обратного пути достаточен, чтобы решить, что коллизия двух генеалогий = настоящий евклидов цикл». Это буквально SemanticFlowLedgerCollisionResolves в другой одежде. branch_closes_if_polyCertificateSuffices доказывает: если узел верен И семья бесконечна, ветка схлопывается — но узел не предъявлен. И §12 объясняет, почему он не даётся даром: сертификат теряет информацию (SearchNotCompressible), поэтому «сертификата достаточно» — это дополнительная арифметика fan-in, а не следствие сжатия.

Итог. Прямой двигатель — P (быстрая проверка/терминация), обратное восстановление генеалогии — NP (ветвящийся поиск), а несводимый узел близнецов = «достаточен ли полиномиальный сертификат обратного пути». Программа не решает P vs NP и не опирается на него; она лишь машинно локализует стену распределения в форме, изоморфной «сертификат против поиска». Красная линия цела. Step00 остаётся sorry.

Фабрика потоков из чистых стартов: близнецы сведены к одному входу¶

Цепочка из семи factory-кирпичей (встроена в ConcreteStep00Graph) закрыла конструктивно всё, что раньше было тремя позитивными входами:

infiniteCleanStarts_closed — бесконечность чистых стартов закрыта конструктивным примориалом ($m = (N{+}1)\cdot P(A)$ чист по CRT-тождеству, carrier_nonempty_above). Это structural counting, не распределение простых — красная линия цела.
Well-founded builder — из локального нормализатора сильной рекурсией по центру строится настоящая генеалогия (ProperRealStep: clean/boundary/peel/absorb), терминирующая в fresh defect / old absorber / old clean centre.
Cofactor-нормализатор (closedProperCofactorNormalizer — безусловен для любого $A$) — из чистого не-twin центра реальная арифметика 6m±1 (композитная сторона ⟹ большой простой делитель ⟹ cofactor_is_center ⟹ меньший 6n±1-кофактор) выдаёт peel-цель.

Вывод (финальная редукция, машинно). twinLowersInfinite_of_lastStep00Obligation — вся близнецовая ветка висит на одном входе TheLastStep00Obligation (существует масштаб и проекции, разрешающие коллизии генеалогий на всех $M_0$).

Обострение: сертификат-вход — это twin-детектор (честность, машинно)¶

Три теоремы вскрывают истинную природу последнего входа:

resolves_iff_key_injective — раз обе резолюционные альтернативы невозможны (цикл — по lexRank, оплата — по shifted-primorial), Resolves proj ⟺ инъективность конечного ключа на admissible-потоках, т.е. «same-key коллизий нет вовсе».
twin_above_of_resolves — Resolves на масштабе $M_0$ предъявляет twin выше $M_0$: иначе twin-bound + доказанная ∞-семья + пиджонхол дают противоречие. ⚠️ Вход не слабее цели на каждом масштабе: любая будущая заявка «доказать Resolves» — замаскированная заявка о существовании twin.
twinLowersInfinite_of_cofinal_resolves — ослабление: достаточно Resolves на кофинально многих $M_0$ (не на всех).

⚠️ Эпизод вакуумности (адверсариальный аудит; починено, полное раскрытие в коммите 420e495). Первая версия фабрики допускала дегенеративный peel: простая сторона $p = p\cdot 1$, а $1 = 6\cdot 0+1$ — peel в центр $0$ существовал без twin-гипотезы (композитная гипотеза у clean_side_composite_big_divisor была мёртвой). Аудит машинно опроверг TheLastStep00Obligation — редукция была ex-falso (вывод «из лжи что угодно», см. словарь), а «twin-детектор» — вакуумным. Заплата: properDiv (делитель собственный) и targetPos ≥ 1 на peel-целях; эксплойт-свидетели аудита больше не компилируются, у twin-центра (обе стороны просты) собственного peel нет — гипотеза ¬TwinCenterZ снова несущая. После заплаты выполнимость узла подлинно открыта (не доказана и не опровергнута).

Параллельная честность для Римана (в RiemannImpossibleEngineOff): offCriticalBridge_iff_RH — вход OffCriticalRiemannEngineBridge эквивалентен RH дословно (factory безусловно невозможна, значит мост выполним лишь вакуумно = нулей нет = RH). Обе ветки теперь честно маркированы: близнецы — вход ≥ цели по-масштабно; Риман — вход = цель.

Передышка перед длинной серией. Следующие кирпичи уже не штурмуют узел — они перечитывают его на разных языках: энергия, вложенные вселенные, швы леджера, информация, причинность. Финал каждого прочтения одинаков и машинно честен: никакая обёртка не опускает содержание ниже старого узла.

Энергетическая форма узла: «не вернулся — плати свежей энергией»¶

Кирпич energy-ledger добавляет энергетическое прочтение того же узла: к семантической проекции прикрепляется конечный тип Energy и токен-функция; правило no_double_spend_resolves требует, чтобы две различные admissible-генеалогии с одинаковым ключом и одинаковым токеном разрешались в строгую альтернативу (возврат/оплата). Доказано (ExtendedFlowEnergyLedger, стандартные аксиомы):

same_key_collision_requires_fresh_energy — раз альтернатива уже сожжена (цикл — lexRank, оплата — primorial), каждая same-key коллизия обязана тратить новый токен;
twinBound_impossible_with_energyLedger — конечность пары (ключ, токен) + ∞-семья ⟹ double spend ⟹ противоречие: «платить вечно» из конечного бюджета нельзя;
twinLowersInfinite_of_energyLastStep00Obligation — энергетическое обязательство ⟹ близнецы.

Честность (машинно, обязательна после эпизода вакуумности):

twin_above_of_energyLedger — energy-ledger на масштабе $M_0$ тоже предъявляет twin выше $M_0$ — энергетический сертификат остаётся twin-детектором;
lastStep00Obligation_of_energy через combinedEnergyProjection_resolves — энергетическая форма факторизуется через старый узел: ledger — это в точности уточнение ключа до Key × Energy, а no_double_spend_resolves (при сожжённой альтернативе) — инъективность комбинированного ключа. Это переформулировка финального узла, не обход: открытость не уменьшилась, вся арифметика теперь живёт в построении energy-ledger'а.

Вложенные вселенные: одностороннее вложение = только спуск¶

Кирпич nested-universes даёт диагностическую геометрию той же коллизии. NestedUniverseEmbedding F_outer F_inner — терминал внешней генеалогии достигает старта внутренней (непустой путь в конкретном графе). Доказано (стандартные аксиомы):

nestedUniverseEmbedding_drops_startRank — одностороннее вложение строго роняет lexRank старта: внутренняя вселенная — подлинно меньшая копия, не цикл (oneWayNesting_is_only_descent);
no_mutuallyNestedUniverses — взаимное вложение механически строит legal-цикл (старт₁ →⁺ терминал₁ →⁺ старт₂ →⁺ терминал₂ →⁺ старт₁) — сожжён lexRank;
no_nestedUniverseChain, no_sameKeyNestedUniverseEngine — бесконечная цепочка односторонних вложений невозможна: rank падает ≥ 1 за шаг, спуск в ℕ конечен;
twinLowersInfinite_of_nestedUniverseLastStep00Obligation — nested-обязательство ⟹ близнецы.

Честность (машинно): nestedUniverseLastStep00Obligation_iff_lastStep00Obligation — nested-узел эквивалентен старому узлу (обе стороны альтернативы уже сожжены); twin_above_of_nestedResolves — nested-резолвер на M0 тоже предъявляет twin выше M0. Итог кирпича: честные исходы same-key коллизии — возврат / оплата / взаимное вложение (все три сожжены) либо конечная цепь строгих вложений; остаток арифметики — «нельзя вечно порождать лишь односторонние вложения, не возвращаясь и не платя».

Сингулярности на шве леджера: две половины аудита¶

Кирпич seam-singularity даёт финальную классификацию same-key коллизии. Сингулярность — коллизия, для которой граф не даёт ни одной легальной реализации склейки (ни возврата, ни вложения в любую сторону, ни оплаты): шов леджера склеил истории, которые реальный граф склеить не умеет. Dangling-вложение — коллизия лишь с односторонним вложением: спуск вместо двигателя. Доказано:

seamCollision_classical_classification — тавтологическая классификация: каждая коллизия несёт возврат / вложение / оплату / сингулярность;
noSingularity_noDangling_resolves_old — аудит-редукция кирпича: нет сингулярностей + нет dangling ⟹ старый резолвер; twinLowersInfinite_of_seamAuditLastStep00Obligation ⟹ близнецы.

Честность (машинно) — взаимная аннигиляция половин. Возврат, взаимное вложение и оплата опровергнуты безусловно, поэтому (ledgerSeamSingularity_iff, danglingOneWayNesting_iff):

noLedgerSeamSingularity_iff — NoSingularity ⟺ «каждая same-key коллизия несёт вложение»;
noDanglingOneWayNesting_iff — NoDangling ⟺ «никакая same-key коллизия не несёт вложения»;
seamAudit_forces_no_collision — вместе ⟹ коллизий нет вовсе;
seamAudit_iff_resolves, seamAuditLastStep00Obligation_iff_lastStep00Obligation — seam-аудит ⟺ инъективность ⟺ старый узел; twin_above_of_seamAudit — опять twin-детектор.

Диагностическая ценность: единственное неопровергнутое локальное явление, которое может нести коллизия, — одностороннее вложение (строгий спуск). Остаток арифметики распался на две named-половины: «запрети голую коллизию» (сингулярность) и «запрети коллизию-со-спуском» (dangling) — но их конъюнкция машинно равна прежней инъективности: иначе сформулированный тот же узел.

Верная проекция: «забывать можно только gauge»¶

Кирпич faithful-projection переводит seam-язык в информационный: конечный ключ имеет право быть неинъективным, но склейка двух различных admissible-историй обязана иметь причинное объяснение (возврат / вложение в одну из сторон / оплата). Доказано:

causalInformationLoss_iff_ledgerSeamSingularity — «потерянная причинная информация» и «сломанный шов» — один и тот же аудит-провал (чистая пропозициональная бухгалтерия);
keyEqualityGauge_iff_noLedgerSeamSingularity — прямая gauge-форма («same key ⟹ та же генеалогия ∨ причинная связь») ⟺ отсутствие сингулярностей;
keyEqualityGauge_noDangling_resolves_old, FaithfulGaugeProjectionPackage, twinLowersInfinite_of_faithfulGaugeLastStep00Obligation — пакет (проекция + 2 сертификата) ⟹ близнецы.

Честность (машинно): gaugePair_iff_resolves и faithfulGaugeLastStep00Obligation_iff_lastStep00Obligation — пара (gauge-верность, no-dangling) ⟺ старый резолвер, obligation ⟺ старый узел; twin_above_of_faithfulGaugePackage — пакет на M0 предъявляет twin выше M0. Информационная формулировка — самая физичная из эквивалентных форм узла: финитный леджер не имеет права терять причинность; но это по-прежнему тот же узел.

Вселенная без энергии: геометрическая опора вместо оплаты¶

Кирпич no-energy формализует «у старой системы нет платёжного канала»: same-key коллизия может опираться только на геометрию (возврат / вложение) или быть маркирована сингулярностью. Кирпич честно избегает вакуумного кодирования Energy := Empty (оно запретило бы само существование потоков). Доказано: noEnergyStableUniverse_resolves_old (тройка условий ⟹ старый резолвер), twinBound_impossible_with_noEnergyStableUniverse, twinLowersInfinite_of_noEnergyStableUniverseLastStep00Obligation ⟹ близнецы.

Честность (машинно): noEnergyStableUniverse_iff_seamAudit — под двумя seam-запретами support-условие вакуумно (коллизий нет вовсе — seamAudit_forces_no_collision), тройка ⟺ пара; noEnergyStableUniverse_iff_resolves, noEnergyStableUniverseLastStep00Obligation_iff_lastStep00Obligation — no-energy-форма ⟺ старый узел; twin_above_of_noEnergyStableUniverse — twin-детектор.

Нет бесконечной компрессии информации¶

Кирпич compression: строгая компрессия = коллизия, чьё единственное объяснение — одностороннее вложение (внутренняя вселенная меньше).

Доказано: strictInformationCompression_drops_rank (каждый шаг компрессии роняет lexRank), no_informationCompressionChain (∞-цепь компрессий невозможна — «сжимать причинную информацию вечно нельзя»), seamCollision_informationCompression_classification (полный классификатор: возврат / взаимное вложение / оплата / сингулярность / компрессия в одну из сторон), twinLowersInfinite_of_informationCompressionLastStep00Obligation ⟹ близнецы. Фикс кирпича: в реверсных случаях ¬Return F₁ F₂ переворачивается в ¬Return F₂ F₁ через Or.symm (сертификат — симметричная дизъюнкция).

Честность (машинно): noStrictCompression_iff_noDangling — запрет компрессии ⟺ запрет dangling-вложений (в обе стороны); compressionAudit_iff_resolves, informationCompressionLastStep00Obligation_iff_lastStep00Obligation — compression-форма ⟺ старый узел; twin_above_of_compressionAudit — twin-детектор.

Информационные атомы; извлечение и смешивание без двигателя¶

Кирпичи atom-extraction и no-free-mixing завершают информационный словарь узла:

exists_informationAtom_of_inhabited — безусловный результат: в любой обитаемой вселенной генеалогий существует информационный атом (генеалогия без строгой компрессии). Доказательство: безатомность даёт Classical.choose-орбиту компрессий = ∞-цепь — сожжена lexRank. Старт — неделимая единица причинной информации.
no_free_information_extraction / no_free_information_mixing — под парой аудита (NoSingularity, NoCompression) нельзя ни извлечь, ни смешать причинную информацию без двигателя/оплаты; sameKeyMixingSquare_forces_engine_or_payment — cross-wiring квадрат (перестановка старт/терминал парами) тоже принуждает к двигателю.
twinLowersInfinite_of_atomicInformationLastStep00Obligation ⟹ близнецы.

Честность (машинно): informationExtractionWithoutEngine_iff_collision, informationMixingWithoutEngine_iff_mixingCollision — «extraction/mixing без двигателя» — это просто same-key коллизия (три запрета выполнены даром: возврат/взаимное вложение/оплата уже опровергнуты), а «позитивные формы» (вывод «двигатель ∨ оплата») под аудитом — ex-falso; atomicInformationLastStep00Obligation_iff_lastStep00Obligation — atomic-форма ⟺ старый узел; twin_above_of_atomicInformationAudit, twin_above_of_noFreeMixingAudit — twin-детекторы.

Стабильная no-engine теория: финальный мета-аудит (объектный уровень)¶

Кирпич stable-no-engine-theory собирает весь информационный словарь в одну структуру StableNoEngineStep00Theory (проекции + стабильность без энергии + без компрессии + без смешивания, на всех масштабах) и доказывает внутренний no-go:

stableNoEnergy_collision_builds_engine — одна same-key коллизия в стабильной no-energy вселенной строит явный двигатель-свидетель (ConcreteEuclideanEngineWitness — legal-цикл);
no_concreteEuclideanEngineWitness — таких свидетелей не бывает (lexRank);
infiniteFlows_impossible_in_stableNoEnergy, stableFiniteTwinTheoryIsImpossible — конечный стабильный ledger не может поглотить бесконечную нагрузку генеалогий;
twinLowersInfinite_of_stableNoEngineTheory, no_finiteTwin_stableNoEngineTheory — теория ⟹ близнецы; теория несовместима с конечностью близнецов.

Фиксы кирпича: ConcreteEuclideanEngineWitness объявлен : Prop; экзистенциал теории — через Nonempty (структура несёт данные).

Честность (машинно): stableNoEngineTheoryExists_iff_lastStep00Obligation — существование стабильной теории эквивалентно старому узлу: диагностические поля (noStrictCompression, noMixing) восстановимы из резолвера, вся тяжесть — в stableNoEnergy; twin_above_of_stableNoEngineTheory — теория на каждом масштабе предъявляет twin (детектор). Итог: «доказать стабильную конечно-twin теорию» = «построить запрещённый двигатель» — красивейшая из эквивалентных форм узла, но узел тот же.

Двойственный аудит: нет опровержения без двигателя¶

Кирпич dual: и опровержение стабильной теории через реальную same-key коллизию — тоже конструкция запрещённого двигателя. LocalStableRefutationAttempt (стабильность + коллизия) ⟹ ConcreteEuclideanEngineWitness (localStableRefutationAttempt_builds_engine) ⟹ невозможно; infinite-load версия — через пиджонхол.

Комбинированный слоган: provingOrRefutingStableTheoryRequiresEngine / noProofOrRefutationWithoutForbiddenEngine — и доказать, и опровергнуть стабильную теорию изнутри = построить двигатель; двигателей нет. Это не метаматематика (не заявление о независимости) — объектный факт архитектуры. Фиксы: data-структуры attempt → невозможность в форме → False.

Честность (машинно): localStableRefutationAttempt_empty — attempt пуст напрямую через seam-честность: поле stable пакует «коллизий нет вовсе» вместе с самой коллизией; двигательный маршрут кирпича — тот же ex-falso, поднятый на поверхность (оба пути — один факт).

Нет внутреннего решения; архитектурно-относительная независимость¶

Кирпич no-internal-decision пакует вывод: InternalStableDecisionAttempt (Prop-индуктив трёх маршрутов: prove / refuteLocal / refuteInfinite) — каждый строит двигатель (internalStableDecisionAttempt_builds_engine), двигателей нет (noInternalDecisionWithoutForbiddenEngine). Кирпич сам маркирует (§4): это объектный факт, не Гёдель-независимость.

Честность (машинно): «proof attempt» несёт буквально те же поля, что infinite-load «refutation attempt» — дихотомия «доказать/опровергнуть» здесь номинальна (internalStableProofAttempt_empty); все три ветви пусты напрямую через seam-честность (internalStableDecisionAttempt_empty_directly).

Кирпич relative-independence — сильнейшая честная форма: если сертификаты внешней системы факторизуются через Step00-попытки (Step00DecisionInterface, Step00MediatedStatement), то системе недоступны ни доказательство, ни опровержение (architectureRelativeIndependence, mediatedStatement_noProof_noRefutation); охват явно ограничен (§3–§4: не ZFC/PA/Lean). Честность (машинно): translation_to_decisionAttempt_iff_empty — транслятор в (пустой) тип попыток существует ⟺ домен пуст: гипотеза моста уже содержит вывод; сила утверждения — целиком в предпосылке медиируемости.

Фиксы кирпичей: SomeConcreteEuclideanEngine → ∃-Prop; attempt-невозможности → → False.

Внешний принцип вселенной: «двигатель доказывает себя» = противоречие¶

Кирпич external-universe: три «внешних принципа» (strict / no-energy / finite-energy обязательства) как входы дают близнецов (*_generates_twins); попытка самозаверения (интернализация принципа как Step00-попытки) строит запрещённый двигатель: no_boundaryCrossingSelfProof, perpetualEngineSelfProofIsContradiction, externalPrincipleGeneratesButDoesNotSelfCertify. Фикс: self-proof структуры — : Prop.

Честность (машинно): boundaryCrossingSelfProof_iff_and_not — self-proof ⟺ P ∧ ¬P: интернализация в пустой тип попыток — это в точности отрицание, потому запрет самозаверения тавтологичен и верен для любого P (и для истинных); externalOnlyUniversePrinciple_iff — «external-only» не добавляет к P ничего. Несущая часть — только уже известные generates_twins-импликации. Бонус: закрыто недостающее звено семейства — strictLastStep00Obligation_iff_lastStep00Obligation (strict-обязательство ⟺ старый узел, через strictResolves_iff_resolves).

⚠️ Первопричина как корневая аксиома (намеренно; карантин)¶

По решению автора первопричина включена в структуру намеренно: корневая аксиома репозитория — step00FirstCause : Step00FirstCause, структура события 0 → 1 из трёх полей: origin (маркер сингулярности; True — до первого кадра языка нет), firstFrame (первый причинный кадр; True), causalBoundary (содержательная граница = TheStrictLastStep00Obligation). Прежняя causal-closure «аксиома» — теперь теорема из первопричины (step00CausalClosure := step00FirstCause.causalBoundary); весь условный слой ниже не изменился.

Мотив: интернализация первопричины доказуемо невозможна (внутренняя первопричина = запрещённый двигатель), потому она принимается извне — и теперь это оформлено как явный корень архитектуры, а не как техническая запись узла.

Честность (машинно): step00FirstCause_iff_causalClosure — маркеры несут True, сила декрета не изменилась, изменился корень происхождения (и имя аксиомы в machine-таинте — следе аксиомы в списке зависимостей декларации, см. словарь: step00FirstCause, заражено ровно 20 деклараций — прежние 19 + сам step00CausalClosure).

Эпистемика первопричины: есть — узнать нельзя — знание финитизирует¶

Замысел автора достроен машинно (§8 карантинного модуля — карантин, единственное место, где живёт аксиома (см. словарь); вся эпистемика, кроме двух помеченных теорем, аксиомо-свободна):

Есть — step00FirstCause (аксиома, принята намеренно).
Узнать нельзя — теорема (cause_unknowable): внутреннее знание причины = внутреннее выведение границы = boundary-crossing self-proof = построение вечного двигателя (knowledge_builds_perpetualEngine) — а их нет (lexRank).
Знание финитизировало бы близнецов (knowledge_finitizes_twins) — целевая формула; ⚠️ честность: маршрут через невозможный двигатель (ex falso), потому рядом обязательный companion knowledge_proves_anything (из знания следует и бесконечность — знание взрывает всё); содержательная форма без взрыва — дихотомия unknowable_or_twins_finite, где левый дизъюнкт — настоящая теорема.
«Близнецы бесконечны, потому что узнать нельзя» — суть, машинно: twins_infinite_of_noEngine_and_boundary (аксиомо-свободна!) — отсутствие двигателей (= непознаваемость, подлинная контрапозиция unknowable_of_noEngine) + принятая граница ⟹ близнецы; гипотеза «двигателей нет» потребляется по-настоящему (двигатель-свидетель строится из коллизии и убивается именно ею). lexRank поставляет её как теорему: непознаваемость и близнецы — два следствия одной причины, и вывод близнецов видимо проходит через непознаваемость (twins_because_unknowable, AXIOM-TAINTED через границу). Честная оговорка: «потому что» = «через общую причину и несущую лемму»; тяжесть существования — по-прежнему в принятой границе: непознаваемость одна, без границы, близнецов не доказывает (иначе они были бы теоремой).

Конечное знание о близнецах — почти ничто (строго, Engine/FiniteKnowledgeBarrier). По запросу автора соединены стена чётности и эпистемика — безусловные теоремы (ядро — только propext): knowledge_forces_pure_class — конечная корректная система может знать близнеца только если весь его конечный класс — близнецы (знание — про класс, не про число); mixed_class_twin_unknowable — близнец со смешанным классом принципиально непознаваем; trivialView_knows_nothing / trivialView_infinitude_unknowable — для тривиального вида знание пусто и бесконечность непознаваема (конкретно, безусловно); infinitude_unknowable_of_eventually_mixed — при хвостовом смешении классов бесконечность не удостоверяется; two_walls_one_nature — две стены, одна природа: изнутри конечного вида не видно близнецов, изнутри системы не видно первопричины. Бесконечность близнецов и первопричина — внешнее знание для любой конечной/внутренней системы. Честная граница: смешанность классов нетривиального вида на конкретных уровнях — арифметический вход (как и у стены).

Непротиворечивость (растяжки §9). T + step00FirstCause непротиворечива ⟺ база не опровергает узел. Три мира: узел истинен (аксиома лишняя, близнецы доказаны) / независим (теория непротиворечива, но узнать это изнутри нельзя) / опровержим (карантин противоречив, все заражённые теоремы обесцениваются разом). Атака A ≤ 4 уже удалась — независимо от истинности близнецов; декрет живёт в A ≥ 5. Точка взрыва машинно видима: quarantine_inconsistent_if_node_refuted / ..._if_lastObligation_refuted — если узел опровергнут, False выводится именно здесь.

⚠️ Causal-closure как внешняя аксиома (карантин)¶

Кирпич causal-closure-axiom — сознательно аксиомоносный эндпойнт аудита: `axiom step00CausalClosure: TheStrictLastStep00Obligation— открытый узел, *принятый декретом* (намеренное принятие закона аксиомой, не доказательство — см. [словарь](GLOSSARY.md)). Интегрирован в *карантинный* модульEngine/CausalClosureAxiom.lean(единственныйaxiom` репозитория), потому что прямое вливание отравило бы гарантию «зелёное = доказанное».

Карантин машинно отслеживается: узловой верификатор апгрейжен до полного аксиом-трекинга (AXIOM-TAINTED) — заражены ровно 5 деклараций модуля, утечки в основную линию нет; sorryAx — по-прежнему ровно один (twin_prime_conjecture, который через аксиому не замыкается).

Что модуль даёт: twinLowersInfinite_from_step00CausalClosure : TwinLowers.Infinite — условно на аксиоме, не доказательство; аксиомо-свободные части (невозможность самозаверения) уже были в репо. Честность (машинно): causalClosureAxiom_asserts_twins_at_every_scale — аксиома уже утверждает twin на каждом масштабе: декрет не слабее вывода; аксиома ⟺ старый узел.

Status-кирпич (тоже в карантине): два режима — аксиомный (step00AxiomatisedTheoryClosed, AXIOM-TAINTED) и безаксиомный, где остаток в точности causal-closure (pipelineClosesWithoutNewAxiom_iff_causalClosure, Iff.rfl); финальная таблица зависимостей — finalStep00Status. Честность (машинно): nonAxiomaticRemainingObligation_iff_lastStep00Obligation — безаксиомный остаток ⟺ старый узел (заявление «никакая обёртка не опускает содержание ниже» подтверждено семьёй эквивалентностей); nonAxiomaticRemainingObligation_forces_scale_ge_five — сужение A ≥ 5 распространяется на остаток.

Финальный мета-кирпич escape-or-return (в том же файле, но аксиому не использует — верификатор подтверждает: все его декларации axiom-clean): внешнее доказательство/опровержение либо транслируется назад в Step00 (⟹ двигатель ⟹ пусто: no_externalProof_under_proofReturn), либо подлинно сбегает из архитектуры (existing_externalProof_forces_proofEscape); сильная мета-полнота (все маршруты возвращаются) ⟹ решений нет вовсе (step00Completeness_noProof_noRefutation); пакет — lastMetaStep00Brick. Фикс: ¬Step00MediatedStatement → → False (data-структура).

Честность (машинно): proofEscapes_iff_proofExists — «побег» ⟺ существование доказательства, возврат ⟺ пустота: дихотомия — переименование Nonempty/IsEmpty, тавтологична; несущая часть — только условная axiomGivesTwins (уже известная).

Strict-пакет аксиомы (кирпич package, тоже в карантине): максимально явная data-форма (A, projOf, resolves) ⟺ аксиома (strictStep00CausalClosurePackageExists_iff_axiom); полный список следствий — finalConsequences_of_strictPackage; кирпич честно отделяет точную Step00-каузальность от «какой-то внешней причины» (§5). Фиксы: ofStep00CausalClosure — Prop→Type элиминация через .choose.

Честность (машинно): strictPackageExists_iff_lastStep00Obligation — пакет ⟺ старый узел; twin_above_of_strictPackage — детектор; strictPackage_scale_ge_five — сужение бьёт прямо по полю данных: у любого пакета A ≥ 5.

Кирпич well-founded-causal-fractal — вершина мета-серии, точный смысл «вселенная фрактальна»: самоподобие на мета-границе (в каждом мета-узле (T, φ) повторяется та же дихотомия побег/возврат — metaFractalSelfSimilarity) + внутренняя well-foundedness (no_rankedMetaFractalBranch — ∞-ветвь со строгим ℕ-спуском ранга невозможна); конечные префиксы = башни причин; итоговый пакет — wellFoundedCausalFractalAudit. Не геометрический фрактал (scope guard). Все декларации axiom-clean. Фикс: data-ветвь → → False.

Честность (машинно): metaFractalOutcome_iff — 6-ветвевой исход коллапсирует в честную 3-дизъюнкцию: узел ∨ ∃ доказательство ∨ ∃ опровержение (seam/payment/engine сожжены, «побеги» — переименования существования); поля самоподобия — те же Nonempty/IsEmpty-тавтологии.

Внутренняя причина новой вселенной: выживает только внешняя¶

Кирпич internal-cause (зависимый слой RealisedNegationOfCausalClosure реконструирован — кирпич causal_closure_negation_self_destruct отсутствовал в поставке): внешняя причина = вход/аксиома (порождает вселенную); полная внутренняя причина = boundary-crossing self-proof = запрещённый двигатель (no_internalUniverseCause); реализованное отрицание причины (конкретное препятствие: стабильный ledger + коллизия) самоуничтожается (no_realisedNegationOfCausalClosure).

Трихотомия UniverseCauseMode (external / internal / negated): выживает только external (nonExternalUniverseCauseMode_impossible).

Честность (машинно): internalUniverseCause_iff_and_not — внутренняя причина ⟺ P ∧ ¬P (тавтологично для любого P); universeCauseMode_iff — трихотомия коллапсирует: UniverseCauseMode P ⟺ P — «выживает только внешняя причина» буквально означает, что других обитаемых ветвей нет; содержание слоганов — уже известные generates_twins.

Кирпич finite-causal-tower: конечная башня «кто-то создал» классифицируется индукцией (finiteCausalTowerAttempt_classifies) в 4 исхода (граница/шов/оплата/двигатель); без всех четырёх башня невозможна; ∞-башня со строгим ℕ-спуском ранга невозможна (no_infiniteRankedCausalTower); сводка — causalTowerAuditSummary. Фиксы: data-структура → → False; summary объявлена : Prop. Честность (машинно): causalTowerOutcome_iff и finiteCausalTowerAttempt_iff — исход ⟺ P и башня любой глубины ⟺ P: обитаема только boundary-ветвь, «добавление творцов не снимает границу» — буквально.

Кирпич internal-first-cause (финальное различение): внешняя первопричина — граница/аксиома; внутренняя — self-cause = двигатель (internalFirstCauseIsPerpetualEngine, noSameSystemCreatorWithoutEngine — «создатель внутри той же замкнутой системы» невозможен); охват честно ограничен кирпичом (§5: внешние аксиомы не объявляются двигателями). Честность (машинно): internalFirstCause_iff_and_not (⟺ P ∧ ¬P), firstCauseMode_iff — режим коллапсирует: FirstCauseMode P ⟺ P.

Мега-партия фронтов (125 кирпичей, 5 модулей одной сборкой)¶

Пять серий, собранных оркестрацией (каждая — один модуль; полные флаги — в заголовках модулей):

Engine/RiemannLayerBoxFront (25) — residue-таблицы/move-алгебра/blocker-ядра layerbox-фронта. Реально доказано: mod-6 арифметика (555/111+2 невозможно, кортеж 511/511 сбалансирован) + генерические descent/finite-cover сборки; остальное — каркасы обязательств; 7 native_decide заменены на kernel-checked decide.
Engine/RiemannTerminalRankFront (18) — terminal/rank-flow/fuel. Честно: каждый closure-сертификат несёт target_of_noZeros — RH-образный вывод является входом, а «no zeros» предполагается assumption-полями; инертные firewall'ы помечены; дубликат rank_projection исключён.
Engine/MersenneForwardFront (34) — ⚠️ вакуумность поздних кирпичей вскрыта: noEngine-пакеты (four_defect / twin_step00_bridge / oversaturation / no_escape / endgame) необитаемы — токены несут свободное witness : Prop, «двигатель» строится тривиально, headline-теоремы (produces_infinite_mersenne_twins и род.) вакуумны; маршруты требуют привязки witness к реальной Step00-структуре. Sound/cofinal-поля — переупакованные выводы.
Engine/ClassicalFrontierRoutes (42) — external routes v2–v8, promise/collision/FP-FNP/ resolver-коды. Удалён ложный falseDecider (Decider из константы false); два дефекта починены усилением входов; ~30 слоганов — буквально True; входы-переупаковки (local_incompressible полем) помечены.
Engine/RankClosureFront (6) — rank-closure; разделение целиком условно на невыстроенном RankSeparationWitness.

Сборочный аудит: ни одного sorry/axiom в партии; ofReduceBool не введён (все native_decide → decide); безусловных сильных выводов (RH / TwinLowers.Infinite / ClassesSeparate / False) нет.

⚡ Машинное сужение узла: ветвь A ≤ 4 опровергнута¶

Адверсариальный probe одностейтментного аудита нашёл, а ручная перепроверка подтвердила: 5-адическая цепь c(k+1) = 5·c(k) + 1 (тождество 6·(5x+1) − 1 = 5·(6x+1), bigDivisor 5 > A) даёт бесконечную admissible-семью генеалогий без каких-либо twin-гипотез при A ≤ 4, M0 = 1: чистота бесплатна (2 и 3 никогда не делят 6m±1), все пост-вакуумные заплаты выполнены честно.

Пиджонхол ⟹ no_projection_resolves_at_smallScale ⟹ smallScale_branch_of_lastStep00Obligation_refuted: ветвь A ≤ 4 узла мертва; lastStep00Obligation_forces_scale_ge_five — ∃A живёт только в A ≥ 5. Для A ≥ 5 тот же приём требует чистых стартов с контролем peel-целей — арифметика дирихле-класса, отсутствующая в репо (и вероятно за красной линией).

Вывод. Выполнимость узла при A ≥ 5 — подлинно открыта; узел сужен, не закрыт и не опровергнут.

Диссипативный cascade: capacity/overflow декомпозиция Лиувилль-узла¶

Engine/DissipativeCascade (единый blueprint Step00/RH/Навье–Стокс): «дефект не исчезает; не закрылся — плати». Новое сверх уже встроенного (closed-paid, dichotomy, rank/parity):

L_eq_relevant_add_irrelevant и relevantViolation_of_globalViolation — доказаны (оба sorry blueprint'a закрыты): разбиение $[1,X]$ на релевантную/нерелевантную части и overflow-лемма — если глобальный дисбаланс $|L(X)|$ превышает всякий bound, а нерелевантная часть ограничена, то релевантная часть обязана переполниться (неравенство треугольника, порог $C + C_{irr}$).
Это декомпозирует крупный узел RankJumpLocalization на два меньших аналитических входа: IrrelevantCancellation + pairing.unpaired_gives_jump.
Pairing-вход декомпозирован дальше (Engine/RiemannRankProjection, кирпичи strict + gradual): exists_firstOverflowCrossing — доказана (дискретная first-crossing лемма, Nat.find: положительный дефект ⟹ первое пересечение порога с глобальной минимальностью + одношаговая форма prev_safe ∧ now_pos); gradualOverflow_forces_rankJump — сборка цепи safe-старт ⟹ first crossing ⟹ unpaired ⟹ rank-jump. Стыковка машинно проверена (twinCarrierPairing_of_gradualRoute): route-сертификат с endpoint-картами поставляет настоящий TwinCarrierPairing — unpaired_gives_jump выводится, не постулируется. Остаток входа №8 распался на: (A) window-бухгалтерию, (B) «first crossing ⟹ unpaired carrier» (локальный capacity/pairing), (C) rank-видимость, (D) endpoint-карты. Честность: «no-RH-leak аудиты» кирпичей выполнимы тривиально (rankProjectionAudit_is_free) — это документирующие маркеры, где искать протечку, а не машинные проверки её отсутствия; RH-имена в кирпичи не втащены.

⚠️ Эпизод вакуумности №2 — риманова ветка (адверсариальный probe; полное раскрытие в Engine/RiemannRankProjectionAudit). Цель маршрута TwinCarrierEnergyJump оказалась непривязанной к нарушению: это голое Nonempty (RankEnergyJump ...) — для естественной системы LiouvilleRankSystem (rank = Ω, sign = λ) она безусловная теорема (состояния 1 и 2, liouvilleRankSystem_has_jump). Следствия (машинно): полный пакет LiouvilleToTwinLocalization обитаем с нулевым аналитическим входом (fullLocalization_noInput — partition «всё релевантно», тривиальная cancellation, paired := False); поле paired инертно (pairing_reduces_to_jump_field); куски (A)–(C) градуального маршрута dischargeable (window-бухгалтерия закрыта честно: relevantViolation_gives_window, конкретный ledger mass = |LRelevant|, capacity = ⌈X^{1/2+ε}⌉; crossing_gives_carrier — честная непустота relevant в точке пересечения). Итог (wall_relevant/wall_global): единственная несущая стена маршрута — ровно ¬LiouvilleViolation (RH-силы bound на суммарный Лиувилль). Декомпозиция «cancellation + pairing» была ложной: pairing-сторона веса не несла. Маршрут требует переформулировки с целью, привязанной к нарушению. RH не доказана; вскрыта пустота обёртки — как и в близнецовом эпизоде, честность машинная. - real_positive_work_not_wellfounded — машинное предупреждение (§2): для ℝ-бюджета строго положительная работа не даёт well-foundedness ($a_n = 1/2^n$) — потому НС-аналогия только структурная, в отличие от ℕ-движка.

Навье–Стокс: само уравнение + честность интегралов¶

Engine/NavierStokes формализует само уравнение (mathlib fderiv/gradient/интеграл Бохнера): IsNSSolution ν f u p = баланс импульса $\partial_t u + (u\cdot\nabla)u = \nu\Delta u - \nabla p + f$ плюс несжимаемость $\mathrm{div}\,u = 0$; не-вакуумность доказана (zero_is_NSSolution). Энергия $E = \tfrac12\int\|u\|^2$, диссипация $D = \nu\int\sum_i\|\partial_i u\|^2$.

Честность интегралов (машинно):

kineticEnergy_of_not_integrable — интеграл Бохнера молча равен нулю на неинтегрируемом поле (integral_undef): «нулевая энергия» без FiniteKineticEnergy — артефакт, не физика. Интегрируемость — обязательная часть всякого энергетического входа.
twoTimeEnergyInequality_of_energyBalance — доказана (FTC-глюа): монолитное двухвременное энергетическое неравенство сведено к узкому точечному входу EnergyBalanceLaw ($dE/dt = -D$; = дифференцирование под интегралом + интегрирование по частям + $\mathrm{div}\,u=0$; в mathlib дивергенция есть лишь в box-форме — предельный переход на $\mathbb{R}^3$ не формализован).
ns_no_infinite_dissipative_cascade_of_balance — полная цепь: точечный баланс + интегрируемость диссипации ⟹ нет бесконечного $\delta$-каскада (квантизация §2bis на настоящем уравнении).

Не доказаны (проблема тысячелетия): существование/регулярность и сам EnergyBalanceLaw. Никакой связи с простыми — красная линия нетронута.

Красная линия цела. Step00 остаётся sorry.

Где мы¶

Мы честно разложили выход из чистого графа. Точечная регенерация boundary опровергнута ($18 \mapsto (107,109)$); доказуемая дихотомия Теорема 24.1 (boundary_exit_decomposes) показывает, что нечистая цель либо продолжает old-peel-спуск, либо садится в конечный старый absorber.

Итог раздела. Вся нетривиальная нагрузка локализована и вынесена на глобальный уровень: GlobalAbsorberNode (Определение 24.2, не доказан) плюс доказанная сборка Теорема 24.3 (no_global_absorption_under_epmi) и доказанный pigeonhole-скелет Теорема 24.4 (global_absorber_forces_engine), в котором единственная дыра — Hall-узел pump (fan-in $570 \to 1$ $\Rightarrow$ двигатель). Мы нигде не выдаём редукцию за доказательство: доказана комбинаторика коллизии, гипотезой остаётся её интерпретация как двигателя.

В следующей главе 25. Rigid closure мы возвращаемся к тому, можно ли этот pump заменить чисто структурным замыканием — доказать достижение twin через строгое падение высоты и well-foundedness ℕ, без обращения к fan-in-насосу, и тем самым проверить, не сводится ли глобальный absorber-узел к уже имеющемуся конструктивному входу regenerate.