Числа Ферма: вторая ставка против ожиданий — граница, машинно допустимая и вновь не взятая

← 47. Совершенные числа · Оглавление · 49. Геометрия пути →

Lean-источник: Engine/FermatBranch.lean — честный мост Ферма ↔ близнецы, вся 🟢; Engine/FermatManifestationFront.lean — зелёный фронт манифестации, вся 🟢; Engine/FermatMersenneEpistemic.lean — эпистемический комплемент обеих ветвей, вся 🟢; Engine/CausalClosureAxiom.lean §16–§17 — комментарий-вердикт (деклараций нет). Проза-контекст: 34. Ветка Мерсенна, 43. Мерсенн через первопричину. Обозначения статуса: 🟢 — доказано при стандартных аксиомах; 🟡 — условно на аксиому step00FirstCause; 🔴 — открытый вход.

Где мы

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

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

Эта глава — зеркало той. Числа Ферма \(F_k = 2^{2^k} + 1\) проходят ту же архитектуру, дают тот же зелёный фронт, ту же читаемую теорему «опровержение предъявляет двигатель» — и упираются в тот же вердикт, только знак эвристики здесь ещё резче.

У Мерсенна сумма по twin-парам всего лишь сходилась. У Ферма известный хвост составных чисел огромен, простыми известны лишь пять первых, и консенсус ждёт, что новых простых Ферма нет вовсе. Так вторая ставка против ожиданий выходит тяжелее первой — и мы её снова не делаем.

Впервые за программу отказ по знаку эвристики становится правилом, а не единичным решением.

Минус-сторона: зеркало Мерсенна на другой стороне сетки

Мерсенн жил на плюс-стороне: \(2^p - 1 = 6m + 1\) (34). Ферма живёт ровно напротив.

Теорема 48.1 (six_mul_fermatCenter, 🟢). При \(k \ge 1\) деление в центре \(c_k = (F_k + 1)/6\) точное: \(\;6\,c_k = F_k + 1\), то есть \(F_k = 6\,c_k - 1\) — число Ферма есть минус-сторона центра, младший член пары.

Почему это верно. При \(k \ge 1\) показатель \(2^k\) чётен, и \(2^{2^k} = 4^{2^{k-1}} \equiv 1 \pmod 3\); значит \(F_k \equiv 2 \pmod 3\), а по нечётности \(F_k \equiv 1 \pmod 2\) — вместе это даёт \(F_k \equiv 5 \pmod 6\) (fermatNumber_mod_six). Пятёрка по модулю шесть — это ровно минус-сторона \(6m - 1\), зеркальная плюс-стороне Мерсенна.

Случай \(k = 0\) исключён сознательно: \(F_0 = 3\) не лежит на сетке \(6m \pm 1\) вовсе, и мост начинается с \(k = 1\). Twin-критерий тогда дословно зеркалит мерсенновский: центр \(c_k\) — twin-центр \(\iff\) оба \(F_k\) и \(F_k + 2\) просты (isTwinCenter_fermatCenter_iff 🟢).

И единственная честная стрелка между темами, как у Мерсенна, направлена в обратную сторону — Ферма-близнецы \(\Rightarrow\) близнецы (twinLowersInfinite_of_fermatTwins 🟢): подпоследовательность близнецов — всё ещё близнецы, и ни слова о простых Ферма из гипотезы близнецов не следует.

Цепь, которая не пилится — и на сей раз квадратично

У Мерсенна центры росли линейно, база-4 репьюниты \(m \to 4m + 1\); у пятиадической цепи из 24 — \(c \to 5c + 1\). Ферма ломает и эту линейность.

Теорема 48.2 (fermatCenter_chain, 🟢). Цепь центров квадратична: \(c_{k+1} = 6\,c_k^2 - 4\,c_k + 1\), записано без вычитания как \(c_{k+1} + 4\,c_k = 6\,c_k^2 + 1\).

Почему это верно. Рекуррента mathlib \(F_{k+1} = (F_k - 1)^2 + 1\), переведённая через \(6c = F + 1\), даёт именно нелинейный закон — и в этом вся соль.

У пятиадической цепи было тождество \(6(5x+1) - 1 = 5(6x+1)\) с простым постоянным делителем 5, и потому она ковала потоки при малых \(A\). У линейной \(4m+1\) Мерсенна такого делителя уже не было. У квадратичной \(6c^2 - 4c + 1\) его нет и быть не может: нелинейный старший член не оставляет постоянного простого множителя, стороны на стороны не отображаются.

Ковать нечего — цепь умеет расти (fermatCenter_strictMono_from_one 🟢), пилить не умеет.

Теорема 48.3 (isEmpty_properCenterPeel_three_one, 🟢). Шаг цепи \(3 \to 1\) не несёт собственного пила ни при каком масштабе.

Почему это верно. Всё видно голыми руками уже на первом шаге, как и у Мерсенна, только числа другие: стороны центра 3 — это 17 и 19, оба просты; стороны цели, центра 1, — лишь 5 и 7. Никакой факторизации из первых во вторые не существует, ни при каком \(A\).

Следствие то же, что и у Римана, Мерсенна, Софи Жермен: кованого свидетеля в ветви Ферма не существует — машинно построенного контрпримера к закону, «ковки» (см. словарь), — точная противоположность Янг–Миллсу (cookedLadder) и Навье–Стоксу (cookedProfileCascade), где именно кованая лестница взрывала манифестационных кандидатов. Дверь для честного закона открыта.

Свидетель-отсутствие — и самая сильная конкретная локализация в программе

Как у Мерсенна, отклонение здесь — не точка-данные, а \(\Pi\)-свидетель: FermatTwinAbsenceAbove P, утверждение, что каждый Ферма-близнец сидит младшим членом не выше \(P\). Плумбинг связывает его с целью точно: неограниченность Ферма-близнецов \(\iff\) свидетелей отсутствия нет (fermatTwinCentersUnbounded_iff_no_absence 🟢). Про домен свидетеля мы знаем нижнюю грань — и она рекордная.

Теорема 48.4 (fermatAbsenceBound_ge_65537, 🟢). Всякая граница отсутствия не меньше 65537.

Почему это верно. Здесь ветвь Ферма даёт самую сильную конкретную локализацию близнецов во всей программе. Конкретные Ферма-близнецы (fermat_twin_instances 🟢) — это \(k = 1\): пара \((5, 7)\); \(k = 2\): пара \((17, 19)\); и — рекорд — \(k = 4\): \(F_4 = 65537\) и \(F_4 + 2 = 65539\), оба просты. Пара при \(k = 4\) зелёно существует, и никакой свидетель отсутствия не может отсечь её снизу — значит, любая граница \(\ge 65537\).

Заметим и честный провал между ними: \(k = 3\) пары не даёт, \(F_3 + 2 = 259 = 7 \cdot 37\) составное (fermat_twin_non_instance 🟢) — Ферма-близнецы не автоматичны, и это тоже зелёная теорема. За 65537, впрочем, начинается настоящая тьма: предъявить свидетеля отсутствия значило бы решить открытую задачу о хвосте Ферма-близнецов.

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

Дальше фронт повторяет мерсенновский буква в букву, только на данных Ферма. Закон манифестации FermatManifestationLaw гейчен свидетелем отсутствия: негейченная форма «\(\forall P\), отсутствие манифестирует» при \(P = 0\) вместе с принятой границей дала бы поставку — бесконечную допустимую семью потоков, которой отклонение «расплачивается» (см. словарь), — на разрешённом масштабе — противоречие с зелёной невозможностью (no_deviationFlowSupply_at_resolved_scale, взятой у Римана и не передоказываемой).

Гейт по зелёно-непредъявимому свидетелю — несущая стена, а не украшение; ровно на её отсутствии взорвались кандидаты Янг–Миллса и Навье–Стокса. И теперь — две главные теоремы, обе зелёные, обе с подлинным потреблением гипотез.

Теорема 48.5 (fermatRefutation_carries_engine, 🟢 — читаемая форма). Свидетель отсутствия + закон манифестации + сведённые книги на масштабе не ниже \(P\) предъявляют вечный двигатель — как объект, ConcreteEuclideanEngineWitness, до всякого убийства.

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

Теорема 48.6 (fermatTwinsUnbounded_of_noEngine_and_boundary_and_manifestation, 🟢 — essence). Нет двигателей + принятая граница + закон манифестации \(\Rightarrow\) Ферма-близнецы неограничены.

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

Цена — и почему мы её снова не заплатили

Трилемма пройдена: свидетель непредъявим (любая граница \(\ge 65537\), а предъявить = решить открытую задачу), закон не разрешим зелёно ни в какую сторону, ковки нет (isEmpty_properCenterPeel_three_one). По тому же машинному критерию, что впустил риманову границу и отверг кандидатов Янг–Миллса, Навье–Стокса, P/NP и Ходжа, поле fermatBoundary допустимо.

И вот его цена:

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

Декрет был бы ровно Ферма-близнецовой силы — не слабее и не сильнее, как у Римана и Мерсенна. Но знак эвристики здесь инвертирован жёстче, чем у Мерсенна.

У Мерсенна сумма \(\sum\) по twin-парам всего лишь сходилась, прямо бесконечности не запрещая. У Ферма стандартная эвристическая сумма \(\sum 2^{-2^k}\) сходится почти мгновенно, и — что решает дело — известный хвост составных чисел Ферма огромен: простыми известны лишь \(F_0\) через \(F_4\), а \(F_5\) через \(F_{32}\) все доказуемо составны. Консенсус ждёт, что новых простых Ферма нет вовсе.

Значит, правая часть этого \(\iff\) — не просто «против ожиданий», а против ожиданий с самой отрицательной ожидаемой истинностью во всей программе. Ставить на неё непротиворечивость всего карантина было бы ставкой ещё дальше от разумного, чем мерсенновская.

Мы решили так же, как в §16: поле не добавлено — намеренно. Закон живёт определением в зелёном фронте (как жил закон Римана до §10), вся строгая цепь доказана с границей-гипотезой, таинт карантина — машинный след аксиомы в зависимостях (см. словарь) — не изменился, а вердикт зафиксирован §16 дословно и записан в реестр §17: допустимо, но отложено по знаку эвристики.

Итог раздела. Машинный критерий говорит «можно»; честность говорит «можно — не значит нужно», и на Ферма это «нужно» отрицательнее, чем где-либо ещё.

Примечание. Отметим, чего эта глава не притязает и что вскрывает сама. Импликация «близнецы \(\Rightarrow\) Ферма» не записана, не доказана и не известна математике — маркер охвата noTwinsToFermatImplicationClaimed стоит в ветви явно, чтобы это нельзя было тихо забыть.

Фронт держит запрет вакуумности №3: ни одного свободного Prop-поля, ни одного свободного гейта, ни одного переименованного вывода — каждая гипотеза именована арифметически. Свидетель здесь — именованное \(\Pi\)-утверждение об отсутствии, поставка — тот же строгий объект DeviationFlowSupply, что у Римана, и модуль даже не импортирует карантин.

Философское отступление: ставка против сходящейся эвристики

У этой главы есть исторический патрон, и он поучителен ровно наоборот к тому, к чему ведёт нас машина. Сам Ферма верил, что простыми будут все числа \(F_k\) — красивая гипотеза, которую Эйлер опроверг одним делением: \(641 \mid F_5\). Ферма поставил против сходящейся эвристики, поставил на «ожидаемо-ложное» — и проиграл.

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

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

Риман прошёл не потому, что трилемма у него была легче — она была ровно та же, — а потому, что знак эвристики смотрел в сторону, где ставить не стыдно. Ферма трилемму проходит столь же чисто (свидетель непредъявим, закон неразрешим, ковать нечего) — и всё же машина честно говорит «нет», потому что честность отвечает на вопрос «стоит ли поставить», а не только «можно ли».

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

Ферма и Мерсенн за тем же горизонтом

Обе ставки этой серии — мерсенновская (43) и здешняя, фермовская — отложены по знаку эвристики: границы машинно допустимы, и обе сознательно не взяты. Оставался вопрос, висевший в воздухе: а нет ли пути изнутри — обосновать закон манифестации, не прося декрета вовсе? Модуль Engine/FermatMersenneEpistemic.lean (весь 🟢) закрывает этот вопрос для двух фронтов сразу — тем же горизонтом, за которым в 56 остались Коллатц и P/NP.

Механика знакома. Опровергнуть при законе и сведённых книгах — значит предъявить двигатель как объект: это уже доказанные fermatRefutation_carries_engine и mersenneRefutation_carries_engine.

Самообосновать же закон поверх собственного свидетеля опровержения — значит собрать того же двигателя у себя внутри и погибнуть об стену lexRank: пакет InternalisedFermatGround строит свидетеля (internalisedFermatGround_builds_engine 🟢) и самоуничтожается (no_internalisedFermatGround 🟢); мерсенновское зеркало InternalisedMersenneGround строит и гибнет дословно так же (internalisedMersenneGround_builds_engine, no_internalisedMersenneGround — обе 🟢).

«Узнать нельзя изнутри» — теперь теорема обеих ветвей, зеркала коллатцевской и P/NP-версий.

Теорема 48.8 (fermatCause_unknowable, mersenneCause_unknowable, 🟢). Внутреннего самообоснования причины не существует ни в одной ветви: \(\neg\,\mathsf{InternalKnowledgeOfFermatCause}\) и \(\neg\,\mathsf{InternalKnowledgeOfMersenneCause}\), где \(\mathsf{InternalKnowledgeOfFermatCause}\) есть пакет InternalisedFermatGround — закон манифестации плюс собственный свидетель за-горизонтом, собирающий двигателя внутри себя — а мерсенновский предикат зеркален.

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

Итоговый статус fermatMersenne_locked_behind_engine_status 🟢 держит всё вместе: локализации доменов (граница отсутствия \(\ge 65537\) у Ферма, \(\ge 29\) у Мерсенна), обе теоремы непознаваемости, аудит цены — условный на ту самую не взятую границу — и стену no_someConcreteEuclideanEngine.

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

Примечание (что мы не утверждаем). Это не решение вопросов о Ферма- и Мерсенн-близнецах и не Гёдель: никакой теоремы о неполноте — только модель-внутренняя эпистемика, пижонхол-самоуничтожение о вполне-фундированность. Створки, где участвует граница, условны на TheStrictLastStep00Obligation, которой ветвям сознательно не дано.

И оговорка силы: связка слабее P/NP-эталона, где beyondOwnHorizon зелёно инстанцируем при малых масштабах (concreteSupply_unbounded_smallScale), — здесь ни одно поле пакета зелёно не реализуемо: свидетель отсутствия стоил бы решения открытой задачи о хвосте, сведённые книги — содержания не взятого декрета. Зато сильнее коллатцевской тавтологичной пары ground/¬ground: beyondOwnHorizon — не отрицание закона, и противоречие оплачено подлинной двигательной конструкцией.

Содержательные дихотомии unknowable_or_fermat_books_never_resolve и unknowable_or_mersenne_books_never_resolve держат обе руки честно — левая доказана. Карантин модуль не импортирует; таинт репозитория не меняется.

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

Теперь две ветви с инвертированным знаком — Мерсенн и Ферма — стоят фронтами без полей: трилеммы пройдены (свидетель непредъявим, закон неразрешим, ковки нет), границы машинно допустимы, и обе сознательно не взяты.

То, что у Мерсенна было единичным решением по знаку эвристики, у Ферма становится правилом серии, и §17 фиксирует его для всего арифметического зоопарка: честная граница требует зелёно-непредъявимого свидетеля — и ставки, за которую не стыдно. У Ферма второе условие нарушено резче, чем где-либо: у него самая отрицательная ожидаемая истинность в программе, и потому он — не исключение из правила, а его самый ясный случай.

twin_prime_conjecture остаётся sorry; таинт карантина — прежний; ни одна открытая задача не объявлена решённой. Простые Ферма подождут своего 641-го делителя или своей вечности — но решение о них, как и о совершенных числах Мерсенна, сделано с открытыми глазами.

---

← 47. Совершенные числа · Оглавление · 49. Геометрия пути →