16. От противного: finite и H дают False¶
← 15. Цепь к близнецам · Оглавление · 17. Закон оплаты →
В главе 15 ToTwins мы собрали прямую цепь: из реального four-corner на всех масштабах вытекает TwinLowers.Infinite — бесконечность близнецов. Теперь мы посмотрим на ту же конструкцию с обратной стороны: предположим противное — что близнецов конечно — и покажем, что вместе с четырёхугольным входом это ведёт к False. Это не новая теорема, а контрапозиция всей программы, и её ценность в том, что она с математической точностью локализует единственный открытый узел.
Машинно проверено:
Engine/FiniteContradiction.lean(twin_finite_contradiction, безsorry, аксиомы только стандартные).
Постановка от противного¶
Введём объект, конечность которого и есть отрицаемая гипотеза. Пусть TwinLowers — множество нижних членов близнецовых пар, то есть множество тех \(n\), для которых оба числа \(n\) и \(n+2\) просты (в терминах двигателя — центров \(m\) с обеими сторонами \(6m\pm 1\) простыми). Гипотеза о бесконечности близнецов есть в точности утверждение TwinLowers.Infinite. Её отрицание записывается как
что для множеств равносильно TwinLowers.Finite. Содержательно это значит: существует последний twin-центр \(M_0\), за которым каждый центр \(m > M_0\) плох — хотя бы одна из сторон \(6m\pm 1\) составная.
Второй ингредиент — открытый вход. В файле он вводится как сокращение, дословно совпадающее с посылкой twin_primes_of_four_corner из предыдущей главы:
Определение 16.1 (открытый вход программы). Сокращение FourCornerInput: для каждого масштаба \(N\) существуют конечные множества \(R_{00}, R_{03}, R_{30}, R_{33},\ \mathrm{carrier},\ \mathrm{bad}\), удовлетворяющие
Первое неравенство \(|R_{00}|\cdot|R_{33}| < |R_{03}|\cdot|R_{30}|\) — это строгий реальный four-corner на настоящих ранговых счётах; второе, \(|R_{03}|\cdot|R_{30}| \le |R_{00}|^2\), — лёгкий side-corner. Вместе они, как показано в 15 ToTwins через N33_lt_N00_of_four_corner, дают \(|R_{33}| < |R_{00}|\), то есть плохих центров в блоке строго меньше, чем carrier-мест, — а значит хотя бы один выживший, и он twin.
Теорема о противоречии¶
Собственно противоречие формулируется одной строкой.
Теорема 16.2 (twin_finite_contradiction). Если \(\neg\,\mathtt{TwinLowers.Infinite}\) (близнецов конечно) и выполнен FourCornerInput H, то False.
Доказательство прозрачно: из H прямая цепь предыдущей главы (twin_primes_of_four_corner) выдаёт TwinLowers.Infinite; применяя к этому гипотезу конечности hfin, получаем False. В Lean это буквально hfin (twin_primes_of_four_corner H) — конечность есть функция «из бесконечности в пустоту», и мы скармливаем ей ровно ту бесконечность, которую производит четырёхугольник.
Тот же факт переформулирован через явную конечность множества:
Теорема 16.3 (twin_finite_contradiction_of_finite). Если TwinLowers.Finite и FourCornerInput H, то False.
Единственное отличие — переход Set.not_infinite.mpr, снимающий разницу между Finite и ¬ Infinite; содержательно это та же теорема, записанная так, чтобы её было удобно применять там, где конечность дана как Finite, а не как отрицание.
Наконец, контрапозиция извлекается в чистом виде:
Теорема 16.4 (twin_infinite_of_fourCorner). Из FourCornerInput H следует TwinLowers.Infinite.
Это тождественно twin_primes_of_four_corner H — мы лишь даём выводу имя, подчёркивающее логическую роль: H опровергает конечность. Три теоремы (16.2, 16.3, 16.4) — одно и то же утверждение в трёх грамматических залогах (противоречие, противоречие-через-Finite, прямой вывод), и наличие всех трёх в файле — не избыточность, а карта того, как одна и та же импликация встраивается в разные контексты доказательства.
Примечание. Логически контрапозиция ничего не добавляет: \((\neg P \wedge H \to \bot)\) и \((H \to P)\) равносильны. Ценность формы «от противного» — методологическая: она делает осязаемым, что именно ломается при отрицании тезиса. Если близнецов конечно, двигатель обязан обработать весь бесконечный хвост \((M_0,\infty)\) так, чтобы плохие центры покрывали его целиком, не оставив ни одного выжившего.
Hутверждает обратное — что на каждом масштабе выживший есть. Совместить нельзя, и это несовместимость и естьFalse.
Почему все маршруты упираются в одну стену¶
Естественно спросить: не даёт ли рассуждение от противного нового рычага — быть может, отрицание тезиса открывает обход открытого узла? Независимая разведка тремя линзами — counting, EPMI, four-corner — дала единый ответ: ни один маршрут не обходит стену, все сводятся к строгому реальному four-corner и оценке carrier снизу. Сведём наблюдение в таблицу.
| Маршрут | Где живёт открытое | Почему это красная линия |
|---|---|---|
| Counting (union bound по простым) | \(2\!\sum_{A<p\le\sqrt X} 1/p < \text{density}\) | По Мертенсу \(\sum 1/p \to \infty\), поэтому union bound никогда не побивает carrier; починка только через включения-исключения Бруна, а её главный член \(\prod(1-2/p)\cdot\lvert\Omega\rvert\) и контроль остатка на реальном интервале — это Бомбьери–Виноградов, то есть распределение простых. |
| EPMI (бесконечный спуск) | «изготовить тотальную цепь спуска \(H:\mathbb N\to\mathbb N\)» | Инвертирует бремя: чтобы применить no_infinite_descent, нужна вечная цепь спуска, а «покрытие тотально» — это ровно то, что требуется опровергнуть, а не предположить. Орфан-ветка, ни на что на живой линии не опирающаяся. |
| Four-corner (этот файл) | конъюнкт «строгий реальный four-corner» в H |
Перенос модель\(\to\)реальность (real_four_corner_of_remainder): харнесс tools/RESULTS_remainder.md показывает, что остаток \(\sim 4\times\) модели, а зазор модели тает — модельный four-corner не переносится distribution-free. Это чётность. |
Вывод разведки дословно: «No route escapes the four-corner/carrier/parity wall; all three reduce to it. The machine-checked links are all distribution-FREE and red-line-clean; distribution is quarantined entirely inside H.» Три разных начала — счёт простых, бесконечный спуск, четырёхугольник — сходятся в одну точку, и это схождение само по себе есть свидетельство: стена структурна, а не артефакт одного выбора маршрута.
Примечание. Схождение трёх маршрутов имеет геометрический образ. Реальный four-corner держится, пока margin — зазор \(|R_{03}|\cdot|R_{30}| - |R_{00}|\cdot|R_{33}|\), нормированный на масштаб блока, — остаётся положительным. Численно margin ползёт к нулю: это knife-edge, лезвие ножа. И тает он не по случайной причине, а потому что остаток \(e_{ij}\) реальных счётов относительно модели CRT 14 RealFourCorner несёт ту же знаковую структуру, что и в решете чувствительна к чётности числа простых множителей. Иными словами, margin\(\to 0\) — это не «почти получилось», а проявление проблемы чётности: distribution-free методы принципиально не различают знак, от которого зависит перевес four-corner.
Что доказано честно — и что нет¶
Разграничим строго. Доказана условная теорема (Теорема 16.2) finite ∧ H ⟹ False — машинно, без sorry, на стандартных аксиомах. Это корректно собранное, полное на уровне модели противоречие: каждое звено склейки (16.4)
проверено и distribution-free. Открытым остаётся ровно H (Определение 16.1), и внутри H содержательно открыт единственный конъюнкт — строгий реальный four-corner (= чётность + перенос модель\(\to\)реальность) вместе с нижней оценкой carrier (= плотность). Модельная сторона (four_corner_binom_strict, model_four_corner) уже доказана безусловно; не переносится именно шаг от модели к реальности.
Гипотеза (открытый узел).
FourCornerInputHистинна: на сколь угодно больших масштабах реальные ранговые счёты дают строгий four-corner. План закрытия: контроль остатка \(e_{ij}\) на настоящем интервале с точностью, достаточной, чтобы удержать знак margin положительным. Из имеющихся идей это distribution-free не следует — что подтверждено и численно (margin\(\to 0\), остаток \(\sim 4\times\) модели). Честный статус:H— типизированная гипотеза, а не доказанный факт, и мы нигде не выдаём редукцию к ней за доказательство самого тезиса.
Итог и мост к следующей главе¶
Рассуждение от противного не даёт нового рычага: оно перекодирует ту же стену — «union bound покрывает интервал» и «остаток переворачивает four-corner» суть одно и то же parity/sieve-remainder-препятствие. Но оно даёт чистый верифицированный артефакт: конечность близнецов противоречива по модулю H, а H — единственный, точно локализованный, открытый вход всей программы.
Естественно спросить дальше: если двигатель всё же вынужден остановиться на плохом центре — во что ему это обходится? Отрицание тезиса требует, чтобы весь хвост \((M_0,\infty)\) был покрыт плохими, то есть чтобы двигатель бесконечно часто «платил» на границе. В главе [17 закон оплаты] мы перейдём от логики противоречия к его алгебре: покажем, что boundary-смерть не бесплатна, что оплата распределена по малым простым и подчинена строгому закону дефекта, — и увидим, как та же parity-стена проступает с нового, более арифметического ракурса.