11. Гипотеза близнецов из блочного ядра¶

← 10. survivor ⇒ twin · Оглавление · 12. Four-corner →

Lean: Engine/TwoTransport.lean (twin_prime_conjecture_of_blocks, twin_center_of_block, prime_of_no_small_prime_factor, isTwinCenter_of_root_sieve).

В главе 10 NonCover мы построили два элементарных факта: из перевеса носителя над «плохим» множеством извлекается выживший (survivor_of_not_covered), а неограниченный по масштабу запас twin-центров влечёт саму гипотезу (infinite_of_unbounded_centers). Теперь мы собираем из этих кирпичей единый нециркулярный мост и, что важнее, точно очерчиваем, где именно в нём проходит граница между доказанным и открытым.

Настоящая глава — узловая: она формулирует условную редукцию гипотезы простых-близнецов к одному блочному утверждению и доказывает, что одно из трёх слагаемых этого утверждения (переход survivor⟹twin) элементарно, а значит вся оставшаяся трудность локализована в счётной части.

Постановка: что мы хотим перенести¶

Напомним центровую форму пары близнецов, зафиксированную в основаниях программы. Центр $m$ задаёт пару близнецов, если обе стороны простые.

Определение 11.1 (twin-центр). Для $m \in \mathbb{N}$ полагаем $$\mathrm{IsTwinCenter}(m) \;:\Longleftrightarrow\; (6m-1)\ \text{простое}\ \wedge\ (6m+1)\ \text{простое}.$$ В Lean это IsTwinCenter m := (6 * m - 1).Prime ∧ (6 * m + 1).Prime. Множество младших членов пар близнецов обозначается TwinLowers, а цель всей цепочки — TwinLowers.Infinite, то есть бесконечность множества $\{p : p, p+2\ \text{простые}\}$.

Ограничение центров вида $6m\pm 1$ не сужает задачу: всякая пара близнецов, кроме $(3,5)$, имеет вид $(6m-1, 6m+1)$, поскольку любое простое $>3$ сравнимо с $\pm 1$ по модулю $6$. Поэтому бесконечность twin-центров равносильна бесконечности пар близнецов — эта равносильность и оформлена в infinite_of_unbounded_centers из предыдущей главы.

Один блок: локальная лемма переноса¶

Работа ведётся поблочно. На каждом масштабе $N$ мы рассматриваем конечное множество кандидатов — carrier (носитель), — все элементы которого лежат выше $N$, и конечное множество bad (плохих), которые заведомо не являются twin-центрами. Локальный шаг утверждает: если носитель численно перевешивает плохих и каждый неплохой элемент носителя есть twin-центр, то выше $N$ гарантированно найдётся twin-центр.

Теорема 11.2 (twin_center_of_block). Пусть $N \in \mathbb{N}$, а $\mathit{carrier}, \mathit{bad} \subseteq \mathbb{N}$ — конечные множества, для которых выполнено: $$(\mathrm{above})\ \forall m \in \mathit{carrier},\ N < m;\qquad (\mathrm{cov})\ |\mathit{bad}| < |\mathit{carrier}|;$$ $$(\mathrm{twin})\ \forall m \in \mathit{carrier},\ m \notin \mathit{bad} \Rightarrow \mathrm{IsTwinCenter}(m).$$ Тогда $\exists m,\ N < m\ \wedge\ \mathrm{IsTwinCenter}(m).$

Доказательство прямое и опирается ровно на два факта. Из строгого неравенства мощностей $(\mathrm{cov})$ по survivor_of_not_covered (глава 10) извлекается выживший $m \in \mathit{carrier}$ с $m \notin \mathit{bad}$. Условие $(\mathrm{above})$ даёт $N < m$, а импликация $(\mathrm{twin})$, применённая к этому выжившему, даёт $\mathrm{IsTwinCenter}(m)$. В Lean это буквально две строки:

obtain ⟨m, hm, hmb⟩ := survivor_of_not_covered hcov
exact ⟨m, habove m hm, htwin m hm hmb⟩

Примечание. Здесь нет ни анализа, ни распределения простых — только Finset-комбинаторика: если бы носитель целиком лежал в плохих, было бы $|\mathit{carrier}| \le |\mathit{bad}|$, что противоречит $(\mathrm{cov})$. Вся содержательная работа спрятана в трёх гипотезах $(\mathrm{above})$, $(\mathrm{cov})$, $(\mathrm{twin})$; лемма лишь честно комбинирует их.

Глобальный мост: редукция гипотезы к блочному ядру¶

Локальная лемма даёт twin-центр выше одного $N$. Чтобы получить бесконечность, нужно, чтобы блочная посылка выполнялась на каждом масштабе. Это и есть блочное ядро.

Теорема 11.3 (twin_prime_conjecture_of_blocks). Предположим, что $$\forall N \in \mathbb{N},\ \exists\, \mathit{carrier}, \mathit{bad} \subseteq \mathbb{N}\ \text{конечные},\quad (\mathrm{above}) \wedge (\mathrm{cov}) \wedge (\mathrm{twin}).$$ Тогда $\mathrm{TwinLowers.Infinite}$ — простых-близнецов бесконечно много.

Доказательство собирается из уже готовых частей. По infinite_of_unbounded_centers достаточно показать неограниченность twin-центров: для произвольного $N$ предъявить центр выше $N$. Фиксируем $N$, берём из посылки блок $(\mathit{carrier}, \mathit{bad})$ для этого $N$ и применяем Теорему 11.2 (twin_center_of_block). Формально:

apply infinite_of_unbounded_centers
intro N
obtain ⟨carrier, bad, habove, hcov, htwin⟩ := h N
exact twin_center_of_block habove hcov htwin

Смысл теоремы в том, что она изолирует открытое ядро в форме, пригодной для дальнейшей работы. Импликация «блочное ядро $\Rightarrow$ гипотеза» машинно проверена и нециркулярна: она нигде не использует саму гипотезу и не прячет её в посылке. Открытым остаётся ровно доказать посылку — что на каждом масштабе такой блок существует. Эта посылка распадается на три независимых узла:

carrier-оценка снизу — что носитель кандидатов выше $N$ достаточно велик (в терминах программы это вход CarrierInput — именованное 🔴-утверждение, которого не хватает до цели, см. словарь);
bad-оценка сверху — что множество плохих строго меньше носителя (через fan/cycle-счёт, см. 09 Cycle);
survivor⟹twin — что всякий неплохой выживший действительно twin-центр.

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

Третий узел элементарен: сито до корня¶

Оставшаяся часть главы закрывает узел (3) полностью и тем самым сдвигает всю трудность в счётную пару (1)–(2). Ключ — классический критерий простоты через пробное деление до квадратного корня.

Теорема 11.4 (prime_of_no_small_prime_factor). Пусть $n \ge 2$ и ни один простой $p$ с $p^2 \le n$ не делит $n$: $$\forall p\ \text{простое},\ p^2 \le n \Rightarrow p \nmid n.$$ Тогда $n$ простое.

Доказательство от противного. Если $n$ не простое, рассмотрим его минимальный простой делитель $p = \mathrm{minFac}(n)$; при $n \ge 2$ он существует и прост (Nat.minFac_prime), и $p \mid n$ (Nat.minFac_dvd). Минимальность даёт $p \le n / p$ (Nat.minFac_le_div для непростого $n$), откуда $$p^2 = p \cdot p \le p \cdot (n / p) \le n$$ (последнее — Nat.mul_div_le). Итак $p$ — простой делитель $n$ с $p^2 \le n$, что противоречит посылке. Значит $n$ простое.

Примечание. Наблюдение, лежащее в основе критерия: у составного $n$ наименьший простой делитель не превосходит $\sqrt n$, иначе произведение двух делителей, каждый больше $\sqrt n$, превзошло бы $n$. Это тождество эпохи Эратосфена, здесь оформленное без сита как таковое — через minFac. Никакого перебора: одно неравенство и минимальность.

Применяя критерий к обеим сторонам центра, получаем искомый критерий выживания.

Теорема 11.5 (isTwinCenter_of_root_sieve). Пусть для центра $m$ обе стороны не меньше $2$ ($2 \le 6m-1$ и $2 \le 6m+1$), и ни один простой до корня каждой стороны её не делит: $$\forall p\ \text{простое},\ p^2 \le 6m-1 \Rightarrow p \nmid (6m-1);\qquad \forall p\ \text{простое},\ p^2 \le 6m+1 \Rightarrow p \nmid (6m+1).$$ Тогда $\mathrm{IsTwinCenter}(m)$.

Доказательство — просто пара применений предыдущей теоремы: Теорема 11.4 (prime_of_no_small_prime_factor) даёт простоту $6m-1$ и $6m+1$ по отдельности, а их конъюнкция и есть $\mathrm{IsTwinCenter}(m)$. В Lean это одна строка через конструктор:

⟨prime_of_no_small_prime_factor h1 s1, prime_of_no_small_prime_factor h2 s2⟩

Содержательный вывод: узел (3) не содержит трудности. Условие «$m$ не плохой» в правильной кодировке означает ровно «ни один малый простой (до корня стороны) не делит ни одну из сторон» — а это по Теореме 11.5 (isTwinCenter_of_root_sieve) немедленно влечёт twin-центральность. Иными словами, если множество плохих определить как центры, у которых хотя бы у одной стороны есть простой делитель ниже корня, то импликация $(\mathrm{twin})$ из блочного ядра выполняется автоматически, без дополнительных допущений.

Примечание. Здесь важно не выдать редукцию за доказательство. Теорема 11.5 (isTwinCenter_of_root_sieve) доказывает лишь направление survivor⟹twin: неплохой выживший есть twin-центр. Оно не утверждает, что выживший существует, — это работа узлов (1)–(2). Мы закрыли третий из трёх узлов и тем самым показали, где остальная трудность точно не прячется.

Что доказано и что осталось¶

Соберём баланс главы. Машинно проверены и нециркулярны:

локальный перенос Теорема 11.2 (twin_center_of_block): блок с перевесом носителя $\Rightarrow$ twin-центр выше $N$;
глобальная редукция Теорема 11.3 (twin_prime_conjecture_of_blocks): блочное ядро на всех масштабах $\Rightarrow$ гипотеза близнецов;
элементарность третьего узла: Теорема 11.4 (prime_of_no_small_prime_factor) и Теорема 11.5 (isTwinCenter_of_root_sieve) закрывают survivor⟹twin без анализа.

Итог главы. Остаётся открытым счётное ядро — узлы (1) и (2): на каждом $N$ носитель выше $N$ строго перевешивает множество плохих, $|\mathit{bad}| < |\mathit{carrier}|$.

Естественно предположить, что этот перевес обеспечивается структурной эксклюзивностью двойки (глава 02 Carrier): простой $p>2$ делит не более одной из сторон $6m\pm 1$, поскольку $\gcd(6m-1, 6m+1) \mid 2$. Из этой эксклюзивности плохие классы по разным простым не могут «складываться свободно» — они частично исключают друг друга, и суммарная плохая доля не покрывает носитель.

План закрытия таков: перевести перевес $|\mathit{bad}| < |\mathit{carrier}|$ в неравенство на счётах низкого и высокого рангов и доказать это неравенство комбинаторно, а не через плотность простых.

Именно к этому переводу мы переходим в следующей главе [12 four-corner]: там эксклюзивность двойки оформляется как отрицательная ассоциация рангов сторон — перекрёстный член запрещён, производящая функция раскладывается в произведение $\prod_p (c_p + a_p x + b_p y)$ без члена $xy$, — и это даёт четырёхугольное неравенство $N_{00}N_{33} \le N_{03}N_{30}$, из которого извлекается искомый перевес носителя над плохими. Так открытое счётное ядро настоящей главы получает свой конкретный комбинаторный маршрут.

← 10. survivor ⇒ twin · Оглавление · 12. Four-corner →