Мерсенн через манифестацию: опровержение предъявляет двигатель — и граница, которую мы не взяли¶
← 42. Ходж · Оглавление · 44. Стороны и Полиньяк →
Lean-источник:
Engine/MersenneManifestationFront.lean— зелёная цепь, вся 🟢;Engine/CausalClosureAxiom.lean§16 — комментарий-вердикт (деклараций нет). Проза-контекст: 34. Ветка Мерсенна, 38. Риман через первопричину. Обозначения статуса: 🟢 — доказано при стандартных аксиомах; 🟡 — условно на аксиомуstep00FirstCause; 🔴 — открытый вход.
Где мы¶
Глава 34 оставила ветку Мерсенна намеренно скромной: честный мост «Мерсенн-близнецы ⟹ близнецы», запрет обратного соблазна и вскрытая вакуумность №3. Но после того как Риман прошёл через манифестационную архитектуру (38), а Коллатц — через хвост-двигатель, у Мерсенна остался незакрытым тот же вопрос, что и у них: что стоило бы опровержение? Если Мерсенн-близнецов конечно много — что именно предъявляет миру эта конечность?
Ответ этой главы: при законе манифестации и сведённых книгах — вечный двигатель, как объект. Напомним язык: закон манифестации — принцип «отклонение обязано проявиться следом-поставкой», а «книги сведены» — леджер разрешает коллизии на данном масштабе (см. словарь). А её вторая, не менее важная новость — про честность: четвёртая граница декрета здесь допустима по всем машинным критериям, и мы её сознательно не взяли. Впервые за всю программу.
Свидетель-отсутствие: отклонение без объекта¶
У Римана отклонение было объектом-данными — конкретным нулём вне прямой. У Мерсенна опровержение устроено иначе: это конечность, утверждение о том, что выше некоторого порога близнецов среди чисел Мерсенна больше нет. Свидетель здесь — не точка, а граница:
Определение 43.1 (MersenneTwinAbsenceAbove P). Отсутствие Мерсенн-близнецов выше P: каждая
пара (2^p − 3, 2^p − 1) из простых сидит нижней стороной не выше P. Формально:
$\(\mathrm{MersenneTwinAbsenceAbove}(P)\ :\equiv\ \forall p\in\mathbb{N},\ (2^p-3)\text{ простое}\ \wedge\ (2^p-1)\text{ простое}\ \Rightarrow\ 2^p-3\le P. \tag{43.1}\)$
Это Π-утверждение — зеркало близнецовой границы TwinBoundAbove, и плумбинг связывает его с целью
ветки точно: неограниченность Мерсенн-близнецов эквивалентна отсутствию таких свидетелей.
Теорема 43.2 (mersenneTwinCentersUnbounded_iff_no_absence, 🟢). Центры чисел Мерсенна
неограничены тогда и только тогда, когда ни при каком P не существует свидетеля отсутствия:
$\(\mathrm{MersenneTwinCentersUnbounded}\ \iff\ \forall P\in\mathbb{N},\ \neg\,\mathrm{MersenneTwinAbsenceAbove}(P). \tag{43.2}\)$
Про домен свидетеля мы знаем и нижнюю грань:
Теорема 43.3 (mersenneAbsenceBound_ge_29, 🟢). Всякая граница отсутствия не меньше 29:
$\(\mathrm{MersenneTwinAbsenceAbove}(P)\ \Rightarrow\ 29\le P. \tag{43.3}\)$
Почему это верно. Пара (29, 31) при p = 5 зелёно существует — оба числа просты, и никакой
свидетель не может отсечь её снизу. Дальше 29, впрочем, начинается настоящая тьма: предъявить
свидетеля отсутствия значило бы решить открытую задачу о хвосте Мерсенн-близнецов.
Почему здесь нет ковки: цепь, которая не пилится¶
Прежде чем декретировать закон, программа обязана проверить трилемму — обязательную тройную
проверку кандидата в границы (см. словарь) — и решающий её пункт мы
помним по Янг–Миллсу и Навье–Стоксу: манифестационные кандидаты взрывались там, где свидетеля
можно было выковать — машинно построить контрпример к универсальной форме закона (лестница
{2⁻ⁿ}, профильный каскад). Есть ли кованый свидетель у Мерсенна?
Центры чисел Мерсенна образуют явную цепь — базы-4 репьюниты 0, 1, 5, 21, 85, … с рекуррентой
m → 4m + 1; она строго монотонна и инъективна. Внешне это
близнец пятиадической цепи c → 5c + 1, которая в 24 выковала бесконечную семью генеалогий и
опровергла малую ветвь узла.
Теорема 43.4 (mersenneCenterChain_strictMono, 🟢). Функция центра mersenneCenter
строго монотонна (в частности, инъективна):
$\(\forall k\in\mathbb{N},\ \mathrm{mersenneCenter}(k)<\mathrm{mersenneCenter}(k+1). \tag{43.4}\)$
Но сходство обманчиво, и разница — арифметическая:
Теорема 43.5 (isEmpty_properCenterPeel_five_one, 🟢 — даже без Classical.choice). Первый шаг
базы-4 цепи, 5 → 1, не несёт собственного пила ни при каком масштабе:
$\(\forall A\in\mathbb{N},\ \mathrm{ProperCenterPeel}(A,5,1)\ \text{пуст}. \tag{43.5}\)$
Почему это верно. У пятиадической цепи есть тождество 6(5x+1) − 1 = 5(6x+1) с простым
постоянным делителем 5 — каждый шаг честно пилится. У цепи 4m+1 такого тождества нет и быть не
может: старшие коэффициенты навязывают делитель 4, а он не прост и не сравним с ±1 по модулю 6 —
стороны на стороны не отображаются. И уже на первом шаге всё видно голыми руками: стороны центра 5 —
это 29 и 31, оба просты, а стороны центра 1 — лишь 5 и 7; никакой факторизации не существует.
Следствие принципиально: Мерсенн-цепь не строит безусловной поставки потоков — кованого свидетеля в этой ветви не существует. Точь-в-точь ситуация Римана (нуль не предъявишь, не опровергнув RH), и точная противоположность Янг–Миллсу и Навье–Стоксу. Дверь для честного закона открыта.
Закон манифестации — гейченный свидетелем¶
Определение 43.6 (MersenneManifestationLaw). Для каждого порога P со свидетелем отсутствия:
на каждом леджер-масштабе не ниже P, всюду где проекция сводит книги, отсутствие проявляется
неоплатимой бесконечной поставкой потоков (DeviationFlowSupply — тот же объект, что у Римана):
$\(\mathrm{MersenneManifestationLaw}\ :\equiv\ \forall P,\ \mathrm{MersenneTwinAbsenceAbove}(P)\Rightarrow\ \forall A, M_0,\ P\le M_0\Rightarrow\ \forall\,\mathrm{proj},\ \mathrm{Resolves}(\mathrm{proj})\Rightarrow\ \mathrm{DeviationFlowSupply}(A,M_0). \tag{43.6}\)$
Гейт свидетелем — не украшение, а несущая стена. Негейченная форма «∀ P, отсутствие манифестирует»
при P = 0 вместе с принятой границей дала бы поставку на разрешённом масштабе — а это противоречит
зелёной невозможности (та же no_deviationFlowSupply_at_resolved_scale, что убивала риманову
поставку). Ровно так провалились манифестационные кандидаты Янг–Миллса и Навье–Стокса. Гейт по
зелёно-непредъявимому свидетелю — то, что отличает честную форму от взрывной.
Опровержение предъявляет двигатель¶
Теперь главные теоремы — обе зелёные, обе с подлинным потреблением гипотез.
Теорема 43.7 (mersenneRefutation_carries_engine, 🟢 — читаемая форма). Свидетель отсутствия +
закон манифестации + сведённые книги на масштабе не ниже P предъявляют вечный двигатель — как
объект, ConcreteEuclideanEngineWitness, до всякого убийства:
$\(\mathrm{MersenneManifestationLaw}\ \wedge\ \mathrm{MersenneTwinAbsenceAbove}(P)\ \wedge\ P\le M_0\ \wedge\ \mathrm{Resolves}(\mathrm{proj})\ \Rightarrow\ \mathrm{ConcreteEuclideanEngineWitness}(A,M_0). \tag{43.7}\)$
Почему это верно. Разрешающая проекция даёт стабильную безэнергетическую вселенную; закон превращает отсутствие в бесконечную семью потоков; конечный ключ вынужден столкнуть двух её членов (пигеонхол); из коллизии собирается двигатель-свидетель. Опровергнуть Мерсенн-близнецов там, где книги сведены, — буквально построить вечный двигатель.
Теорема 43.8 (mersenneTwinsUnbounded_of_noEngine_and_boundary_and_manifestation, 🟢 — essence).
Нет двигателей + принятая граница + закон манифестации ⟹ Мерсенн-близнецы неограничены:
$\(\neg\,\mathrm{SomeConcreteEuclideanEngine}\ \wedge\ \mathrm{TheStrictLastStep00Obligation}\ \wedge\ \mathrm{MersenneManifestationLaw}\ \Rightarrow\ \mathrm{MersenneTwinCentersUnbounded}. \tag{43.8}\)$
Зеркало близнецовой и римановой essence-лемм, с тем же стандартом честности: из конечности
извлекается свидетель P; граница даёт разрешение ровно на масштабе P; закон поставляет семью —
не ex falso, а как данные; и убивает построенный двигатель именно гипотеза «двигателей нет». Через
честный мост 34 эта же тройка доводится и до близнецов:
Теорема 43.9 (twinLowersInfinite_of_noEngine_boundary_and_mersenneManifestation, 🟢). Та же
тройка гипотез влечёт бесконечность нижних сторон близнецов:
$\(\neg\,\mathrm{SomeConcreteEuclideanEngine}\ \wedge\ \mathrm{TheStrictLastStep00Obligation}\ \wedge\ \mathrm{MersenneManifestationLaw}\ \Rightarrow\ \mathrm{TwinLowers.Infinite}. \tag{43.9}\)$
Цена — и почему мы её не заплатили¶
Трилемма пройдена: свидетель непредъявим, закон не разрешим зелёно ни в какую сторону, ковки нет.
По машинному критерию — тому самому, что впустил риманову границу и отверг кандидатов Янг–Миллса,
Навье–Стокса, P/NP и Ходжа, — четвёртое поле mersenneBoundary допустимо. И вот его цена:
Теорема 43.10 (mersenneManifestationLaw_iff_unbounded_of_boundary, 🟢 — главный аудит M7). При
принятой границе закон манифестации эквивалентен неограниченности Мерсенн-близнецов:
$\(\mathrm{TheStrictLastStep00Obligation}\ \Rightarrow\ \bigl(\mathrm{MersenneManifestationLaw}\ \iff\ \mathrm{MersenneTwinCentersUnbounded}\bigr). \tag{43.10}\)$
Декрет был бы ровно Мерсенн-близнецовой силы — не слабее и не сильнее, как у Римана. Но здесь впервые за программу возникает то, чего не было ни в одной предыдущей трилемме: знак эвристики инвертирован. Принять риманову границу значило поставить на RH — утверждение, в которое верит консенсус.
Принять мерсенновскую значило бы поставить на неограниченность Мерсенн-близнецов — а
эвристика глядит в другую сторону: ожидаемое число пар (2^p−3, 2^p−1) из простых даётся сходящейся
суммой, известны лишь p = 3 и p = 5, и вдобавок при всяком p ≡ 3 (mod 4) число 2^p − 3
делится на 5 — половина экспонент выбывает сразу.
Вывод. Ставка была бы не на ожидаемо-истинное, а против ожиданий; и непротиворечивость всего карантина легла бы на неё.
Мы решили иначе: поле не добавлено — намеренно. Закон живёт определением в зелёном фронте (как жил закон Римана до §10), вся строгая цепь доказана с границей-гипотезой, таинт карантина не изменился, а вердикт зафиксирован комментарием §16: допустимо, но отложено по знаку эвристики. Машинный критерий говорит «можно»; честность говорит «можно — не значит нужно».
Примечание. Отметим и то, чего эта глава не чинит: вакуумность №3 из 34 остаётся вскрытой — форвард-серия как была необитаемой, так и осталась, и новый фронт не разделяет с ней ни одного определения. Свидетель здесь — именованное арифметическое утверждение об отсутствии, поставка — тот же строгий объект, что у Римана, и ни одного свободного Prop-поля в модуле нет.
Философское отступление: ставка, которую видно¶
Глава 34 закончилась теоремой Евклида–Эйлера: простые Мерсенна и чётные совершенные числа — один объект, и вопрос об их бесконечности стоит открытым со времён «Начал». Эта глава добавляет к той нити последний виток — о природе ставок в математике.
Аксиома — это всегда ставка. Приняв риманову границу, мы поставили на RH — так физик закладывает в теорию симметрию, в которую верит всё сообщество. Мерсенновская граница прошла все те же проверки честности — свидетеля не предъявить, закон не разрешить, ковки нет, — и всё же мы её не взяли, потому что критерии честности отвечают на вопрос «можно ли поставить», а не «стоит ли».
Ставить против собственной эвристики — право игрока; но программа, чья витрина — честность, обязана как минимум показать игроку таблицу коэффициентов. Мы её показали: M7 говорит, чему равна ставка, эвристика говорит, куда дует ветер, и §16 фиксирует решение не играть.
В этом, пожалуй, самый зрелый урок всей причинной линии. Сила аксиоматического метода не в том, что аксиомой можно закрыть что угодно, — а в том, что видно, что именно закрывается и почём. Первый раз за программу машинно-допустимая граница осталась не взятой — и этот отказ говорит о честности архитектуры больше, чем любое из принятых полей. Совершенные числа подождут: они ждали Евклида две тысячи лет — подождут и решения, сделанного с открытыми глазами.
Место в общем ходе¶
Теперь у всех крупных ветвей есть ответ на вопрос «что стоило бы опровержение»: близнецы и Риман —
границы декрета (🟡); Коллатц — декрет взят и снят (закон каната машинно опровергнут, глава 56),
хвост-двигатель от минимума орбиты остаётся 🟢; Мерсенн —
манифестационный двигатель при законе и книгах (🟢, условно), с допустимой, но отложенной границей.
Правило серии уточнилось: честная граница требует зелёно-непредъявимого свидетеля — и ставки, за
которую не стыдно. twin_prime_conjecture остаётся sorry; таинт карантина — прежние 16
деклараций; ни одна открытая задача не объявлена решённой.