Софи Жермен: удвоение центра и жемчужина серии

← 44. Стороны и Полиньяк · Оглавление · 46. Гольдбах и Лежандр →

Lean-источник: Engine/SophieGermainBranch.lean — ветвь с классической теоремой, вся 🟢; Engine/SophieGermainManifestationFront.lean — зелёный манифестационный фронт (зеркало Мерсенна) с рестрикт-секцией 3 (mod 4). Обозначения статуса: 🟢 — доказано при стандартных аксиомах; 🟡 — условно на аксиому step00FirstCause; 🔴 — открытый вход.

Где мы

Весь арифметический зверинец этой части — Мерсенн, пятиадика, Коллатц — держался на одном приёме: у всякой ветви есть цепь центров с рекуррентой m → am + b, она строго растёт, и вопрос лишь в том, пилится ли она (строит кованого свидетеля — машинный контрпример, см. словарь) или нет. Мерсеннова 4m+1 не пилилась, пятиадическая 5m+1 пилилась, и на этом контрасте держалась вся честность манифестационной архитектуры.

Но во всех этих ветвях сами по себе арифметические факты были скромны — вакуумные серии, тождества на пол-строки, рост на omega. Ни одной содержательной классической теоремы среди них не было.

Ветвь Софи Жермен отличается. Она приносит ту же цепь центров — но с ней приходит и единственная за всё добавление подлинно нетривиальная классическая теорема: простое Софи Жермен убивает простоту Мерсенна. Это результат Эйлера и Лагранжа, и здесь он не пересказан, а доказан машиной до последнего шага.

Вокруг этой жемчужины и построена глава: сперва геометрия пары в языке программы, затем сама теорема, а затем — то, ради чего она вообще нужна общему ходу. Она оказывается формальным осколком той самой эвристики, которой карантин §16 (глава 43) обосновал отказ взять границу Мерсенна.

Геометрия пары: почему SG-простые живут только на минус-стороне

Пара Софи Жермен — это (p, 2p+1), оба простые (IsSophieGermain). В координатах программы, где каждое простое > 3 сидит стороной 6m ± 1, у этой пары обнаруживается жёсткая односторонность.

Теорема 45.1 (not_sophieGermain_of_plusSide, 🟢). Если p = 6m + 1 при m ≥ 1, то 2p + 1 не простое.

Почему это верно. Считаем прямо: 2(6m+1) + 1 = 12m + 3 = 3(4m+1), и тройка делит спутника нацело. При m ≥ 1 спутник больше трёх — значит, составной. Плюс-сторона отпадает целиком: SG-простое p > 3 не может иметь вид 6m+1.

Остаётся минус-сторона, и она не просто уцелевает — она навязывает вычет:

Теорема 45.2 (sophieGermain_minusSide, 🟢). SG-простое p > 3 обязано быть p ≡ 5 (mod 6).

Почему это верно. Простое p > 3 не делится ни на 2, ни на 3, так что p % 6 — либо 1, либо 5. Первое только что исключено плюс-стороной (Теорема 45.1). Значит, p ≡ 5 (mod 6), то есть p = 6m − 1.

А теперь — суть, ради которой ветвь вообще попала в эту серию. На минус-стороне SG-отображение в координатах центров есть чистое удвоение:

Теорема 45.3 (sg_center_doubling, 🟢). 2(6m − 1) + 1 = 6(2m) − 1.

Почему это верно. Раскрываем скобки — тождество проверяется в уме. Но смысл его не в арифметике, а в родословной: спутник 2p+1 пары с центром m сам сидит на минус-стороне, и его центр — ровно 2m. SG-отображение центров есть m → 2m. Это третий брат тех самых цепей: мерсеннова 4m+1, пятиадическая 5m+1, и вот теперь SG-удвоение 2m. Первые SG-простые выкладывают эту цепочку наглядно — 5, 11, 29, 89 (sg_instances): центры 1, 2, 5, 15, спутники 11, 23, 59, 179, каждый следующий член семьи вырастает из удвоенного центра предыдущего класса.

Примечание. Критерий isSGCenter_iff замыкает картину симметрично: m — SG-центр (оба числа 6m−1 и 6(2m)−1 просты) в точности тогда, когда 6m−1 — SG-простое. Язык центров и язык пар здесь — одно и то же, переписанное через удвоение.

Жемчужина: простое Софи Жермен гасит Мерсенна

Теперь — единственная содержательная классическая теорема всего добавления, доказанная машиной целиком.

Теорема 45.4 (sophieGermain_divides_mersenne, 🟢). Если p простое, p ≡ 3 (mod 4), p > 3, и q = 2p + 1 простое, то q ∣ M_p и число Мерсенна M_p = 2^p − 1 — составное.

Почему это верно. Маршрут — классический Эйлер–Лагранж, и он держится на одном сцеплении вычетов. Раз p ≡ 3 (mod 4), то q = 2p + 1 ≡ 7 (mod 8). Но q ≡ ±1 (mod 8) — ровно условие, при котором 2 есть квадратичный вычет по модулю q (ZMod.exists_sq_eq_two_iff); семёрка попадает в допустимый класс.

Значит, 2 — квадрат в ZMod q, и по критерию Эйлера 2^((q−1)/2) ≡ 1 (mod q). А показатель здесь — ровно p, потому что (q−1)/2 = (2p)/2 = p. Итого 2^p ≡ 1 (mod q), то есть q ∣ 2^p − 1 = M_p. Остаётся убедиться, что делитель собственный: при p ≥ 4 имеем 2p + 1 < 2^p − 1 (two_mul_add_one_lt_mersenne — простая индукция по показателю), так что 1 < q < M_p, и M_p не может быть простым.

Демонстрация не абстрактна:

Теорема 45.5 (mersenne_composite_examples, 🟢). 23 ∣ M_11 = 2047, и M_11 составное.

Здесь p = 11 ≡ 3 (mod 4), спутник q = 23 прост, и действительно 2047 = 23 · 89 — распадается ровно на предсказанный делитель. Теорема не просто отрицает простоту; она указывает пальцем на множитель.

Примечание. Оговорка про p = 3 — не педантизм, а честный край, который формализация уважает. Условие p > 3 не декоративно: при p = 3 спутник q = 7, но 7 = M_3 есть само число Мерсенна, и оно простое. Делитель совпал бы с делимым — «собственного» распада нет. Ровно на этом единственном показателе маршрут Эйлера даёт делитель, но не даёт составности; и hgt : 3 < p в сигнатуре теоремы — это машинная запись именно данного исключения. Программа не заметает край под ковёр: она его именует.

Две ставки, глядящие друг на друга

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

Взять её значило бы поставить на неограниченность Мерсенн-близнецов, тогда как эвристика глядит в другую сторону. И один из доводов той эвристики против простоты чисел Мерсенна — ровно этот: простые Софи Жермен поштучно гасят кандидатов.

Манифестационный фронт ветви делает этот довод формальным. Он — зеркало Мерсенн-фронта: тот же Π-свидетель отсутствия (SGAbsenceAbove P), та же цепь удвоения, которая не пилится (isEmpty_properCenterPeel_two_one, 🟢 — коэффициент 2, хоть и прост, не сравним с ±1 по модулю 6 и не делит нечётные стороны 6n ∓ 1; уже первый шаг 2 → 1 пуст), тот же гейченный — то есть запертый за честно названным входом — свидетелем закон, та же essence «нет двигателей + граница + закон ⟹ пары Софи Жермен неограничены».

Всё это — точная копия архитектуры Римана и Мерсенна, и спотлайт на ней задерживать не стоит.

Но у этого фронта есть секция, которой нет ни у одного другого. Он умеет работать не по всему семейству SG-простых, а по подсемейству p ≡ 3 (mod 4) — ровно тому, которое жемчужина превращает в убийц простоты Мерсенна. И тогда его вывод меняет знак:

Теорема 45.6 (mersenneComposites_unbounded_of_noEngine_boundary_and_sgManifestation, 🟢, условно). Нет двигателей + принятая граница + рестрикт-закон 3 (mod 4) ⟹ простых p с составным M_p неограниченно много.

Почему это верно. Essence рестрикт-фронта даёт неограниченность SG-простых класса 3 mod 4 (SGThreeMod4Unbounded), а жемчужина ветви — через mersenneComposites_unbounded_of_sg — превращает каждое такое p в показатель с составным M_p. Вот где сходятся две линии.

Вывод. Мерсенн-фронт отказался ставить на простую сторону величины M_p. Этот фронт своим выводом изготовляет составную сторону той же самой величины. Одна ставка отклонена по знаку эвристики; вторая — оборотная ей — собирается зелёно, условно на ту же гипотезу неограниченности. Две ставки на M_p, глядящие друг на друга через одно число.

Отметим честно и границы этого построения. Рестрикт-гейт SGThreeMod4AbsenceAbove слабее полносемейного, потому рестрикт-закон открывается более слабым свидетелем, а полносемейный закон не даёт его напрямую. Импликация между двумя законами здесь не утверждается и не потребляется: королларий кормится только рестрикт-законом.

И сама безусловная бесконечность составных Мерсеннов давно известна литературе другими методами; здесь честно зафиксирован лишь SG-маршрут к ней.

Как и у соседей по серии, поле границы не добавлено — но по причине, обратной мерсенновской. Знак эвристики Софи Жермен положителен (Харди–Литтлвуд обещает ~ 2C₂ · x / ln² x пар), так что это была бы ставка на ожидаемо-истинное, как у Римана. И всё же вердикт §17 гласит, что манифестационные поля за пределами Римана программа не множит.

Философское отступление

Софи Жермен вела свою переписку с Гауссом под мужским именем — «месье Леблан», — потому что академия её века не пускала женщин к математике. Когда Гаусс узнал правду, он написал, что удивление сменяется восхищением тем сильнее, чем труднее был путь.

Простые, носящие её имя, она ввела в осаде Великой теоремы Ферма: для таких p первый случай теоремы поддавался. Спустя два столетия те же числа держат безопасность цифровой связи. «Безопасное простое» q = 2p + 1 со своим SG-простым p даёт группу, в которой дискретный логарифм не разваливается на мелкие множители, и на этом стоит половина криптографии Диффи–Хеллмана.

Число, рождённое в осаде одной старой задачи, охраняет тайны, которых её автор вообразить не могла.

Но глубже здесь другое, и оно про саму сетку программы. Гипотеза Софи Жермен — бесконечность её простых — открыта, как открыта гипотеза о простоте бесконечно многих чисел Мерсенна. Это две разные нерешённые задачи, из разных углов теории чисел.

И вот жемчужина этой главы — вместе с рестрикт-фронтом — строит между ними условный мост: если SG-простых класса 3 mod 4 бесконечно много, то составных Мерсеннов бесконечно много. Мост односторонний, честный, ничего не решающий сам по себе; но он делает видимым родство, которого в обычной записи не разглядеть.

Открытая задача о Софи Жермен оказывается привязана к составной стороне открытой задачи о Мерсенне — и привязана именно тем классическим делением, что Эйлер нашёл два с половиной века назад. Сетка центров не доказывает новых теорем; она проявляет скрытые арифметические родословные, как проявитель — латентное изображение.

И третий брат цепей стоит теперь в ряду на своём месте. Мерсеннова 4m+1, пятиадическая 5m+1, SG-удвоение 2m — три рекурренты, три семьи центров, из которых пилится лишь пятиадическая. Программа не выбирала эти цепи ради красоты симметрии; они выпали из ветвей независимо, каждая из своей задачи. То, что все три укладываются в один язык m → am + b и один вопрос о пиле, — не украшение, а свидетельство, что язык подобран под предмет, а не предмет подогнан под язык.

Софи Жермен за тем же горизонтом

У стены, о которую разбиваются внутренние решения (глава 56), есть и склон Софи Жермен — модуль Engine/SophieGermainEpistemic.lean, целиком зелёный. «Решить гипотезу изнутри» значило бы самообосновать закон манифестации: связка InternalisedSGGround держит три поля разом — сам закон, свидетеля отсутствия пар не выше собственного горизонта (тот же SGAbsenceAbove) и сведённые книги на этом масштабе — то есть бухгалтерию без свободной энергии (см. словарь).

Ни одно из трёх зелёно не обитаемо; но вместе они предъявляют вечный двигатель — подлинной конструкцией, не ex falso, то есть не выводом «из лжи что угодно» (internalisedSGGround_builds_engine, внутри которой работает sgRefutation_carries_engine фронта), — и построенное гибнет об lexRank-стену no_someConcreteEuclideanEngine.

Отсюда — закон манифестации не самообосновать: «узнать нельзя изнутри» и для Софи Жермен теорема, а не лозунг.

Теорема 45.7 (no_internalisedSGGround, sgCause_unknowable, 🟢). Ни на каком масштабе (A, M0) внутреннее самообоснование недостижимо: InternalisedSGGround(A, M0) → False, эквивалентно ¬ InternalKnowledgeOfSGCause(A, M0). (Утверждение не о самих SG-парах, а о цене внутреннего решения: собранная связка строит свидетель-двигатель SomeConcreteEuclideanEngine и гибнет об lexRank-стену no_someConcreteEuclideanEngine.)

Второй внутренний путь — опровергнуть — стоит того же. Сводка sg_no_internal_decision_without_engine (🟢) раскладывает развилку: опровержение изнутри — свидетель отсутствия при законе на сведённых книгах — строит двигатель; самообоснование самоуничтожается; решала бы лишь внешняя граница, но её §17 не выдал, и в конъюнкты она входит только гипотезой.

Оговорку делаем сразу: «опровержение = двигатель» у Софи Жермен условно на закон — слабее безусловного коллатцевского хвоста, и мы этого не прячем.

Итог собран в sg_locked_behind_engine_status (🟢) — как у Полиньяка, без декрет-конъюнкта; а рестрикт-зеркало 3 (mod 4) повторяет ту же эпистемику для подсемейства жемчужины (InternalisedSGThreeMod4Ground, sgThreeMod4Cause_unknowable, 🟢) и в сводке sgThreeMod4_locked_behind_engine_status несёт анти-Мерсенн-конъюнкт — дважды условный, на границу-гипотезу и на рестрикт-закон.

А жемчужина за этот горизонт не заходит. 23 ∣ M_11 и весь маршрут Эйлера–Лагранжа (sophieGermain_divides_mersenne, mersenne_composite_examples, 🟢) доказаны безусловно — без закона, без границы, без эпистемических связок. Горизонт запирает внутренние решения открытого вопроса; классической теореме, решённой здесь машиной до последнего шага, он не указ.

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

Теорема 45.8 (unknowable_or_sg_unbounded, 🟢). На любом масштабе (A, M0) верно (¬ InternalKnowledgeOfSGCause(A, M0)) ∨ SophieGermainUnbounded. В формулировке нет ex falso; левый дизъюнкт — теорема (Теорема 45.7), правый — открытая гипотеза, здесь не утверждаемая.

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

Впервые за всё добавление в серию вошла содержательная классическая теорема — Эйлер–Лагранж, sophieGermain_divides_mersenne, — и вошла зелёной и безусловной: она доказана целиком, без гипотез и без границ, вместе с честным исключением показателя p = 3.

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

Сама эта гипотеза — бесконечность её простых — как была открытой, так и осталась; ни она, ни задача Мерсенна не объявлены решёнными. Жемчужина зелена; вопрос, которому она служит, по-прежнему ждёт. Ровно так, как и должно быть у программы, чья витрина — честность.

---

← 44. Стороны и Полиньяк · Оглавление · 46. Гольдбах и Лежандр →