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

10. Survivor значит twin: мост к бесконечности

← 09. Factor-repeat rigidity · Оглавление · 11. Блочное ядро →

Lean: EuclidsPath/Engine/NonCover.lean (survivor_of_not_covered, infinite_of_unbounded_centers); EuclidsPath/Engine/TwoTransport.lean (prime_of_no_small_prime_factor, isTwinCenter_of_root_sieve).

В предыдущей главе 09 мы установили жёсткость повторного делителя: если простой ℓ возвращается делителем на двух центрах, он делит их разность, а значит попадания одного делителя ригидно периодичны. Это делает суммарное покрытие «плохими» центрами коротким и подконтрольным. Теперь мы собираем плоды: покажем, что как только «плохих» строго меньше, чем несущих, из блока падает выживший, и что выживший — не просто не-плохой центр, а настоящий twin-центр; из неограниченного запаса таких центров мы честно, машинно-проверенно, выводим бесконечность простых-близнецов.

Постановка: три звена одного моста

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

Определение 10.1 (twin-центр и TwinLowers). Индексная (центровая) форма пары близнецов: центр \(m\) задаёт пару, если оба соседа шестёрки просты. Формально IsTwinCenter:

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

Целевое множество — младшие члены пар, TwinLowers \(= \{\,p \mid p\ \text{и}\ p+2\ \text{просты}\,\}\); гипотеза близнецов есть в точности TwinLowers.Infinite.

Три звена таковы:

  1. Non-cover \(\Rightarrow\) выживший (survivor_of_not_covered): чистая мощностная комбинаторика Finset.
  2. Сито-до-корня \(\Rightarrow\) простота (prime_of_no_small_prime_factor), откуда survivor \(\Rightarrow\) twin (isTwinCenter_of_root_sieve): элементарная теория делимости.
  3. Неограниченность центров \(\Rightarrow\) бесконечность (infinite_of_unbounded_centers): порядковый переход от «сколь угодно высоко» к «бесконечно».

Разберём их по очереди — что доказано, почему именно так, и что каждое звено значит для программы.

Звено 1. Non-cover даёт выжившего

Пусть на некотором масштабе мы выделили конечное несущее множество центров \(\Omega\) (carrier) и конечное множество \(\mathrm{bad}\) «плохих» центров — тех, что заведомо не годятся (одна из сторон \(6m\pm1\) составная, потому что её накрыл какой-то запрещающий делитель). Единственное, что нам нужно от комбинаторного ядра, — это строгое неравенство мощностей.

Определение 10.2 (non-cover). Говорим, что bad не покрывает Ω, если

\[ |\mathrm{bad}| < |\Omega|. \]

Теорема 10.3 (survivor_of_not_covered). Если \(|\mathrm{bad}| < |\Omega|\), то существует \(m \in \Omega\) с \(m \notin \mathrm{bad}\).

\[ |\mathrm{bad}| < |\Omega| \;\Longrightarrow\; \exists\, m \in \Omega,\; m \notin \mathrm{bad}. \tag{10.1}\]

Доказательство — принцип Дирихле в чистейшем виде. От противного: если бы каждый \(m \in \Omega\) лежал в \(\mathrm{bad}\), то \(\Omega \subseteq \mathrm{bad}\), откуда по монотонности мощности \(|\Omega| \le |\mathrm{bad}|\) — противоречие с посылкой. В Lean это ровно три хода: by_contra, построение включения \(\Omega \subseteq \mathrm{bad}\), затем Finset.card_le_card и omega.

Примечание. Заметим, что здесь нет ни анализа, ни распределения простых, ни аналитического сита — только Finset и порядок на \(\mathbb{N}\). Это принципиально: вся аналитическая трудность программы вынесена наружу, в оценку двух мощностей (\(|\Omega|\) снизу, \(|\mathrm{bad}|\) сверху). Само наличие выжившего при выполненном неравенстве не стоит нам ничего.

Почему именно строгое неравенство, а не, скажем, положительная плотность выживших? Потому что для моста к бесконечности (звено 3) достаточно одного выжившего на каждом масштабе. Экономность посылки — не слабость, а точность: мы просим у открытого ядра ровно столько, сколько несёт вывод, и ни граммом больше. Это делает редукцию максимально «дешёвой» по входу и потому максимально честной.

Звено 2. Сито до корня даёт простоту; выживший — это twin

Выживший \(m \notin \mathrm{bad}\) — это центр, ни одна сторона которого не была накрыта запрещающими делителями в пределах масштаба. Чтобы превратить «не накрыт» в «прост», нужен классический факт: пробное деление до квадратного корня решает вопрос простоты.

Теорема 10.4 (prime_of_no_small_prime_factor). Пусть \(n \ge 2\) и ни один простой \(p\) с \(p^2 \le n\) не делит \(n\). Тогда \(n\) просто.

\[ n \ge 2 \;\wedge\; \bigl(\forall p\ \text{prime},\; p^2 \le n \Rightarrow p \nmid n\bigr) \;\Longrightarrow\; n\ \text{простое}. \tag{10.2}\]

Доказательство от противного через минимальный простой делитель Nat.minFac. Если \(n\) составное, то \(p := \mathrm{minFac}(n)\) прост и делит \(n\); из минимальности \(p \le n/p\), откуда \(p \cdot p \le p \cdot (n/p) \le n\), то есть \(p^2 \le n\). Но тогда \(p\) — простой делитель \(n\) с \(p^2 \le n\), что противоречит посылке. Ключевой шаг в Lean — Nat.minFac_le_div (минимальный делитель не превосходит частного), дающий \(p \le n/p\); отсюда Nat.mul_le_mul и Nat.mul_div_le собирают неравенство \(p^2 \le n\).

Примечание. Именно поэтому сито «до корня», а не до самого \(n\): наименьший делитель составного числа всегда не больше \(\sqrt{n}\). Проверив все простые до корня и не найдя делителя, мы исчерпали всех кандидатов — оставаться числу нечего, кроме как быть простым.

Применяя это к обеим сторонам центра, получаем целевую импликацию survivor \(\Rightarrow\) twin.

Теорема 10.5 (isTwinCenter_of_root_sieve). Если \(6m-1 \ge 2\) и \(6m+1 \ge 2\), и ни один простой до корня не делит соответствующую сторону, то \(m\) — twin-центр:

\[ \Bigl(\forall p\ \text{prime},\; p^2 \le 6m-1 \Rightarrow p \nmid (6m-1)\Bigr) \;\wedge\; \Bigl(\forall p\ \text{prime},\; p^2 \le 6m+1 \Rightarrow p \nmid (6m+1)\Bigr) \;\Longrightarrow\; \mathrm{IsTwinCenter}(m). \tag{10.3}\]

Доказательство — просто пара обращений к Теореме 10.4 (prime_of_no_small_prime_factor) для \(6m-1\) и \(6m+1\), упакованная в конъюнкцию IsTwinCenter. Содержательно это и есть утверждение «выживший значит twin» из заголовка: если сито активной части двигателя дошло до корня и не срубило ни одну сторону, обе стороны просты — а это по определению twin-центр.

Примечание. Этот шаг фиксирует важную границу трудности. Направление survivor \(\Rightarrow\) twin элементарно — оно не содержит никакой гипотезы. Значит, вся содержательная работа программы сосредоточена не здесь, а в том, чтобы гарантировать, что выживший, найденный звеном 1, действительно «просеян до корня» (то есть bad учитывает все делители до \(\sqrt{6m+1}\), а не только малые). Естественно предположить, что это и есть настоящее carrier/bad-условие; именно оно остаётся открытым узлом и передаётся дальше.

Звено 3. Неограниченность центров даёт бесконечность

Осталось перейти от «на каждом масштабе есть twin-центр выше \(N\)» к безусловной бесконечности множества TwinLowers.

Теорема 10.6 (infinite_of_unbounded_centers). Если для любого \(N\) найдётся центр \(m > N\) с \(\mathrm{IsTwinCenter}(m)\), то TwinLowers бесконечно:

\[ \bigl(\forall N,\ \exists m,\ N < m \wedge \mathrm{IsTwinCenter}(m)\bigr) \;\Longrightarrow\; \texttt{TwinLowers.Infinite}. \tag{10.4}\]

Доказательство порядковое, через Set.infinite_of_not_bddAbove: множество натуральных чисел бесконечно тогда и только тогда, когда оно не ограничено сверху. Развернув not_bddAbove_iff, для произвольного \(N\) берём центр \(m > N\) и предъявляем свидетеля \(6m-1 \in \texttt{TwinLowers}\): он больше \(N\) (так как \(6m-1 > m > N\)), и он — младший член пары, ведь \(6m-1\) прост, а \((6m-1)+2 = 6m+1\) тоже прост (обе части даёт IsTwinCenter). Тождество \(6m-1+2 = 6m+1\) и оценка \(6m-1 > N\) закрываются omega.

Примечание. Тонкость, которую стоит проговорить: неограниченность центров \(m\) автоматически даёт неограниченность младших членов \(6m-1\), потому что \(6m-1\) монотонно растёт с \(m\). Поэтому «сколь угодно высокий центр» превращается в «сколь угодно большой элемент TwinLowers», а для множества в \(\mathbb{N}\) этого достаточно для бесконечности. Никакого пересчёта или инъекции строить не нужно — хватает отсутствия верхней грани.

Что собрано и где проходит честная граница

Соберём три звена в один вывод. Предположим блочное ядро: для каждого \(N\) существуют конечные \(\mathrm{carrier}\) и \(\mathrm{bad}\) такие, что все центры carrier лежат выше \(N\), \(|\mathrm{bad}| < |\mathrm{carrier}|\), и каждый выживший carrier есть twin-центр. Тогда Теорема 10.3 (survivor_of_not_covered) даёт выжившего \(m\), условие блока делает его twin-центром выше \(N\) (это twin_center_of_block), а Теорема 10.6 (infinite_of_unbounded_centers) превращает произвольность \(N\) в TwinLowers.Infinite. Именно эта сборка и есть twin_prime_conjecture_of_blocks — предмет следующей главы.

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

Сформулируем открытый узел явно.

Гипотеза 10.7 (блочное non-cover, открыто). На сколь угодно больших масштабах \(N\) существует несущее множество центров \(\mathrm{carrier}\) выше \(N\), для которого множество «плохих» центров \(\mathrm{bad}\) (тех, у кого одна из сторон \(6m\pm1\) имеет делитель до корня) строго меньше по мощности: \(|\mathrm{bad}| < |\mathrm{carrier}|\).

План закрытия. Узел распадается надвое, и обе части — предмет линий [12–18]: оценка \(|\mathrm{carrier}|\) снизу (плотность несущих классов, CarrierInput) и оценка \(|\mathrm{bad}|\) сверху через ригидность повторных делителей из 09 и короткость покрытия из 07–08. Из наблюдения звена 2 добавляется требование полноты сита: bad должен учитывать все делители до \(\sqrt{6m+1}\), иначе выживший не гарантированно twin. Как только оба счёта сойдутся в строгое неравенство мощностей хотя бы на одной последовательности масштабов, все три звена этой главы срабатывают автоматически и дают бесконечность.

Три доказанных звена — это готовая арматура моста; чего недостаёт, так это гарантии, что пролёт \(|\mathrm{bad}| < |\mathrm{carrier}|\) выдерживает нагрузку на каждом масштабе. Как именно эта арматура собирается в единый машинно-проверенный нециркулярный мост «гипотеза \(\Longleftarrow\) блочное ядро» — предмет следующей главы 11 TwoTransport, где twin_prime_conjecture_of_blocks изолирует открытое ядро и передаёт его дальше по цепочке.

← 09. Factor-repeat rigidity · Оглавление · 11. Блочное ядро →