Гольдбах и Лежандр: свидетель, которого можно проверить, но нельзя предъявить¶
← 45. Софи Жермен · Оглавление · 47. Совершенные числа →
Lean-источник:
Engine/GoldbachManifestationFront— зелёная цепь, вся 🟢;Engine/LegendreDesertFront— зелёная цепь, вся 🟢 (плюс уникальный безусловный компаньон — постулат Бертрана). Обозначения статуса: 🟢 — доказано при стандартных аксиомах; 🟡 — условно на аксиомуstep00FirstCause; 🔴 — открытый вход.
Где мы¶
Риман и Мерсенн научили нас читать опровержение как двигатель, и мы уже различаем два сорта свидетелей. У Мерсенна свидетель был Π-утверждением — границей, целым классом чисел, отсутствием, растянутым в бесконечность; предъявить его нельзя, потому что это значило бы обозреть весь хвост разом. У Римана свидетель был объектом-данными — конкретным нулём вне прямой; предъявить его нельзя, потому что построить такой нуль значило бы опровергнуть RH. Эти два фронта — Гольдбах и Лежандр — идут по римановой линии, но доводят её до предела, и в этом их общая, редкая для серии черта.
Их свидетель — объект-данные, и при этом поточечно разрешимый. Не Π-форма, которую надо доказывать; не аналитический нуль, чью нулевость надо устанавливать анализом, — а конкретное натуральное число, про которое машина за конечное время говорит «да» или «нет».
Это сильнейшая форма непредъявимости во всей серии, и парадокс её виден сразу: каждого отдельного кандидата проверить легче всего, а предъявить настоящего свидетеля — невозможно.
Разберём оба фронта, а затем и то, почему лёгкость проверки и невозможность предъявления здесь не противоречат друг другу, а суть две стороны одного квантора.
Гольдбах: фальшивка умирает мгновенно, настоящая опровергла бы гипотезу¶
Бинарная гипотеза Гольдбаха утверждает, что всякое чётное E ≥ 4 есть сумма двух простых.
Отклонение здесь — конкретное чётное число, у которого такого разложения нет: GoldbachViolationAt E
значит 4 ≤ E, E чётно и ¬ GoldbachRep E.
Ключевое свойство этого предиката — он разрешим насквозь. Экзистенциал «E есть сумма двух простых»
сводится к ограниченному перебору одного простого p < E с проверкой простоты дополнения E − p.
Ядровая Nat.decidableExistsLT вместе с Nat.decidablePrime дают инстанс автоматически, а decide
работает над этой формой напрямую. Отрицание разрешимого разрешимо, Even и 4 ≤ · тоже — значит,
разрешимо и само нарушение.
Отсюда — первая пара зелёных теорем, и обе про поточечную разрешимость в действии.
Теорема 46.1 (goldbach_upTo_52, 🟢). Всякое чётное E в диапазоне 4 ≤ E < 52 есть сумма двух
простых.
Почему это верно. decide перебирает все такие E над разрешимой ограниченной формой и находит
разложение для каждого; результат переносится на GoldbachRep через доказанную эквивалентность. Ни
одной гипотезы, ни следа аксиомы — чистая машинная проверка.
Теорема 46.2 (goldbachViolation_ge_52, 🟢). Всякий свидетель нарушения Гольдбаха сидит при
E ≥ 52.
Почему это верно. Меньшие чётные кандидаты уже отсеяны предыдущей теоремой: если бы нарушение
жило ниже 52, goldbach_upTo_52 дала бы ему разложение, а свидетель разложение отрицает —
противоречие. Так локализуется домен: фальшивка, поставленная где угодно ниже 52, умирает decide'ом
на месте.
Но выше 52 начинается настоящая тьма. Литература проверила гипотезу до 4·10^18 (Оливейра э Силва и
другие) — эта граница не формализована, и зелёно у нас только ≥ 52. Предъявить настоящего свидетеля
значило бы опровергнуть Гольдбаха.
Манифестационный фронт над этим свидетелем устроен по-риманову — объект-квантифицирован, без гейта
(гейт — именованный открытый красный вход, которого не хватает до цели; см. словарь).
Закон GoldbachManifestationLaw пробегает тип свидетелей GoldbachViolation и говорит: каждое
конкретное нарушение манифестирует.
На всяком леджер-масштабе не ниже самого числа, всюду где проекция
сводит книги — то есть разрешает коллизии потоков на данном масштабе, — отклонение проявляется
неоплатимой бесконечной поставкой потоков (DeviationFlowSupply
— тот же объект, что строит риманов фронт).
Гейт свидетелем здесь не нужен: якорь масштаба M0 := E привязан к самому числу — высота отклонения
есть само отклонение, — и негейченной «взрывной» формы просто не существует. И вот несущая сборка.
Теорема 46.3 (noGoldbachViolation_of_manifestation_and_boundary, 🟢 — essence). Нет двигателей +
принятая граница + закон манифестации ⟹ нарушений Гольдбаха нет — то есть гипотеза Гольдбаха верна.
Почему это верно. Гипотетический свидетель V даёт масштаб M0 := V.1. Принятая граница даёт
разрешающую проекцию ровно на нём (через le_refl). Закон превращает нарушение в бесконечную семью
потоков — не ex falso (не выводом «из лжи что угодно»), а как данные. Конечный ключ сталкивает двух её членов, из коллизии собирается
двигатель-свидетель — и убивает его именно гипотеза «двигателей нет». Через мост
goldbachConjecture_iff_no_violation та же тройка доводится и до самой гипотезы Гольдбаха.
Чтение прямое: неоплаченное чётное число проявило бы вечный двигатель. Знак эвристики здесь — за гипотезу: квантор закона пробегает ожидаемо пустой тип свидетелей, закон ожидаемо вакуумно-истинен, и это точное зеркало Римана, а не инвертированного Мерсенна.
Поля декрета мы, как и у Мерсенна, не добавляем — закон живёт определением в зелёном фронте.
Лежандр: единственный зелёный компаньон — и честное признание, что он не спасает¶
Гипотеза Лежандра (1808) утверждает, что между любыми последовательными квадратами n² и (n+1)²
при n ≥ 1 лежит простое. Отклонение — простая пустыня в этом интервале: LegendreViolationAt n
значит 1 ≤ n и PrimeDesertBetween (n²) ((n+1)²), то есть ни одного простого строго между
квадратами.
Предикат снова разрешим — через bounded-ball форму (Nat.decidableBallLT, редуцируемую под
decide), — и всё повторяется, зеркаля пару Гольдбаха.
Теорема 46.4 (legendre_holds_upTo_10, 🟢). Для всех n с 1 ≤ n < 11 нарушения Лежандра нет:
\(\forall n,\ 1 \le n < 11 \Rightarrow \neg\,\mathrm{LegendreViolationAt}(n)\).
Почему это верно. decide перебирает всех кандидатов 1 ≤ n < 11 над разрешимой bounded-ball
формой и для каждого находит простое строго между n² и (n+1)²; ни аксиомы, ни native_decide.
Теорема 46.5 (legendreViolation_ge_11, 🟢). Всякий свидетель нарушения Лежандра сидит при
n ≥ 11: \(\forall V:\mathrm{LegendreViolation},\ 11 \le V.1\).
Почему это верно. Меньшие точки отсеяны Теоремой 46.4 (legendre_holds_upTo_10): свидетель ниже
11 получил бы простое в своём интервале, а свидетель это отрицает — противоречие. Литературная граница
далеко за 10^18 не формализована; зелёно только ≥ 11. Всё как у Гольдбаха.
Но у этого фронта есть то, чего нет больше нигде в серии, — зелёный безусловный компаньон.
Теорема 46.6 (no_desert_doubles, 🟢). Простая пустыня не может пережить удвоение: между n и 2n
(при n ≠ 0) простое есть всегда.
Почему это верно. Это прямая перепаковка постулата Бертрана
(Nat.exists_prime_lt_and_le_two_mul, mathlib, безусловный). Никакой открытой задачи, никакого гейта:
между n и 2n простое существует — это доказанная теорема, а не декрет. Единственное место во всём
фронте, где вакуум не имеет щели по-настоящему, безусловно.
И ровно здесь — честное раскрытие, без которого зелёный Бертран превратился бы в завышенную заявку.
Бертран покрывает удвоение [n, 2n], а Лежандру нужен интервал (n², (n+1)²). Достаточно ли первого
для второго?
Теорема 46.7 (legendre_interval_shorter_than_bertrand, 🟢). При n ≥ 3 имеем (n+1)² < 2n².
Почему это верно. Чистое неравенство, nlinarith. Но следствие принципиально: интервал Лежандра
короче бертрановского удвоения. Значит, зелёное «пустыня не удваивается» бессильно на квадратичной
щели — Бертран не решает Лежандра.
Модуль фиксирует это явным флагом NoBertrandToLegendreImplicationClaimed = True: никакая импликация
Бертран ⟹ Лежандр здесь не заявлена и не доказана. Зелёная сила блока Бертрана остаётся строго слабее
открытого Лежандра, и мы это не прячем, а выписываем машинно.
Дальше объект-фронт повторяет риманову архитектуру дословно. LegendreManifestationLaw
объект-квантифицирован по свидетелям, якорь масштаба M0 := V.1² привязан к самой пустыне.
Теорема 46.8 (noLegendreViolation_of_manifestation_and_boundary, 🟢 — essence). Нет двигателей +
принятая граница + закон манифестации ⟹ свидетелей Лежандра нет:
\(\neg\,\mathrm{SomeConcreteEuclideanEngine} \wedge \mathrm{TheStrictLastStep00Obligation} \wedge
\mathrm{LegendreManifestationLaw} \Rightarrow \neg\,\mathrm{Nonempty}\ \mathrm{LegendreViolation}\).
Почему это верно. Та же тройка, что в Теореме 46.3 (noGoldbachViolation_of_manifestation_and_boundary):
гипотетический свидетель V даёт масштаб M0 := V.1², граница разрешает проекцию ровно на нём (через
le_refl), закон поставляет семью потоков, из коллизии собирается двигатель-свидетель — и его убивает
гипотеза «двигателей нет». Через мост legendreConjecture_iff_no_violation та же тройка доводится и до
самой гипотезы Лежандра. Свидетель заякорен ровно там, где живёт пустыня, — на n².
Примечание. У обоих фронтов ни одного свободного Prop-поля, свободного гейта или переименованного вывода — каждая гипотеза именована арифметически, поставка — тот же строгий объект
DeviationFlowSupply, что и у Римана, а Impossible-сторона на разрешённых масштабах — переиспользованная зелёная теоремаno_deviationFlowSupply_at_resolved_scale, никогда не декрет.Оба модуля карантин — единственный модуль, где живёт аксиома
step00FirstCause, — не импортируют;axiom,sorry,native_decide— нет. И оба знака эвристики направлены за гипотезу: типы свидетелей ожидаемо пусты, законы ожидаемо вакуумно-истинны — ориентация Римана, не Мерсенна. Поля декрета не добавлены намеренно: серийное расширение обесценило бы карантин.
Философское отступление: свидетель, который проверяем, но не производим¶
Через всю причинную линию тянется один образ — свидетель, которого можно проверить, но нельзя предъявить. В близнецовой, римановой и мерсенновской ветвях эта непредъявимость имела аналитический или бесконечный корень: чтобы предъявить нуль вне прямой, надо было бы иметь его как результат анализа; чтобы предъявить границу Мерсенн-близнецов, надо было бы обозреть весь бесконечный хвост. Свидетеля нельзя было даже записать конечным объектом.
Здесь непредъявимость тоньше — и потому острее. Каждый кандидат в свидетели конечен и
машинно-проверяем: чётное число E, точка n. Дай нам любого конкретного претендента — и мы за
конечное время скажем decide'ом, свидетель он или фальшивка.
Трудность не в проверке какого-либо одного; она целиком в кванторе. Гипотеза говорит «для всех
E» и «для всех n», а никакой конечный перебор такое не закрывает: сколько бы мы ни проверили —
4·10^18 у Гольдбаха, ещё дальше у Лежандра, — за проверенным краем остаётся бесконечный хвост
непроверенных, и именно в нём мог бы прятаться единственный контрпример.
Это ровно граница разрешимости и неразрешимости, прочитанная на арифметике: поточечно всё разрешимо, а
квантифицированное по всему ℕ — уже нет, и никакая машина не пройдёт бесконечность за конечное
время.
Двигательное чтение даёт этому точную форму. Контрпример был бы щелью в вакууме — единственной чётной дырой, единственной квадратичной пустыней. И найти его стоило бы того же невозможного: неоплаченное отклонение проявило бы вечный двигатель.
Вывод. Мы можем сколько угодно проверять, что вакуум пока без щелей, и не можем предъявить щель — не потому, что она где-то есть и её трудно достать, а потому, что её наличие есть по построению запрещённый двигатель. Проверяемость каждого кандидата и непредъявимость свидетеля — не в противоречии: первое живёт на уровне точки, второе — на уровне квантора, и мостом между ними служит именно запрет двигателя.
И здесь стоит быть честными до конца — ради того единственного места, где вакуум щели не имеет по
настоящей теореме. Бертран зелёный и безусловный: между n и 2n простое есть всегда, без всякого
декрета, без гейта, без ставки. Это самая твёрдая арифметика во всей главе — и ровно поэтому так
поучительно, что она до Лежандра не дотягивает.
Интервал (n², (n+1)²) короче удвоения [n, 2n] (при n ≥ 3 строго, (n+1)² < 2n²), и на этой
квадратичной щели безусловная сила Бертрана кончается. Соблазн был бы велик — выдать Бертрана за
«почти Лежандра», — и мы явным флагом от него отказались.
Итог раздела. Зелёная теорема рядом с открытой задачей не делает открытую задачу зелёной; она лишь чётко очерчивает, где кончается доказанное и начинается ставка. В этом и урок фронта: даже там, где у нас есть настоящий безусловный факт, честность требует показать, чего именно он не закрывает.
Гольдбах и Лежандр за тем же горизонтом¶
У этой главы, как у Коллатца и P/NP, есть эпистемический склон — Engine/GoldbachLegendreEpistemic,
целиком зелёный. Соберём «внутреннее самообоснование решения»: носитель якорит масштаб не ниже
своего свидетеля (E ≤ M0 у Гольдбаха, n² ≤ M0 у Лежандра), сводит книги и несёт манифестацию
этого одного свидетеля — структуры InternalisedGoldbachGround и InternalisedLegendreGround.
Из такой посылки двигатель-свидетель строится как объект — internalisedGoldbachGround_builds_engine
и internalisedLegendreGround_builds_engine, не ex falso, а та же цепь, что в несущей сборке,
только топливом служит манифестация одного свидетеля, а не весь закон. Нарушение при сведённых
книгах — это и есть двигатель, теперь выписанный конструкцией.
А дальше сборка самоуничтожается. На разрешённом масштабе поставки нет — противоречие поставляет
зелёная двигательная no_deviationFlowSupply_at_resolved_scale, и чтобы форма не была пустой
отговоркой, её непустота предъявлена зелёной deviationFlowSupply_of_twinBound.
Отсюда no_internalisedGoldbachGround и no_internalisedLegendreGround, а из них — теоремы
goldbachCause_unknowable и legendreCause_unknowable: узнать причину изнутри нельзя — теорема,
не лозунг.
Развилки goldbach_no_internal_decision_without_engine и
legendre_no_internal_decision_without_engine раскладывают это по створкам: опровергнуть изнутри =
предъявить двигатель (условно на закон-определение — безусловного аналога
nonHalting_carries_perpetual_engine у этих фронтов нет и быть не может без решения самой открытой
задачи); самообосноваться = самоуничтожиться; решает лишь внешняя граница — гипотеза
TheStrictLastStep00Obligation — вместе с законом.
У Лежандра к трём створкам добавлена четвёртая,
безусловная: бертрановская Теорема 46.6 (no_desert_doubles) с честным флагом
NoBertrandToLegendreImplicationClaimed — сильна, но квадратичную щель по-прежнему не закрывает.
И здесь «проверка, а не вывод» звучит в чистейшей форме за всю серию. У Коллатца проверка — прогон
орбиты, у P/NP — конечнотопливный бюджет; здесь она буквально decide: свидетель поточечно
разрешим, и про каждого кандидата машина отвечает за конечное время.
Теоремы goldbach_verification_not_derivation и legendre_verification_not_derivation ставят три факта
рядом: внутреннее знание причины невозможно; проверка машинно досмотрена (Теорема 46.1
goldbach_upTo_52, Теорема 46.4 legendre_holds_upTo_10); и потому свидетель отодвинут ровно на
глубину досмотра — ≥ 52 и
≥ 11, ни шагом дальше (литературные 4·10^18 не формализованы, зелёно только это). Решение
находимо ровно настолько далеко, насколько достаёт проверка — здесь это не оборот речи, а сама
структура теоремы.
Общая сводка — goldbachLegendre_locked_behind_engine_status, зеркало
pnp_locked_behind_engine_status и, как у него, без декрет-конъюнкта: полей Гольдбаха и Лежандра в
декрете нет — серийное расширение обесценило бы карантин.
Примечание (что мы не утверждаем). Это не решение гипотезы 1742 года и не задачи 1808-го, и не Гёдель — ни неполноты, ни неподвижной точки, только модель-внутренняя двигательная стена. Слой честно слабее эталона P/NP: поле
beyondOwnHorizon— вера в закон-определение, зелёной инстанции у него нет (типы свидетелей ожидаемо пусты), тогда как у P/NP аналогичный слой (concreteSupply_unbounded_smallScale) зелёно истинен. Модуль карантин не импортирует, таинт репозитория не меняется; обе гипотезы остаются открытыми входами 🔴 при запертой изнутри двери.
Место в общем ходе¶
Теперь линия «что стоило бы опровержение» покрывает и два старейших вопроса о простых. Гольдбах и Лежандр входят той же манифестационной архитектурой, что Риман: объект-свидетель, знак эвристики за гипотезу, поле декрета не взято — но со своим предельным свойством, поточечной разрешимостью, которая делает их самой сильной формой непредъявимости в серии.
Правило серии дополнилось ещё одним различением: непредъявимость свидетеля не обязана иметь бесконечный или аналитический корень. Она может целиком сидеть в кванторе над разрешимым предикатом, и тогда лёгкость проверки любого кандидата и невозможность предъявить свидетеля оказываются двумя чтениями одного «для всех».
Бертран остаётся единственной зелёной безусловной опорой этого фронта — и честно отмеченной как
недостаточная для Лежандра. GoldbachConjecture и LegendreConjecture остаются открытыми входами;
таинт карантина не сдвинут; ни одна открытая задача не объявлена решённой.