Риман через первопричину: отклонение, которого двигатель не может позволить¶

← 37. Римановы фронты · Оглавление · 39. P/NP: оплата сертификатов →

Lean-источник: Engine/RiemannManifestationFront.lean — зелёная цепь (модуль не импортирует карантин); Engine/RiemannLawEpistemic.lean — эпистемический маршрут; Engine/Step00FrontClosureAudit.lean — машинная запись о том, почему Риман был ИЗЪЯТ из декрета (Option A); Engine/RiemannDualEngineFront.lean — дуальный маршрут-спутник. Обозначения статуса: 🟢 — доказано при стандартных аксиомах; 🟡 — доказано условно на аксиому step00FirstCause; 🔴 — открытый вход.

Обновление статуса (Option A). Риман больше не граница декрета. В ранних черновиках на step00FirstCause висело поле riemannBoundary, из которого проецировалась RH (🟡); это поле и его проекция изъяты, и ни одна римановская декларация больше не заражена аксиомой. Остаётся зелёная условная редукция: RH следует из закона манифестации плюс близнецовая граница — это редукция, а не результат декрета. Причина и честная асимметрия с близнецами разобраны в разделе «Римановская граница, изъятая (Option A)» ниже.

Где мы¶

Близнецы прошли через одну и ту же машину: зелёная арифметика на целых (генеалогии, ранг lexRank, двойной перенос XY − ZW = 2, спуск, конечноключевые проекции, пигеонхол — принцип ящиков, см. словарь) свела всё к одному узлу причинной формы, и узел мы приняли намеренной аксиомой — первопричиной (глава 33). Гипотеза Римана кажется задачей из совсем другого мира — комплексный анализ, дзета-функция, нетривиальные нули. И тем удивительнее, что тот же самый маршрут проходит и здесь.

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

Что такое отклонение нуля¶

Напомним постановку. Нетривиальные нули дзета-функции Римана лежат в критической полосе 0 < Re s < 1. Гипотеза Римана утверждает, что все они сидят ровно на серединной прямой Re s = 1/2. Отклонение — это нуль, соскочивший с прямой: нетривиальный нуль с Re s ≠ 1/2. В Lean у него точный mathlib-тип OffCriticalZero: он несёт ζ(s) = 0, свидетельство нетривиальности, s ≠ 1 и, главное, Re s ≠ 1/2. Гипотеза Римана в этих терминах — это просто «отклонений не существует».

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

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

Первый пункт — причинный закон, некогда римановская граница декрета, ныне изъятая (Option A); остаётся зелёная условная редукция. Второй — зелёная теорема. Разберём их по порядку.

Закон манифестации: как отклонение выдаёт себя¶

Что значит «отклонение проявляется»? Сначала припишем каждому нулю натуральный масштаб, на котором он живёт: zeroHeight Z = ⌊|Im s|⌋ — целую часть модуля мнимой части. Дальше вводим ключевой объект.

Определение 38.1 (DeviationFlowSupply A M0). «Неоплаченная поставка» на леджер-масштабе (A, M0) — это бесконечная допустимая семья расширенных порождённых потоков: $$\mathrm{DeviationFlowSupply}(A, M_0) \;:=\; \exists\,\mathcal{F} \subseteq \mathrm{ExtProperFlow}(A, M_0),\ \mathrm{InfiniteFamily}(A, M_0, \mathcal{F}). \tag{38.1}$$

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

Теорема 38.2 (deviationFlowSupply_of_twinBound, 🟢 — свидетель содержательности). Для любых $A, M_0$ из ограничения на twin-центры выше масштаба $M_0$ (TwinBoundAbove M0) зелёно следует DeviationFlowSupply A M0: $\mathrm{TwinBoundAbove}(M_0) \Rightarrow \mathrm{DeviationFlowSupply}(A, M_0).$

Теперь сам закон. Он говорит, что отклонение обязано выдавать себя такой поставкой всюду, где книги сведены:

Определение 38.3 (RiemannManifestationLaw). Для каждого отклонения $Z$ и каждого масштаба $M_0 \ge \mathrm{zeroHeight}(Z)$: всюду, где проекция $\mathrm{proj}$ сводит книги (разрешает коллизии), есть неоплаченная поставка DeviationFlowSupply: $$\forall Z\ \forall A, M_0\ \big(\mathrm{zeroHeight}(Z) \le M_0 \Rightarrow \forall \mathrm{proj}\ (\mathrm{Resolves}(\mathrm{proj}) \Rightarrow \mathrm{DeviationFlowSupply}(A, M_0))\big). \tag{38.2}$$

Подчеркнём форму: закон утверждает положительное событие — «отклонение проявляется», причинную связь «нуль → манифестация». Он не утверждает «нулей нет». Это принципиально: сила и честность декрета целиком зависят от того, что мы кладём в него причину, а не заключение.

Примечание (почему отклонение обязано выдавать себя). Поставка DeviationFlowSupply A M0 — это не новая абстракция, а ровно та же бесконечная допустимая семья расширенных порождённых потоков, которую зелёно строит близнецовая граница (deviationFlowSupply_of_twinBound, см. выше). Оба сюжета кормит одна ранговая машина. А почему off-critical нуль вынужден её выдать — видно из балансовой интуиции переноса двойки главы 30: равновесие на Re s = 1/2 — это точка, где прирост и убыль массы вдоль descent компенсируются. Асимметрия Re s ≠ 1/2 снимает компенсацию и даёт «бесплатное» направленное перекачивание массы — а бесконечно перекачивать массу и значит бесконечно поставлять потоки. Поэтому закон говорит о событии: нуль вне прямой оставляет след, а не «нулей нет».

Зелёная невозможность: сторона «нельзя» — это теорема, а не декрет¶

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

Теорема 38.4 (no_deviationFlowSupply_at_resolved_scale, 🟢). Для любой проекции $\mathrm{proj}$ на масштабе $(A, M_0)$, разрешающей коллизии, поставки не существует: $\mathrm{Resolves}(\mathrm{proj}) \Rightarrow \neg\,\mathrm{DeviationFlowSupply}(A, M_0).$

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

Примечание (пигеонхол по шагам). Разберём цепочку словами. На масштабе, где проекция сводит книги, вселенная стабильна и без свободной энергии. Бесконечная же семья потоков не помещается под конечный ключ — по принципу ящиков (пигеонхол) два потока обязаны совпасть под проекцией, и это столкновение — не безобидное: из него собирается конкретный двигатель-свидетель. Но такого двигателя нет — его убивает no_someConcreteEuclideanEngine. Значит никакая бесконечная поставка не выживает на сводящем книги масштабе: сторона «нельзя» — теорема.

Это и есть водораздел честности. Сторону «нельзя» — что поставки не бывает — мы доказываем зелёно. Декретируется только сторона «обязано проявиться». Мы никогда не постулируем невозможность нуля; мы постулируем лишь то, что нуль, если он есть, оставляет следы, — а отсутствие следов на сводящем книги масштабе выводим из запрета двигателя.

Сборка: отклонений нет, значит гипотеза Римана верна¶

Соединим закон, границу и запрет двигателя. Получается точное зеркало близнецовой essence-леммы.

Теорема 38.5 (noOffCriticalZero_of_manifestation_and_boundary, 🟢). Отсутствие двигателей ($\neg\,\mathrm{SomeConcreteEuclideanEngine}$) плюс принятая близнецовая граница ($\mathrm{TheStrictLastStep00Obligation}$) плюс закон манифестации ($\mathrm{RiemannManifestationLaw}$) влекут $\neg\,\mathrm{Nonempty}\ \mathrm{RiemannOffCriticalZero}$ — отклонений не существует.

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

Теорема 38.6 (riemannHypothesis_of_manifestation_and_boundary, 🟢). Та же тройка гипотез влечёт $\mathrm{RiemannHypothesis}$ (в точном mathlib-смысле).

Тут вступает единственная тяжёлая аналитика, и она уже сделана в предыдущих главах: классификация тривиальных нулей trivialBelowZeroClassification доказана честной mathlib-аналитикой. Опираясь на неё, из «отклонений нет» извлекается RH. Заметим важное: вся эта цепь — зелёная, она живёт в модуле, который не импортирует карантин — единственное место, где живёт аксиома (см. словарь); аксиома здесь ещё не появлялась.

Примечание (три гипотезы делают работу, а не взрыв). В noOffCriticalZero_of_manifestation_and_boundary каждая посылка несёт свою ношу, и ни одна не пропущена через ложь. Близнецовая граница даёт разрешающую проекцию ровно на высоте нуля zeroHeight Z — там, где книги можно свести. Закон манифестации превращает нуль в бесконечную поставку DeviationFlowSupply. Из поставки, как в предыдущем разделе, собирается двигатель-свидетель. И его убивает hNoEngine — «двигателей нет». Уберите любую из трёх — и вывод не собирается. Единственная тяжёлая аналитика, trivialBelowZeroClassification, — честная mathlib-работа, уже сделанная в главе 37. А «в точном mathlib-смысле» значит буквально: цель — не самодельный предикат, а RiemannHypothesis из mathlib (квантор по всем нетривиальным нулям riemannZeta, см. главу 30).

Римановская граница, изъятая (Option A)¶

В одном черновике аксиома появлялась ещё на одном шаге — когда закон манифестации клали в первопричину как римановскую границу. При Option A это поле изъято: структура Step00FirstCause несёт теперь только близнецовую границу causalBoundary (SerialTwinBoundaryObligation), а step00FirstCause_iff_causalClosure читается Step00FirstCause ↔ SerialTwinBoundaryObligation — единственный конъюнкт. Поле riemannBoundary и его проекция riemannHypothesis_from_firstCause теперь мёртвый код, живущий внутри блока-комментария /- WITHDRAWN -/; ни одна римановская декларация больше не заражена аксиомой. Ниже описана историческая проекция — как запись о том, что было отсоединено.

Теорема 38.7 (riemannHypothesis_from_firstCause, 🔵 — ИЗЪЯТЫЙ мёртвый код, не заражён аксиомой). Из единого расширенного декрета следовала бы гипотеза Римана: $\mathrm{riemannHypothesis\_from\_firstCause} : \mathrm{RiemannHypothesis}$ — получалась применением Теоремы 38.6 (riemannHypothesis_of_manifestation_and_boundary) к no_someConcreteEuclideanEngine, проекции первопричины step00CausalClosure и полю riemannManifestationLaw. При Option A эта декларация изъята; она больше не живая граница декрета.

Останься она живой, машинный список аксиом этой теоремы нёс бы [propext, Classical.choice, Quot.sound, step00FirstCause] — последнее слово выдавало бы таинт: редукция, закрытая декретом, но не доказательство гипотезы Римана. При Option A поле удалено, поэтому ни одна живая римановская декларация вообще не несёт step00FirstCause; таинт репозитория (16, все про близнецы) не включает RH.

Нетронутой остаётся зелёная условная редукция: RH следует из закона манифестации плюс близнецовая граница (Теорема 38.6) — редукция, которая никогда не была и не является результатом декрета.

Примечание (что читать в списке аксиом). После Option A структура Step00FirstCause несёт одно содержательное поле — causalBoundary (SerialTwinBoundaryObligation, близнецовая граница); прежние riemannBoundary и гейт Навье–Стокса отсоединены и лежат теперь в блоках /- WITHDRAWN -/. В списке вроде [propext, Classical.choice, Quot.sound, step00FirstCause] первые три — стандартные аксиомы самого Lean (пропозициональная экстенсиональность, выбор, факторизация); их несёт почти любая обычная теорема, и выделяется только step00FirstCause — единственный декрет репозитория. «Таинт» — машинная метка: декларация наследует аксиому, если та стоит в её списке зависимостей (см. главу 33); текущее заражённое множество — 16, все про близнецы. riemannHypothesis_from_firstCause, будучи изъятым мёртвым кодом, в него не входит.

Честная цена: декрет ровно RH-силы — но это не тавтология¶

Возникает законное подозрение: не спрятали ли мы гипотезу Римана в закон манифестации, просто переименовав её? Ответ дан машинно, и он тонкий.

Теорема 38.8 (riemannManifestation_asserts_RH, 🟢 — зелёная условная эквивалентность). При близнецовой границе, взятой гипотезой, закон манифестации эквивалентен RH: $\mathrm{RiemannManifestationLaw} \iff \mathrm{RiemannHypothesis}.$

То есть да: закон манифестации при близнецовой границе — ровно RH-силы, редукция не слабее вывода — и мы это не прячем, а доказываем. Заметим: при Option A это зелёная условная импликация (близнецовая граница входит гипотезой, а не аксиомой); Риман больше не кладётся в декрет, так что никакой расширенной первопричины здесь не утверждается.

Но вот в чём отличие честного закона от подделки. Есть осуждённый «мост» OffCriticalRiemannEngineBridge, для которого доказано offCriticalBridge_iff_RH — он эквивалентен RH сам по себе, зелёно, без всяких гипотез. Такой мост был бы дословным переименованием цели, и декретировать его нечестно. Наш закон манифестации устроен иначе: импликация «закон ⟹ RH» без границы вообще не собирается — essence-лемма требует границу.

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

Примечание (в чём именно разница цены). Оба объекта эквивалентны RH — но по-разному, и разница честная. offCriticalBridge_iff_RH держится в одиночку: осуждённый мост OffCriticalRiemannEngineBridge равносилен RH сам по себе, без единой гипотезы, — то есть это буквальное переименование цели, и декретировать его было бы прятать RH под другим именем. riemannManifestation_asserts_RH держится только в паре: закон равносилен RH лишь при уже принятой близнецовой границе — без границы essence-лемма не собирается. Мы декретируем не переименованную цель, а причинное условие поверх границы, которую и так уже приняли. Ровно та же архитектура, что у близнецов: узел даёт близнецов не сам, а только будучи принятым декретом.

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

Примечание (нули как энергетические уровни: гипотеза Гильберта–Пойи). У нашей переформулировки есть глубокая физическая тень. Гильберт и Пойа предположили, что нетривиальные нули дзеты — это собственные значения некоторого самосопряжённого оператора, то есть энергетические уровни квантовой системы. Спектр самосопряжённого оператора веществен — и это в точности загнало бы все нули на критическую прямую: RH стала бы утверждением о вещественности спектра, об устойчивости равновесия. Отклонение нуля от прямой в этой картине — комплексное собственное значение, то есть резонанс с ненулевой мнимой частью, неустойчивая мода, накачивающая энергию. Наш язык буквально это и говорит: off-critical нуль — отклонение, которое пришлось бы бесконечно «оплачивать» поставкой потоков, то есть вечный двигатель. Устойчивость спектра и невозможность вечного двигателя оказываются одним и тем же запретом, прочитанным на двух языках.

Примечание (спектральный якорь). Гильберт–Пойя теперь не только образ: Engine/RiemannSpectralAnchor.lean формализует его двумя слоями — и разница между ними и есть урок честности. Наивная реализация нулей «голым» вещественным спектром — множеством E ⊆ ℝ, дающим каждому нулю форму 1/2 + t·I (SpectralRealisation) — собирается даром: при RH берём E := Set.univ, t := ρ.im, и аудит spectralRealisation_iff_RH доказывает, что этот вход дословно эквивалентен RH — зеркало осуждённого моста offCriticalBridge_iff_RH, переименование цели без носителя. Поэтому содержательный якорь обязан нести сам оператор: OperatorSpectralAnchor — самосопряжённый оператор на гильбертовом пространстве, чей спектр вещественен по причине, а не по декрету (мост operatorAnchor_implies_realisation через mathlib-IsSelfAdjoint.mem_spectrum_eq_re). Это красный вход: сам оператор математика должна предъявить, и его в mathlib v4.31 нет — как нет и спектральной теории неограниченных операторов, которой честный Гильберт–Пойя и требует.

Дуальный маршрут-спутник¶

Рядом лежит Engine/RiemannDualEngineFront.lean — три абстрактных ядра под будущую инстанциацию: синхронизация оплат «фантомного» (спектрального) и «подлинного» (ранго-потокового) двигателей (односторонняя оплата = вечный двигатель, потому оплаты синхронны); закон «встреча ⟺ смена ранга на шве»; и счётный мост «близнецы ↔ встречи ↔ нули» с встроенной защитой от вырождения (бесконечность переносится только по инъективным мостам с декодером).

Честная граница: все законы этой серии — входы-поля 🔴, безусловных сильных выводов в ней нет; к тому же мост считает нетривиальные нули, а не off-critical, так что его заполнение не несло бы RH-информации напрямую. Это язык и заготовки, а не мост.

Риман за тем же горизонтом¶

У стены, о которую разбиваются внутренние решения (глава 56), есть и римановский склон. Спросим прямо: что значило бы «решить Римана изнутри» на нашем языке? Не предъявить нуль и не вывести RH, а самообосновать закон манифестации: нести одновременно сам закон и свидетельство, что он добыт из-за собственного горизонта.

Модуль Engine/RiemannLawEpistemic.lean записывает это буквально: связка InternalisedRiemannGround держит поле ground — сам закон — и поле beyondOwnHorizon. И такая связка самоуничтожается:

Теорема 38.9 (no_internalisedRiemannGround, 🟢). Внутреннее самообоснование закона манифестации невозможно: $\mathrm{InternalisedRiemannGround} \Rightarrow \mathrm{False}$, откуда riemannCause_unknowable 🟢 — $\neg\,\mathrm{InternalKnowledgeOfRiemannCause}$ (зеркало collatzCause_unknowable и pnpCause_unknowable). «Узнать нельзя изнутри» здесь теорема, а не лозунг.

Честность сразу: связка формальна, beyondOwnHorizon — это просто ¬ground, тавтологическая пара вида P ∧ ¬P, ровно как у Коллатца, и мы этого не прячем.

Чем оплачена форма — настоящей конструкцией. Единственный внутренний след отклонения — вечный двигатель:

Теорема 38.10 (deviation_carries_engine_at_resolved_scale, 🟢). Из поставки отклонения на разрешающем масштабе собирается конкретный евклидов двигатель: $\mathrm{Resolves}(\mathrm{proj}) \wedge \mathrm{DeviationFlowSupply}(A, M_0) \Rightarrow \mathrm{SomeConcreteEuclideanEngine}$ (стабильная безэнергетическая вселенная, бесконечная семья, пигеонхол-коллизия конечного ключа), потребляя гипотезы по-настоящему, а не через ложь. Это та же цепь, что внутри Теоремы 38.4 (no_deviationFlowSupply_at_resolved_scale), но с двигателем, явленным в выводе.

(Есть и ex-falso-спутник internalisedRiemannGround_builds_engine — маршрут, чья сила лишь в противоречивости посылки (см. словарь), — но несущая часть — не он.)

Оговорка обязательна: в отличие от безусловного на объекте коллатцевского nonHalting_carries_perpetual_engine, римановский двигатель гейтирован разрешающим масштабом — а разрешение и есть открытый twin-узел (при A ≤ 4 оно опровергнуто no_projection_resolves_at_smallScale). Это ровно уровень Коллатца — и ниже эталона P/NP, где beyondOwnHorizon заселён зелёно.

Сводка — трёхразвилка:

Теорема 38.11 (riemann_no_internal_decision_without_engine, 🟢). Конъюнкция трёх утверждений: (1) опровергнуть при сведённых книгах — построить двигатель ($\mathrm{Resolves}(\mathrm{proj}) \wedge \mathrm{DeviationFlowSupply}(A, M_0) \Rightarrow \mathrm{SomeConcreteEuclideanEngine}$, убитый lexRank'ом); (2) самообосноваться — самоуничтожиться ($\mathrm{InternalisedRiemannGround} \Rightarrow \mathrm{False}$); (3) решает только внешний декрет — закон при границе даёт RH ($\mathrm{TheStrictLastStep00Obligation} \Rightarrow \mathrm{RiemannManifestationLaw} \Rightarrow \mathrm{RiemannHypothesis}$). Оба внутренних пути стоят двигателя; открыта одна дверь, и она внешняя. Причём в этом модуле граница фигурирует гипотезой h : TheStrictLastStep00Obligation, не аксиомой: конъюнкт остаётся зелёной импликацией, модуль не импортирует карантин, и таинт репозитория не растёт. Итоговый статус собран в riemann_locked_behind_engine_status 🟢.

И отличие от соседей по горизонту. У P/NP декрет-границы не было, у Коллатца она пала — а при Option A римановская граница тоже изъята: поле riemannBoundary отсоединено от первопричины и больше в ней не стоит. Остаётся зелёная условная редукция, чья цена раскрыта выше (riemannManifestation_asserts_RH — закон эквивалентен RH лишь при близнецовой границе, а не сам по себе). Единственная граница, которую декрет ещё несёт, — близнецы. Эпистемика этого не отменяет и не подпирает: она говорит лишь, что у самообоснования закона манифестации не может быть внутренней опоры — двигатель, который решал бы за нас, запрещён той же машиной, которой мы всё доказываем. Внешняя дверь остаётся единственной, и открывается она через одну близнецовую границу.

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

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

После этой главы картина асимметрична, и Option A эту асимметрию называет. Близнецы входят в декрет через единственную границу causalBoundary (SerialTwinBoundaryObligation); Риман когда-то входил через riemannBoundary, но это поле изъято — оно живёт теперь в блоке /- WITHDRAWN -/, отсоединённом от первопричины. Что обе ветви ещё делят — зелёную ранговую машину; что несут только близнецы — живую границу декрета. Римановская сторона сохраняет свою зелёную условную редукцию (закон + близнецовая граница ⟹ RH), чья цена раскрыта машинно, но границей декрета она уже не является и в таинт ничего не добавляет.

twin_prime_conjecture остаётся sorry; открытые входы 🔴 остальных римановых фронтов (глава 37) не тронуты и остаются честными картами обязательств. Дальше та же машина встречает задачу, где декрет неожиданно оказывается не нужен, — P/NP (глава 39): там неравенство доказывается зелёно, без всякой первопричины.

← 37. Римановы фронты · Оглавление · 39. P/NP: оплата сертификатов →