29. Последнее звено и его граница¶

← 28. MkNode · Оглавление · 30. Риман: контрапозиция →

Lean-источник: EuclidsPath/Engine/CarrierBridge.lean (namespace EuclidsPath.CarrierBridge), опирается на EuclidsPath/Engine/ProductCore.lean и EuclidsPath/Engine/Residuals.lean. Ключевые имена: cleanCenters_infinite, exists_infinite_fiber, factorizationData_of_carrier, engine_of_carrier_and_factorize, product_core_engine_of_carrier.

В предыдущей главе (28, mkNode) мы научились из одной clean-стороны извлекать конкретный узел ядра RankNode r: разложение составной стороны $6m\pm 1$ в простые факторы > A дало нам знак и role-indexed набор факторов, а factor_rank_le_four зажал ранг между 2 и 4. Иначе говоря, у нас есть локальная карта «центр $m$ $\mapsto$ узел ядра».

Теперь мы собираем последнее звено: соединяем эту карту с уже доказанной бесконечностью носителя (carrier) и с pump-машиной ядра из главы про ProductCore, чтобы получить вечный двигатель Евклида (Engine) — главный запрещённый объект программы (см. словарь). Мы покажем, что вся арифметика этого звена доказана, — и честно очертим единственную границу, о которую оно упирается.

29.1. Что даёт носитель: бесконечность clean-центров¶

Введём множество clean-центров при фиксированном пороге $A$.

Определение 29.1 (CleanCenters). Для $A\in\mathbb{N}$ полагаем

\[ \mathrm{CleanCenters}(A)\;:=\;\{\,m\in\mathbb{N}\;\mid\;\mathrm{CleanZ}\,A\,(m:\mathbb{Z})\,\}, \]

где CleanZ A m означает, что ни одно простое $q\le A$ не делит ни одну из сторон $6m-1$, $6m+1$ (в $\mathbb{Z}$). Это clean-центр: центр, свободный от «старых» простых $\le A$.

Первый кирпич звена — бесконечность этого множества. Она не постулируется: она вытекает из уже доказанного в Residuals факта carrier_nonempty_above, который для любых $A,N$ предъявляет clean-центр строго выше $N$ (конструктивно, $m=(N+1)\cdot\mathrm{oldPrimorial}\,A$; плотность не нужна).

Теорема 29.2 (cleanCenters_infinite). Для всякого $A$ множество $\mathrm{CleanCenters}(A)$ бесконечно:

\[ (\mathrm{CleanCenters}\,A).\mathrm{Infinite}. \]

Доказательство простое по форме и содержательное по смыслу. Мы применяем Set.infinite_of_not_bddAbove: достаточно показать, что множество не ограничено сверху. Для любого кандидата в верхнюю границу $N$ факт carrier_nonempty_above A N даёт clean-центр $m>N$, что и опровергает ограниченность.

Почему это работает без всякой аналитики: clean-центры строятся как кратные примориала $\mathrm{oldPrimorial}\,A$ — произведения всех простых $\le A$; такое кратное сравнимо с $0$ по каждому малому простому, а значит $6m\pm 1\equiv \pm 1$, и ни одно $q\le A$ его не делит. Кратных примориала бесконечно много, они уходят как угодно высоко — отсюда бесконечность.

Что это значит: носитель двойки поставляет неограниченный запас стартов, свободных от малых простых, — то самое «топливо», которого требует pump-машина ядра.

29.2. Единственный реальный вход: FactorizationData¶

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

Определение 29.3 (FactorizationData A X_A). Пакет данных, состоящий из: - ранга $r$ с $1\le r\le 4$; - бесконечного множества стартов $S\subseteq\mathbb{N}$ одного ранга $r$; - карты node : ℕ → RankNode r, инъективной на $S$ (hinj : Set.InjOn node S); - сертификата легальности hamb : ∀ m ∈ S, AmbientLegal X_A (node m).factors.

Здесь AmbientLegal X_A factors означает существование общего top-side $N_0$ с $0<N_0\le 6X_A+1$ и $\text{factors}\,i\mid N_0$ для всех $i$.

Это не аксиома двигателя. Содержательно FactorizationData — это утверждение «бесконечно много clean-стартов одного фиксированного ранга раскладываются в легальные узлы ядра, причём разные старты дают разные узлы». Существование разложения и оценку rank ≤ 4 даёт сама арифметика (глава 28), а фиксацию одного ранга — pigeonhole — пижонхол, принцип ящиков (см. ниже и словарь). Собрав такой пакет, мы немедленно получаем двигатель.

Теорема 29.4 (engine_of_factorization). При separating scale $6X_A+1<P_A$ и наличии $F:\mathrm{FactorizationData}\,A\,X_A$ выполняется Engine:

\[ 6X_A+1<P_A\;\wedge\;F\;\Longrightarrow\;\mathrm{Engine}.\tag{29.1} \]

Это буквально product_core_engine_of_carrier, которому подставлены поля пакета $F$: ранг F.r, множество F.S, бесконечность F.hS, карта F.node, инъективность F.hinj, легальность F.hamb.

Почему этого достаточно: инъективная карта бесконечного $S$ в конечное signature-пространство CoreSig P_A r (конечное, поскольку $A$, а с ним $P_A$, фиксированы) обязана дать коллизию — два разных узла с равной подписью; далее descent-по-рангу (core_step_proved) и rank-1 база (rank_one_coreCollision_absurd), обе доказанные чистой арифметикой при separating scale, замыкают всё до Engine. Вся эта pump-машина — descent, база, pigeonhole — уже доказана в главах про ProductCore и SeparatingScale; здесь мы лишь предъявляем ей вход.

Примечание. Роль separating scale $6X_A+1<P_A$ ровно та же, что в главе 30: она делает coarse-паспорт a mod P_A инъективным на легальном слое (ambient_factor_lt_primorial: каждый фактор $<P_A$), чем обходит трилемму UniqueLegalLift. Здесь мы этим уже пользуемся как готовым фактом.

29.3. Сборка ранга: infinite-pigeonhole¶

Чтобы построить FactorizationData из «сырых» центров, нужно из бесконечного носителя выделить бесконечное подмножество одного ранга. Это чистый комбинаторный факт, и он доказан полностью.

Теорема 29.5 (exists_infinite_fiber). Пусть $S$ бесконечно и $f:S\to \mathrm{Fin}(n+1)$. Тогда некоторый слой бесконечен:

\[ \exists c,\;\{x\mid x\in S\wedge f\,x=c\}.\mathrm{Infinite}. \]

Доказательство — бесконечный ящичный принцип от противного. Если бы каждый слой был конечен, то $S\subseteq\bigcup_c\{x\in S\mid f\,x=c\}$ было бы конечным объединением конечных множеств, значит конечным, — противоречие с бесконечностью $S$. Что это значит для нас: рангов всего четыре ($1..4$), поэтому среди бесконечно многих clean-центров бесконечно много имеют один и тот же ранг. Именно этот слой и станет множеством $S$ внутри FactorizationData.

Теперь склеиваем pigeonhole с картами факторизации.

Определение 29.6 (factorizationData_of_carrier). Даны: - бесконечный носитель $C\subseteq\mathbb{N}$ (hC : C.Infinite); - ранг-функция rankOf : ℕ → Fin 4 (число больших простых факторов, сдвинутое; арифметика главы 28); - карта узлов mkNode : (r:ℕ) → ℕ → RankNode r; - инъективность hinj карты mkNode (r+1) на каждом ранговом слое $\{x\in C\mid \mathrm{rankOf}\,x=r\}$; - легальность hamb: $m\in C$, $\mathrm{rankOf}\,m=r\Rightarrow \mathrm{AmbientLegal}\,X_A\,(\mathrm{mkNode}\,(r{+}1)\,m).\text{factors}$.

Тогда строится FactorizationData A X_A: выбирается бесконечный ранговый слой $c$ (через exists_infinite_fiber), кладётся $r=c+1$ (так $1\le r\le 4$), $S$ — этот слой, node = mkNode (c+1), а hinj/hamb берутся на выбранном слое.

Здесь единственным недоказанным элементом остаются сами карты rankOf, mkNode, hinj, hamb: привязка ранга к центру и легальная факторизация $6m\pm 1=\prod a_i$. Комбинаторику же (выбор бесконечного слоя одного ранга) мы уже провели строго.

29.4. Финал от носителя и факторизации¶

Соединяя всё, получаем итоговую теорему звена.

Теорема 29.7 (engine_of_carrier_and_factorize). При separating scale $6X_A+1<P_A$, бесконечном носителе $C$ и наличии ранг-функции rankOf и карты узлов mkNode, инъективной и AmbientLegal на каждом ранге, — выполняется Engine:

\[ 6X_A+1<P_A,\;C.\mathrm{Infinite},\;\mathrm{rankOf},\;\mathrm{mkNode},\;\mathrm{hinj},\;\mathrm{hamb}\;\Longrightarrow\;\mathrm{Engine}.\tag{29.2} \]

Она есть композиция engine_of_factorization ∘ factorizationData_of_carrier (Теорема 29.4 ∘ Определение 29.6). Что доказано полностью внутри звена: бесконечность носителя (Теорема 29.2, cleanCenters_infinite), выбор бесконечного слоя одного ранга (Теорема 29.5, exists_infinite_fiber), и вся pump-машина, к которой мы подключаемся (product_core_engine_of_carrier).

Единственный вход — карты факторизации rankOf/mkNode/hinj/hamb. Иначе говоря, звено переводит задачу «доказать бесконечность близнецов» в задачу «предъявить бесконечное семейство clean-центров, факторизуемых в легальные узлы фиксированного ранга инъективно».

29.5. Граница: почему прямая склейка невозможна¶

Здесь необходима полная честность, иначе редукция выдаётся за доказательство. Между двумя доказанными концами звена — cleanCenters_infinite слева и pump-машиной справа — есть шов, который не склеивается напрямую.

Наблюдение (масштабный барьер). Легальность AmbientLegal X_A требует, чтобы факторы делили общий top-side $N_0\le 6X_A+1$. Но факторы центра $m$ — это делители его собственных сторон $6m\pm 1$. Значит node m может быть AmbientLegal X_A только когда сторона укладывается в окно, то есть по сути когда $$6m\pm 1\;\le\;6X_A+1,\qquad\text{то есть}\quad m\;\lesssim\;X_A.$$ Это конечный отрезок центров $m\le X_A$ — ровно область, где mkNode/nodeable из главы 28 применимы (там rank ≤ 4 держится именно потому, что произведение факторов ограничено $6X_A+1<A^5$).

С другой стороны, cleanCenters_infinite даёт бесконечность по $m$: clean-центры уходят как угодно высоко, неизбежно выше $X_A$. А там сторона $6m\pm 1>6X_A+1$ и сертификат AmbientLegal X_A больше недоступен; вместе с ним ломается и оценка ранга $\le 4$ (произведение факторов уже не заперто под $A^5$).

Примечание (в чём именно шов). Бесконечность носителя — это бесконечность по вертикали $m\to\infty$; легальность узла — это принадлежность конечному горизонтальному окну $m\le X_A$. Пересечение «бесконечно много $m$» $\cap$ «$m\le X_A$» пусто при фиксированном $X_A$. Поэтому нельзя взять готовую бесконечность из cleanCenters_infinite и напрямую подать её в factorizationData_of_carrier: у почти всех этих центров нет AmbientLegal X_A-узла. Гипотезы hamb из §29.3 при фиксированном $X_A$ не выполнимы на всём носителе — они выполнимы лишь на конечном срезе.

Вывод. Именно поэтому карты mkNode/hinj/hamb оставлены входом, а не выведены: их нельзя получить из одной лишь cleanCenters_infinite. Требуется механизм, который поставляет бесконечно много легальных узлов на растущем масштабе — не при одном $X_A$, а согласованно, когда $X_A$ и $A$ растут вместе с $m$.

29.6. Несводимый узел: GlobalOldAbsorption¶

Этот механизм — GlobalOldAbsorption: утверждение о родословных (genealogies) на растущем масштабе, поглощающих старые простые. Комментарий финальной теоремы ProductCore формулирует это прямо: открытым остаётся ровно carrier-структура CarrierData, «то, что должно прийти из GlobalOldAbsorption (факторизация $6m+\sigma$, rank ≤ 4, бесконечность стартов)».

Честная оценка: GlobalOldAbsorption несводим — по силе он равен самой гипотезе близнецов. Он требует предъявить бесконечное семейство центров, каждый из которых (i) clean, (ii) имеет составную сторону с легальной факторизацией фиксированного ранга и (iii) даёт различимые узлы, — причём согласованно при $m\to\infty$. Это, по сути, и есть контроль над бесконечным числом «поглощённых» родословных. Никакая конечная арифметика (её мы уже исчерпали в главах 28 и 30) сюда не дотягивается: барьер §29.5 показывает, что любой конечный $X_A$ отсекается.

Гипотеза (descent-forest control). Из интуиции переноса двойки естественно предположить следующее. Рассмотрим лес спуска (descent-forest) над clean-центрами: рёбра — шаги строгого спуска высоты вдоль активных факторов. Тогда контроль ветвления этого леса — ограниченность fan-in и невозможность бесконечного спуска (уже доказанный no_infinite_descent) — влечёт, что бесконечно много родословных «absorbed»: их старые простые полностью поглощены, а стороны становятся легально факторизуемыми на своём масштабе. Формально:

\[ \text{descent-forest bounded}\;\Longrightarrow\;\{\,m\;\mid\;m\ \text{absorbed, rank}\le 4,\ \text{node инъективен}\,\}\ \text{бесконечно}. \]

План закрытия. (1) Определить масштаб-функцию $A(m),X_A(m)$, растущую вместе с $m$ так, чтобы сторона $6m\pm 1$ попадала в окно $\le 6X_A(m)+1$ и при этом separating scale $6X_A(m)+1<P_{A(m)}$ сохранялся (по главе 30 это достижимо с запасом: $\log P_A\sim A/\ln 10$ обгоняет $4.5\log A$). (2) На этом растущем масштабе применить арифметику главы 28 (mkNode_of_composite) к absorbed-центрам, получив AmbientLegal-узлы ранга $2..4$ на своём масштабе. (3) Через exists_infinite_fiber зафиксировать один ранг на бесконечном подсемействе. (4) Свести всё к engine_of_carrier_and_factorize, подав absorbed-подсемейство как носитель $C$ и построенные узлы как mkNode. Ключевой недостающий шаг — именно (1)+(2): согласованное с масштабом поглощение старых простых, то есть GlobalOldAbsorption.

Итог раздела. Звено CarrierBridge замкнуто с обоих концов доказанной математикой, и между ними остаётся ровно один именованный, несводимый узел. Мы не выдаём эту редукцию за доказательство близнецов: она честно переформулирует их как GlobalOldAbsorption и указывает план закрытия через контроль descent-forest.

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

Финальный узел близнецов оказался по сложности сопоставим с самой гипотезой — типичная граница глубоких редукций. В следующей главе (30, Риман) мы увидим, что та же схема «от противного через двигатель Евклида» переносится на побочную ветку: ¬RH подаётся в тот же доказанный EPMI, и вся аналитика снова изолируется в единственном мосте EngineBridge — аналоге GlobalOldAbsorption, но уже для нулей $\zeta$. Структура предельного узла повторится, что и объясняет, почему обе задачи упираются в один и тот же механизм переноса двойки.

← 28. MkNode · Оглавление · 30. Риман: контрапозиция →