Стороны сетки и узоры Полиньяка: одиночки зелёные, пары — гипотезы

← 43. Мерсенн через первопричину · Оглавление · 45. Софи Жермен →

Lean-источник: Engine/SideInfinitude.lean — хребет честности, вся 🟢 (Дирихле из mathlib); Engine/PolignacBranch.lean — классификация кузенов и секси в сетке, вся 🟢; Engine/PolignacManifestationFront.lean — две манифестационные ветви, вся 🟢 (деклараций нет). Проза-контекст: 43. Мерсенн через первопричину, 38. Риман через первопричину. Обозначения статуса: 🟢 — доказано при стандартных аксиомах; 🟡 — условно на аксиому step00FirstCause; 🔴 — открытый вход.

Где мы

Глава 43 впервые оставила машинно-допустимую границу декрета не взятой — по знаку эвристики. Мерсенн-близнецы отвечали за одну редкую подпоследовательность экспонент; здесь мы разворачиваемся к самому широкому классу открытых парных задач — к малым чётным зазорам между простыми, к гипотезе Полиньяка. И начинаем не с гипотезы, а с того, что от неё честно отделено.

Ибо у парных задач есть коварная лёгкость: кажется, будто «простых вида 6m ± 1 бесконечно много» уже почти решает всё. Это не так, и провести границу между решённым и открытым — первая обязанность главы. Одиночки зелёные; согласование одиночек в пару — вся открытая суть. Вокруг этого хребта мы и построим две новые манифестационные ветви (манифестация — принцип «отклонение обязано проявиться», см. словарь) — кузенов (зазор 4) и секси (зазор 6), — точные зеркала мерсенновской, с одним новым поворотом честности, которого не было ни у Римана, ни у Мерсенна.

Хребет честности: каждая сторона порознь бесконечна

Сетка 6m ± 1 даёт каждому центру m две стороны — минус-сторону 6m − 1 (класс 5 mod 6) и плюс-сторону 6m + 1 (класс 1 mod 6). Вопрос «бесконечно ли простых на каждой стороне порознь» давно закрыт, и закрыт тяжёлой аналитикой:

Теорема 44.1 (minusSide_primes_unbounded, plusSide_primes_unbounded, 🟢). Над любым n есть простое p > n с p % 6 = 5; и есть простое p > n с p % 6 = 1.

Почему это верно. Это теорема Дирихле о простых в арифметических прогрессиях, взятая у mathlib целиком — Nat.forall_exists_prime_gt_and_modEq, за которой стоит вся машинерия L-рядов и не-обнуления L(1, χ). Классы 1 и 5 по модулю 6 взаимно просты с 6, значит каждый несёт бесконечно много простых.

В форме множеств это minusSide_primes_infinite и plusSide_primes_infinite (🟢): оба множества {p : p.Prime ∧ p % 6 = 5} и {p % 6 = 1} — Set.Infinite. Ни одной новой теоремы чисел мы здесь не доказываем — мы одалживаем готовую и переводим её в центровой язык программы (minusSide_center_unbounded, plusSide_center_unbounded): над любым n есть центр с простой минус-стороной, и, отдельно, центр с простой плюс-стороной.

И вот несущая стена, ради которой модуль существует. Про один и тот же центр эти теоремы не говорят ничего.

Примечание. Маркер NoPairingClaimed (🟢, abbrev … := True) — это подпись под честностью, а не теорема с содержанием. Дирихле даёт две независимые бесконечные шеренги простых — по минус-стороне и по плюс-стороне, — но молчит о том, что они бесконечно часто выстраиваются напротив друг друга, в общем центре m.

Одновременная простота 6m − 1 и 6m + 1 — это гипотеза близнецов, и здесь она не утверждается, не доказана и ниоткуда не выводится. Весь открытый вес парных задач лежит ровно в этом зазоре между «каждая сторона бесконечна» и «стороны совпадают бесконечно часто».

Примечание (якорь ограниченных зазоров). Тот же зазор виден и с другой стороны — со стороны ограниченных промежутков между простыми. Модуль Engine/BoundedGapsAnchor.lean называет предикат BoundedGaps B («бесконечно много пар простых с зазором ≤ B») и два честных неформализованных входа: ZhangAnchor (Чжан 2013, B = 7·10⁷) и MaynardTaoAnchor (Мейнард–Тао 2014, B = 246) — лучший безусловный результат человечества, которого в mathlib нет. Аудит на переименование boundedGaps_two_iff_twins вскрывает машинно, что край B = 2 буквально равносилен гипотезе близнецов: назвать BoundedGaps 2 — значит назвать близнецов, и переименование раскрыто iff-теоремой, а не спрятано. А спуск 246 → 2 — открытая математика, честно не заявленная: монотонность boundedGaps_mono работает лишь вверх по планке, ниже 6 сита упираются в parity problem Сельберга.

Кузены: перекрёстная пара соседних центров

Малые зазоры сетка кодирует геометрически, и код прозрачен. Зазор 2 (близнецы) — это один центр m, пара (6m − 1, 6m + 1).

Зазор 4 (кузены, p и p + 4) — это соседние центры и разные стороны: пара (6m + 1, 6m + 5), где старший член опознаётся тождеством 6m + 5 = 6(m + 1) − 1 (cousin_upper_eq_minusSide, 🟢). Иначе говоря, младший кузен — плюс-сторона центра m, старший — минус-сторона следующего центра m + 1. Пара перекидывается через границу между двумя центрами.

Эта геометрия навязывает жёсткую классификацию:

Теорема 44.2 (cousin_mod_six, 🟢). Всякий младший член пары кузенов p > 3 лежит на плюс-стороне сетки: p % 6 = 1.

Почему это верно. Простое p > 3 не делится ни на 2, ни на 3, поэтому p % 6 есть 1 или 5. Случай p % 6 = 5 исключён арифметикой самой пары: тогда p + 4 ≡ 0 (mod 3), то есть p + 4 делилось бы на 3 — а оно по условию простое и больше трёх, противоречие. Остаётся p % 6 = 1. Кузены рождаются только на плюс-стороне — и конкретные центры это подтверждают (cousin_instances, 🟢): m = 1 даёт (7, 11), m = 2 — (13, 17), m = 3 — (19, 23).

Секси: односторонняя пара соседних центров

Зазор 6 (секси, p и p + 6) устроен иначе. Сдвиг на 6 не меняет вычета по модулю 6 (sexy_preserves_side, 🟢), поэтому секси-пара всегда сидит на одной стороне: либо минус-пара (6m − 1, 6m + 5) на минус-сторонах центров m и m + 1, либо плюс-пара (6m + 1, 6m + 7) на их плюс-сторонах. Секси-центр несёт пару хотя бы на одной стороне (sexy_instances, 🟢: минус-пары (5, 11), (11, 17); плюс-пара (7, 13)).

А когда две геометрии встречаются в одной точке, случается созвездие:

Теорема 44.3 (constellation_of_adjacent_twinCenters, 🟢 — даже без Classical.choice). Два соседних twin-центра m и m + 1 дают одновременно все три узора: кузенов на m и обе секси-пары на m.

Почему это верно. Если и m, и m + 1 — центры близнецов, то просты все четыре стороны: 6m − 1, 6m + 1, 6(m + 1) − 1 = 6m + 5, 6(m + 1) + 1 = 6m + 7. Из них собираются разом кузены (6m + 1, 6m + 5), минус-секси (6m − 1, 6m + 5) и плюс-секси (6m + 1, 6m + 7) — чистой перестановкой, без всякого выбора. При m = 1 это знаменитое созвездие 5, 7, 11, 13: кузены (7, 11), секси (5, 11) и (7, 13) сразу.

Здесь важно то, чего доказательство не делает: оно не строит соседних twin-центров, оно лишь распаковывает их, если они даны. Существование двух соседних twin-центров сколь угодно высоко — это гипотеза, и притом более сильная, чем близнецовая.

Манифестационный фронт — дважды

Теперь мы проводим обе ветви через ту же архитектуру, что Мерсенна в 43: опровержение обязано предъявить вечный двигатель. Отклонение здесь — не объект-данные (как off-critical нуль у Римана), а Π-свидетель отсутствия, зеркало мерсенновского: CousinAbsenceAbove P (все кузен-центры сидят не выше P) и SexyAbsenceAbove P (все секси-центры не выше P).

Плумбинг связывает их с целью точно — неограниченность центров эквивалентна отсутствию свидетелей отсутствия (cousinCentersUnbounded_iff_no_absence, sexyCentersUnbounded_iff_no_absence, 🟢), — а домен свидетеля локализован снизу:

Теорема 44.4 (cousinAbsenceBound_ge_37, sexyAbsenceBound_ge_17, 🟢). Всякая граница отсутствия кузенов не меньше 37; всякая граница отсутствия секси не меньше 17.

Почему это верно. Кузен-центр m = 37 зелёно существует — пара (223, 227) из простых; никакой свидетель не отсечёт его снизу, значит его граница не ниже 37. У секси то же с центром m = 17: по минус-стороне это пара (101, 107). Дальше начинается тьма: предъявить свидетеля отсутствия значило бы решить открытый случай гипотезы Полиньяка для зазора 4 или 6.

Закон манифестации гейчен этим свидетелем (CousinManifestationLaw, SexyManifestationLaw; гейт, напомним, — честно названный недостающий вход), и гейт — несущая стена, как у Мерсенна: негейченная форма при P = 0 вместе с принятой границей дала бы поставку потоков — бесконечную допустимую семью, которой отклонение «расплачивается», — на разрешённом масштабе, а это противоречит зелёной невозможности (no_deviationFlowSupply_at_resolved_scale) — тот самый механизм, которым взрывались манифестационные кандидаты Янг–Миллса и Навье–Стокса.

Объект манифестации DeviationFlowSupply заимствован у римановского фронта целиком, вместе с его свидетелем содержательности; здесь он не передоказывается. Главные теоремы — обе зелёные, для каждой семьи:

Теорема 44.5 (cousinCentersUnbounded_of_noEngine_and_boundary_and_manifestation, и её секси-близнец, 🟢 — essence). Нет двигателей + принятая граница + закон манифестации ⟹ кузен-центры (соотв. секси-центры) неограничены.

Почему это верно. Зеркало мерсенновской и римановой essence-лемм, с тем же стандартом честности. Из конечности извлекается свидетель P; граница даёт разрешение ровно на масштабе M0 := P; закон поставляет бесконечную семью потоков — не ex falso, а как данные; из коллизии её членов собирается двигатель-свидетель (читаемая форма cousinRefutation_carries_engine / sexyRefutation_carries_engine, 🟢); и убивает построенный двигатель именно гипотеза «двигателей нет».

Через честные мосты ветви (cousinLowersInfinite_of_unbounded, sexyLowersInfinite_of_unbounded) та же тройка доводится до цели — бесконечности самих пар.

Вывод. Опровергнуть кузенов или секси там, где книги сведены (то есть где проекция разрешает коллизии на данном масштабе, см. словарь), — буквально построить вечный двигатель.

Почему здесь нет ни ковки, ни декрета

Трилемма — обязательная тройная проверка кандидата в границы (см. словарь) — четвёртого поля пройдена обеими семьями: свидетель непредъявим (V1), закон зелёно не решаем ни в какую сторону (V2), границу он не взрывает (V3). Значит, по машинному критерию — тому самому, что впустил риманову границу, — поля cousinBoundary и sexyBoundary допустимы. И всё же их нет. Две причины, и первая — новая для программы.

У Мерсенна V3 держался на тонком аргументе: цепь центров 4m + 1 есть, но не пилится — старший делитель 4 не прост и не сравним с ±1 по модулю 6. У кузенов и секси аргумент проще и глубже: цепи нет вовсе, а значит и пилить нечего.

Кузены и секси — это полноплотностный узор соседних центров (m, m + 1), а не выделенная подпоследовательность вроде мерсенновской 4m + 1, софи-жермена 2m или ферма 6m² − 4m + 1. Секции цепи в этом модуле нет по существу, не по забывчивости: кованого свидетеля (паттерн, которым взрывались Янг–Миллс и Навье–Стокс) в этих ветвях не существует за отсутствием самого субстрата ковки. Дверь для честного закона открыта настежь — и здесь возникает вторая причина.

Теорема 44.6 (cousinManifestationLaw_iff_unbounded_of_boundary, и её секси-близнец, 🟢 — главный аудит цены M7). При принятой границе закон манифестации эквивалентен неограниченности центров.

Декрет был бы ровно силы соответствующего случая Полиньяка — как у Римана и Мерсенна. И знак эвристики здесь положителен: Харди–Литтлвуд ожидает бесконечность каждого класса пар, как консенсус ждёт RH. То есть ставка была бы на ожидаемо-истинное — впервые с положительным знаком, в отличие от Мерсенна. Казалось бы, бери. Но мы не взяли — и вот отчего.

Во-первых, коваться нечему, а значит нечего и готовить: у Мерсенна декрет отслаивал редкую цепь, у кузенов же перед нами полная плотность соседних центров — субстрата для кухни нет.

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

Примечание. Секси-свидетель заслуживает отдельной оговорки. Гейт IsSexyCenter двусторонний (минус-пара или плюс-пара через Or), поэтому SexyAbsenceAbove P — свидетель сильнее каждой стороны порознь: он одновременно ограничивает и минус-, и плюс-пары.

Это не портит ни одну из теорем — но именно поэтому нижняя грань 17 берётся минус-стороной, тогда как плюс-сторона дала бы другой порог; свидетель обязан переживать оба.

Итог раздела. Поля не добавлены — намеренно. Законы живут определениями в зелёном фронте, вся строгая цепь доказана с границей-гипотезой, таинт карантина не сдвинут ни на одну декларацию, а вердикт зафиксирован §17-комментарием карантина: допустимо, но отложено — на сей раз не по знаку эвристики, а по цене для самого карантина. Ни одного свободного Prop-поля в модуле нет; каждая гипотеза именована арифметически.

Философское отступление: почему пары сопротивляются, а одиночки нет

Гипотеза де Полиньяка утверждает, что каждый чётный зазор встречается между простыми бесконечно часто. Прочтённая через сетку, она распадается на ясный геометрический вопрос: зазоры 2, 4 и 6 — это ровно три способа, которыми две простые могут сесть на соседние центры, — один центр (близнецы), соседние центры на разных сторонах (кузены), соседние центры на одной стороне (секси). Полиньяк для больших зазоров продолжает тот же счёт дальше по сетке.

И тут открывается то, что делает парные задачи упорными, а одиночные — решёнными. Стрелка трудности целит не в сами простые. Про распределение одиночек мы знаем очень много: Дирихле раздаёт простые по всем допустимым классам поровну, каждая сторона сетки бесконечна, и это доказано аналитикой L-рядов без всякой гипотезы.

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

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

Прогресс здесь измеряется не тем, сколько парного мы объявили доказанным, а тем, как чисто мы отделили доказанное от гипотетического — и как честно назвали цену, за которую гипотезу можно было бы, но не следует, купить.

Полиньяк за тем же горизонтом

У стены, о которую разбиваются внутренние решения (глава 56), есть и полиньяковский склон — модуль Engine/PolignacEpistemic.lean, целиком зелёный. «Решить случай 4 или 6 изнутри» на нашем языке значило бы самообосновать закон манифестации: связка InternalisedCousinGround (и её секси-зеркало InternalisedSexyGround) держит три поля разом — сам закон, свидетеля отсутствия центров не выше леджер-масштаба и сведённые книги на этом масштабе.

Ни одно поле не есть отрицание другого — это стиль P/NP, а не тавтологическая пара Коллатца (общее с P/NP именно стиль, не арность: его эталон двухполевой, наша связка трёхполевая); и, в отличие от P/NP, ни одно из трёх зелёно не обитаемо. А вместе тройка зелёно несовместима: no_internalisedCousinGround и no_internalisedSexyGround, откуда следует «узнать нельзя изнутри» — и здесь теорема, а не лозунг:

Теорема 44.7 (cousinCause_unknowable, sexyCause_unknowable, 🟢). При любом леджер-масштабе A, M0 внутреннее знание причины кузенов невозможно — ¬ InternalKnowledgeOfCousinCause A M0; и, зеркально, ¬ InternalKnowledgeOfSexyCause A M0. Это не утверждение о самих кузенах или секси: случаи 4 и 6 открыты, закон не декретирован.

Чем это оплачено — подлинной конструкцией, не ex falso. Теоремы internalisedCousinGround_builds_engine и internalisedSexyGround_builds_engine суть прямая композиция читаемых форм фронта (cousinRefutation_carries_engine, sexyRefutation_carries_engine): закон поставляет семью потоков, стабильная вселенная собирает из их коллизии двигатель-свидетель — и построенное гибнет об зелёную стену no_someConcreteEuclideanEngine, где lexRank строго падает.

Цена честности названа: конструкция условна на гейченный, не декретированный закон и на сведённые книги — оба поля порознь неизвестны. Это слабее безусловного коллатцевского маршрута и зелёного пижонхола P/NP, и мы этого не прячем.

Сводка — обе семьи одной теоремой: самообосноваться значит построить двигатель; построенное самоуничтожается; остаётся внешний декрет, и его цена уже подсчитана — при границе-гипотезе TheStrictLastStep00Obligation закон эквивалентен неограниченности центров.

Теорема 44.8 (polignac_no_internal_decision_without_engine, 🟢). Для каждой из двух семей и при любых A, M0 держится тройка: (1) InternalisedCousinGround A M0 → SomeConcreteEuclideanEngine (самообоснование строит двигатель); (2) InternalisedCousinGround A M0 → False (построенное самоуничтожается об lexRank-стену); (3) TheStrictLastStep00Obligation → (CousinManifestationLaw ↔ CousinCentersUnbounded) (внешняя дверь — ровно случай 4). Секси-конъюнкт зеркален с InternalisedSexyGround, SexyManifestationLaw, SexyCentersUnbounded.

Но здесь и отличие от соседей по горизонту: у Римана внешняя дверь взята, у Коллатца декрет пал, а у Полиньяка поля нет и не будет — cousinBoundary и sexyBoundary не декретированы по вердикту §17, потому что серийный декрет стёр бы единственность карантина, как мы разобрали выше. Итог собран без декрет-конъюнкта, не по падению декрета, а потому что он не был взят вовсе: изнутри — двигатель, снаружи — недекретированный закон ровно гипотезной силы.

Теорема 44.9 (polignac_locked_behind_engine_status, 🟢). Для каждой из двух семей и при любых A, M0 держится четвёрка: (1) ¬ InternalKnowledgeOfCousinCause A M0 — внутреннее знание невозможно (Теорема 44.7); (2) ∀ P, CousinAbsenceAbove P → 37 ≤ P — всякий свидетель отсутствия не ниже 37 (Теорема 44.4); (3) TheStrictLastStep00Obligation → (CousinManifestationLaw ↔ CousinCentersUnbounded) — цена недекретированного поля (Теорема 44.6); (4) CousinCentersUnbounded → CousinLowers.Infinite — неограниченность достигла бы цели программы. Секси-конъюнкт зеркален (порог 17). Декрет-конъюнкта нет: поля cousinBoundary/sexyBoundary не существует.

Примечание (что мы не утверждаем). Это не решение случаев 4 и 6 гипотезы Полиньяка — оба остаются открытыми 🔴, и теоремы этой секции их статуса не двигают. Это и не Гёдель: ни независимости, ни неподвижной точки — самоуничтожение об lexRank-стену, и вся эпистемика модель-внутренняя. Условности названы: двигательная конструкция условна на закон и сведённые книги, граница фигурирует только гипотезой в конъюнктах; карантин модулем не импортируется, таинт репозитория не меняется.

Ось ± ортогональна времени

У хребта честности есть ещё один структурный факт, и он зелёный. Две стороны центра — будущие члены пары 6m ± 1 — переставляются флипом сторон mirrorSide, инволюцией (mirrorSide_involutive). И собственное время этого флипа не видит вовсе.

Теорема 44.10 (lexRank_side_invariant, 🟢). lexRank инвариантен под флипом сторон: lexRank (defect n q (mirrorSide s)) = lexRank (defect n q s). Оба члена пары стоят на ОДНОМ собственном времени; различаются лишь по ортогональной оси ±.

Почему это верно. lexRank = 3·centerOf + phase, и centerOf, и phase отбрасывают аргумент Side у дефекта — флип не меняет ничего из того, что читают часы. Это точное дополнение стрелы времени (Теорема 49.1, timeArrow_step): спуск идёт по оси времени, флип ± — по оси, ей ортогональной.

Теорема 44.11 (signedSideValue_reflection_sum, 🟢). Пара — отражение вокруг 6m: в ℤ signedSideValue plus z + signedSideValue minus z = 12z точно; ℕ-форма sideValue plus n + sideValue minus n = 12n держится при n ≥ 1 (sideValue_reflection_sum).

Почему это верно. (6z + 1) + (6z − 1) = 12z по ring в ℤ. В ℕ тождество под гардом n ≥ 1: при n = 0 усечение 6·0 − 1 = 0 (могила нуля) его ломает, так что ℤ-форма — честная безусловная.

Итак, ось ± есть отражение вокруг значения центра, а время ей ортогонально: зафиксировав один член, мы ставим его напарника в тот же миг, не в обращённый. Физическое прочтение — пара как инволюция, похожая на зарядовое сопряжение, отличная от запрещённого обращения времени — огорожено в Коде, 50: это перевод, не теорема.

Место в общем ходе

Полиньяк встал в один ряд с Мерсенном и Риманом: у всех трёх опровержение предъявляет вечный двигатель при законе и сведённых книгах (🟢, условно на границу), и у всех трёх сама граница декрета осталась — или осталась бы — гипотезой.

Но правило серии уточнилось ещё раз. У Римана границу мы брали — ставка на RH, в которую верит консенсус, — но позже отсоединили её (Option A). У Мерсенна отложили по знаку эвристики. У Полиньяка знак эвристики положителен, как у Римана, — и всё равно отложили, по новой причине: где нет цепи, там нечего готовить, а серийный декрет стёр бы единственность, в которой весь смысл карантина. Честная граница требует теперь не только зелёно-непредъявимого свидетеля и ставки, за которую не стыдно, но и того, чтобы её принятие не обесценило само исключение.

twin_prime_conjecture остаётся sorry; гипотеза Полиньяка для зазоров 4 и 6 — открытой; таинт карантина — прежним. Одиночки зелёные, пары — гипотезы, и ни одна открытая задача не объявлена решённой.

---

← 43. Мерсенн через первопричину · Оглавление · 45. Софи Жермен →