Перейти к содержанию

15. Цепь к близнецам из four-corner (условно)

← 14. Декомпозиция остатка · Оглавление · 16. От противного →

Lean-источник: EuclidsPath/Engine/ToTwins.lean (twin_primes_of_four_corner). Опирается на: EuclidsPath/Engine/FourCorner.lean, EuclidsPath/Engine/TwoTransport.lean, EuclidsPath/Engine/NonCover.lean, EuclidsPath/Step00_Overview.lean.

В предыдущей главе мы получили точную декомпозицию остатка: реальные ранговые счёты раскладываются в модельную (CRT) часть плюс поправку \(e_{ij}\), и весь вопрос о переносе модель→реальность свёлся к тому, перевернёт ли остаток знак модельного four-corner. Теперь мы делаем следующий, чисто сборочный шаг: показываем, что если реальный строгий four-corner действительно держится на всех масштабах, то отсюда механически следует бесконечность простых-близнецов.

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

15.1. Постановка: что именно мы собираем

Напомним рабочие определения, зафиксированные в обзорном модуле Step00_Overview.lean.

Определение 15.1 (IsTwinCenter). Центр \(m\) задаёт пару близнецов, если обе стороны шестёрочного окна простые:

\[ \mathrm{IsTwinCenter}(m) \;:\Longleftrightarrow\; (6m-1)\ \text{простое}\ \wedge\ (6m+1)\ \text{простое}. \]

Определение 15.2 (TwinLowers). Множество младших членов пар близнецов —

\[ \mathrm{TwinLowers} \;=\; \{\,p \mid p\ \text{простое}\ \wedge\ (p+2)\ \text{простое}\,\}, \]

и конечная цель всей цепочки — утверждение TwinLowers.Infinite, то есть бесконечность этого множества.

Наша задача в этой главе — предъявить теорему вида

\[ (\text{реальный four-corner на всех масштабах}) \;\Longrightarrow\; \mathrm{TwinLowers}.\mathrm{Infinite}, \]

в которой посылка — единственная гипотеза, а импликация целиком машинно проверена без sorry. Все промежуточные звенья к этому моменту уже доказаны в отдельных модулях; здесь они соединяются в один вывод.

15.2. Четыре верифицированных звена

Цепь собирается из четырёх ранее доказанных утверждений. Перечислим их с точными Lean-именами и поясним, что делает каждое.

Звено 1 — четырёхугольный переход (строгий).

Лемма 15.3 (N33_lt_N00_of_four_corner). При \(N_{00}>0\), строгом four-corner \(N_{00}\cdot N_{33} < N_{03}\cdot N_{30}\) и side-corner \(N_{03}\cdot N_{30} \le N_{00}^2\) следует

\[ N_{33} < N_{00}. \tag{15.1} \]

Доказательство элементарно и чисто арифметично: из \(N_{00}N_{33} < N_{03}N_{30} \le N_{00}^2\) имеем \(N_{00}N_{33} < N_{00}N_{00}\), а сокращение на положительный множитель \(N_{00}\) (лемма lt_of_mul_lt_mul_left) даёт \(N_{33}<N_{00}\).

Примечание. Роль side-corner здесь — единственная: перегнать неравенство про произведение диагоналей \(N_{03}N_{30}\) в неравенство про квадрат базового ранга \(N_{00}^2\). Именно тогда строгое four-corner становится сравнением \(N_{00}N_{33}\) с \(N_{00}^2\), откуда и падает \(N_{33}<N_{00}\). Без side-corner four-corner сам по себе не контролирует \(N_{33}\) относительно \(N_{00}\). Поэтому в гипотезе H side-corner фигурирует как отдельный, «лёгкий» конъюнкт.

Звено 2 — non-cover даёт выжившего.

Лемма 15.4 (survivor_of_not_covered). Если для конечных множеств \(\Omega\) (carrier) и \(\mathrm{bad}\) выполнено \(|\mathrm{bad}| < |\Omega|\), то существует \(m\in\Omega\) с \(m\notin\mathrm{bad}\). Это чистая Finset-комбинаторика: будь \(\Omega\subseteq\mathrm{bad}\), было бы \(|\Omega|\le|\mathrm{bad}|\) — противоречие. Содержательно: «плохих» центров слишком мало, чтобы накрыть весь carrier, поэтому хотя бы один центр выживает.

Звено 3 — блочное ядро.

Теорема 15.5 (twin_prime_conjecture_of_blocks). Из посылки

\[ \forall N,\ \exists\,\text{carrier},\ \text{bad}:\quad (\forall m\in\text{carrier},\ N<m)\ \wedge\ |\text{bad}|<|\text{carrier}|\ \wedge\ (\forall m\in\text{carrier},\ m\notin\text{bad}\Rightarrow\mathrm{IsTwinCenter}(m)) \tag{15.2} \]

следует TwinLowers.Infinite. Она через вспомогательную twin_center_of_block вытаскивает выжившего (звено 2, лемма 15.4), помещает его выше \(N\) и по условию «survivor \(\Rightarrow\) twin» опознаёт его как twin-центр.

Звено 4 — неограниченность даёт бесконечность.

Теорема 15.6 (infinite_of_unbounded_centers). Если для любого \(N\) найдётся twin-центр \(m>N\), то TwinLowers.Infinite. Формально она использует Set.infinite_of_not_bddAbove — из центра \(m>N\) строится член пары \(6m-1\), больший \(N\), поэтому множество младших близнецов не ограничено сверху, а значит бесконечно.

15.3. Главная теорема

Соединяя четыре звена, получаем условную теорему twin_primes_of_four_corner. Сформулируем её гипотезу \(H\) явно.

Гипотеза H (реальный four-corner на всех масштабах). Для каждого \(N\in\mathbb{N}\) существуют конечные множества рангов \(R_{00}, R_{03}, R_{30}, R_{33}\) и множества \(\mathrm{carrier}, \mathrm{bad}\) такие, что

\[ 0 < |R_{00}|,\qquad |R_{00}|\cdot|R_{33}| \;<\; |R_{03}|\cdot|R_{30}| \quad(\text{строгий four-corner}), \]
\[ |R_{03}|\cdot|R_{30}| \;\le\; |R_{00}|^2 \quad(\text{side-corner, лёгкий}), \]
\[ |\mathrm{carrier}| = |R_{00}|,\qquad |\mathrm{bad}| = |R_{33}|, \]
\[ (\forall m\in\mathrm{carrier},\ N<m),\qquad (\forall m\in\mathrm{carrier},\ m\notin\mathrm{bad}\Rightarrow\mathrm{IsTwinCenter}(m)). \]

Содержательно \(H\) говорит: на сколь угодно большом масштабе \(N\) находится блок, где carrier отождествлён с рангом-\((0,0)\), плохое множество — с рангом-\((3,3)\), реальные ранговые счёты дают строгий four-corner (плюс лёгкий side-corner), весь carrier лежит выше \(N\), а каждый выживший carrier-центр — twin.

Теорема 15.7 (twin_primes_of_four_corner). 🟢 (зелёная условная теорема: без аксиом, при названном входе \(H\))

\[ H \;\Longrightarrow\; \mathrm{TwinLowers}.\mathrm{Infinite}. \tag{15.3} \]

Разбор доказательства. Применяем теорему 15.5 (twin_prime_conjecture_of_blocks) — остаётся для каждого \(N\) предъявить блок с \(|\mathrm{bad}| < |\mathrm{carrier}|\). Раскрываем \(H\,N\), получая ранги, carrier, bad и все семь конъюнктов.

Ключевой шаг — звено 1 (лемма 15.3):

\[ |R_{33}| < |R_{00}| \quad\text{через}\quad `N33_lt_N00_of_four_corner`\ (h_{\text{pos}}, h_{\text{fc}}, h_{\text{sc}}). \]

Затем по тождествам \(|\mathrm{carrier}|=|R_{00}|\) и \(|\mathrm{bad}|=|R_{33}|\) переписываем это неравенство в \(|\mathrm{bad}| < |\mathrm{carrier}|\) — ровно посылка блочного ядра.

Условия «carrier выше \(N\)» и «survivor \(\Rightarrow\) twin» передаются из \(H\) без изменений. На этом машинная цепь замыкается: теорема 15.5 (twin_prime_conjecture_of_blocks) возвращает TwinLowers.Infinite.

Примечание. В файле нет sorry. Это честная условная теорема: заключение (гипотеза близнецов) следует из явного входа \(H\). Мы никогда не выдаём эту редукцию за доказательство гипотезы близнецов — доказано ровно то, что написано в сигнатуре: импликация \(H\Rightarrow\) TwinLowers.Infinite. Всё нетривиальное содержание вынесено в посылку \(H\).

15.4. Почему граница проходит именно здесь

Естественно спросить: почему открытым остаётся ровно \(H\), а не что-то ещё? Наблюдение состоит в том, что каждое из четырёх звеньев distribution-free — они не апеллируют ни к анализу, ни к распределению простых:

  • звено 1 — арифметика натуральных (сокращение неравенства на положительный множитель);
  • звено 2 — принцип Дирихле в форме Finset.card_le_card;
  • звено 3 — комбинаторная сборка выжившего;
  • звено 4 — «неограничено сверху \(\Rightarrow\) бесконечно» для множеств.

Ни одно из них не «знает» о простых числах ничего сверх определения IsTwinCenter. Всё аналитически трудное — распределительное — оказывается сосредоточено внутри \(H\), а именно в двух его конъюнктах:

  1. строгий реальный four-corner \(|R_{00}|\,|R_{33}| < |R_{03}|\,|R_{30}|\) на всех масштабах — это перенос модельного (CRT) four-corner на реальные ранговые счёты, то есть контроль остатка \(e_{ij}\) из главы 14; по своей природе это задача о чётности и остаточном члене сита;
  2. carrier-условия — что carrier лежит выше \(N\) и что каждый выживший — twin (нижняя оценка плотности плюс элементарное «сито-до-корня \(\Rightarrow\) простота», ср. isTwinCenter_of_root_sieve в TwoTransport.lean).

Примечание. Комментарий Lean-источника фиксирует статус прямо: модельный four-corner уже доказан (ModelFourCorner), открыт ровно перенос модель→реальность. Эмпирика из tools/RESULTS_remainder.md (глава 14) показывает, что остаток \(e_{ij}\) примерно вчетверо превосходит модель при тающем зазоре модельного four-corner — то есть модельное неравенство не переносится distribution-free. Здесь линия упирается в проблему чётности, и это не дефект сборки, а точная локализация единственного нерешённого узла.

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

Примечание. Гипотеза \(H\) в этой формулировке — прямой предшественник более поздней, не-счётной переформулировки узла (линия 18, SNOL: twin_primes_of_SNOL в SNOL.lean использует тот же мост twin_prime_conjecture_of_blocks). Там открытое ядро вынесено из счётного языка рангов в структурный предикат; но логический скелет — «блок \(\Rightarrow\) выживший \(\Rightarrow\) twin \(\Rightarrow\) бесконечность» — остаётся тем же, что собран здесь.

15.5. План закрытия

Закрыть \(H\) означает установить два его аналитических конъюнкта на реальных интервалах: предъявить строгий реальный four-corner на сколь угодно больших масштабах (перенос модели через контроль остатка \(e_{ij}\), глава 14) и обеспечить carrier-оценку с распознаванием выжившего как twin. Первый конъюнкт — задача о чётности и остаточном члене сита; второй — нижняя оценка плотности carrier. Оба, по имеющимся численным данным, distribution-free из текущих идей не следуют.

Явная, изолированная форма \(H\) ровно и нужна для того, чтобы дальнейшая работа била в одну точно очерченную мишень, а не в размытую совокупность лемм.

Собрав прямую импликацию \(H\Rightarrow\) TwinLowers.Infinite, естественно посмотреть на неё с другой стороны — от противного. В следующей главе мы берём контрапозицию всей программы: предполагаем, что близнецов конечно, и показываем, что вместе с тем же входом \(H\) это ведёт к противоречию (twin_finite_contradiction).

Мы увидим, что доказательство от противного не даёт нового рычага — оно перекодирует ту же самую four-corner/carrier/parity-стену, — но зато даёт чистый верифицированный вердикт: конечность близнецов противоречива по модулю \(H\), а \(H\) — единственный, точно локализованный открытый вход.

← 14. Декомпозиция остатка · Оглавление · 16. От противного →