30. Гипотеза Римана: контрапозиция через двигатель¶

← 29. Последнее звено · Оглавление · 31. Риман через Лиувилля →

Lean: Engine/RiemannBranch.lean (NontrivialZeroM, no_zero_of_one_le_re, TrivialBelowZeroClassification, nontrivialZero_in_strip, EngineBridge, riemannHypothesis_of_engine_bridge, not_RH_gives_engine, TwoTransportLaw, twoTransportLaw_holds, TwoTransportBridge, riemannHypothesis_of_two_transport). Ядро: Engine/EPMI.lean (no_infinite_descent), Engine/TwoGap.lean (det_law_rank33). RiemannHypothesis — из mathlib (официальная формулировка через нули riemannZeta, все нетривиальные нули), а не самодельный def. Расположение нулей Re ≥ 1 — из mathlib (riemannZeta_ne_zero_of_one_le_re); классификация Re ≤ 0 ⟹ тривиальный — явный аналитический вход TrivialBelowZeroClassification.

Завершив часть V, мы располагаем полностью замкнутым механизмом невозможности вечного двигателя: абстрактная теорема no_infinite_descent доказана без аксиом, а закон переноса двойки det_law_rank33 проверен машинно. Естественно спросить, что ещё этот механизм способен закрыть тем же приёмом от противного, каким мы замыкали близнецов. В настоящей главе мы разбираем побочную ветвь — гипотезу Римана (RH) — и делаем это честно: показываем, где именно проходит граница доказанного, и почему RH здесь остаётся условной на одном явно выделенном узле.

Честная рамка: чего мы не утверждаем¶

Прежде всего зафиксируем то, что легко было бы выдать за большее, чем оно есть.

Примечание. RH не следует логически из бесконечности близнецов. Это два независимых арифметических утверждения, и мы не записываем импликацию twin ⟹ RH как теорему — она была бы ложной. Всё, что делает эта ветвь, — переиспользует тот же доказанный EPMI-механизм и ту же схему контрапозиции, а не переносит истинность одной гипотезы на другую.

Логическая форма ветви ровно та же, что у близнецов. Мы уже видели её в паре «нет двигателя ⟹ есть близнецы»; здесь она принимает вид

\[\bigl(\neg P \Rightarrow \text{Engine}\bigr)\ \wedge\ \neg\,\text{Engine}\ \Longrightarrow\ P, \qquad P := \text{RH}.\]

Содержательно мы строим цепочку

\[\neg\text{RH}\ \Longrightarrow\ \exists\,\text{нуль }\rho,\ \mathrm{Re}\,\rho \ne \tfrac12 \ \overset{H_{RH}}{\Longrightarrow}\ \text{вечный двигатель}\ \Longrightarrow\ \bot,\]

где последний шаг — уже доказанный no_infinite_descent, а помеченный \(H_{RH}\) переход — единственный открытый узел ветви. Никакой редукции мы за доказательство не выдаём: RH ниже формализована как условная теорема, посылка которой явно выписана и явно помечена открытой.

Определения: нетривиальный нуль и RH¶

Вводим объект, о котором идёт речь. Мы работаем с дзета-функцией Римана riemannZeta из mathlib и интересуемся её нулями внутри критической полосы.

Гипотеза Римана — из mathlib (не самодельная). По принципу «всё внешнее — из mathlib» целью служит именно RiemannHypothesis из mathlib: квантор по всем нулям riemannZeta, исключая тривиальные (-2(n+1)) и s = 1. Это строго общее, чем «нули только в полосе», и мы обязаны дать Re = 1/2 для всякого такого нуля.

Определение 30.1 (NontrivialZeroM, нетривиальный нуль). \(\mathrm{NontrivialZeroM}(\rho) :\Longleftrightarrow \zeta(\rho)=0 \wedge (\neg\exists n,\ \rho = -2(n{+}1)) \wedge \rho \ne 1\) — ровно посылка mathlib-RH, собранная в один объект.

Локализация нуля (доказано + один вход). Вход здесь — в домовом смысле: именованное открытое утверждение, которого не хватает до цели (см. словарь). Чтобы применить двигатель, нужно загнать нетривиальный нуль в полосу \(0 < \mathrm{Re}\,\rho < 1\):

Верх (\(\mathrm{Re}\,\rho < 1\)) — замыкается mathlib-аналитикой (не ядром двигателя). no_zero_of_one_le_re из riemannZeta_ne_zero_of_one_le_re (у дзеты нет нулей при \(\mathrm{Re}\ge 1\)). ⚠️ Честная оговорка: это неисчезание дзеты на \(\mathrm{Re}\ge 1\) — аналитический результат PNT-уровня, доказанный в mathlib, а не нами. «Доказано» тут = «выводимо из mathlib», а не из ядра. Он лишь ограничивает полосу, не помещает нуль на \(\tfrac12\) и не закрывает ни один мост.
Низ (\(\mathrm{Re}\,\rho > 0\)) — явный аналитический вход. TrivialBelowZeroClassification: всякий нуль с \(\mathrm{Re}\,\rho \le 0\) тривиален. Это классика (функциональное уравнение); mathlib даёт лишь значения тривиальных нулей (riemannZeta_neg_two_mul_nat_add_one), но не обратную классификацию, — поэтому берём её явной помеченной гипотезой, а не самодельной RH.

nontrivialZero_in_strip собирает оба факта: нетривиальный нуль лежит строго в полосе. Отрицание RH, которое мы эксплуатируем, — существование нетривиального нуля \(\rho\) с \(\mathrm{Re}\,\rho \ne \tfrac12\).

Мост `EngineBridge`: где живёт вся аналитика¶

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

Определение 30.2 (EngineBridge, мост двигателя).

\[\mathrm{EngineBridge}\ :\Longleftrightarrow\ \forall\,\rho,\ \zeta(\rho)=0\ \wedge\ 0<\mathrm{Re}\,\rho\ \wedge\ \mathrm{Re}\,\rho<1\ \wedge\ \mathrm{Re}\,\rho \ne \tfrac12\ \Longrightarrow\ \exists\,A\ge 1,\ \exists\,H:\mathbb N\to\mathbb N,\ \forall t,\ \mathrm{DescentStep}\,A\,(H\,t)\,(H(t{+}1)).\]

В Lean (посылка — нуль строго в полосе с \(\mathrm{Re}\ne\tfrac12\); локализацию в полосу делают mathlib + вход TrivialBelowZeroClassification):

def EngineBridge : Prop :=
  ∀ ρ : ℂ, riemannZeta ρ = 0 → 0 < ρ.re → ρ.re < 1 → ρ.re ≠ 1 / 2 →
    ∃ (A : ℕ) (H : ℕ → ℕ), 1 ≤ A ∧ ∀ t, DescentStep A (H t) (H (t + 1))

Напомним из части I, что DescentStep A h h' : Prop := A * h' < h — один успешный clean-спуск, в котором высота падает не менее чем в \(A\) раз. Свидетель — в домовом смысле конкретный объект, удостоверяющий утверждение (см. словарь): здесь \(H:\mathbb N\to\mathbb N\) с \(\mathrm{DescentStep}\,A\,(H\,t)\,(H(t{+}1))\) при всех \(t\) — это ровно бесконечная clean-цепь строго убывающей высоты, то есть вечный двигатель.

Содержательно мост говорит следующее. Асимметрия \(\mathrm{Re}\,\rho \ne \tfrac12\) отвечает несбалансированности между «левой» и «правой» половинами критической полосы. Из интуиции переноса двойки: сбалансированность на \(\tfrac12\) — это ровно то условие, при котором прирост и убыль массы вдоль descent компенсируются и цепь обязана либо выйти на boundary, либо упереться в дно.

Нуль вне \(\tfrac12\) снимает эту компенсацию и даёт «бесплатное» направленное перекачивание массы: каждый шаг descent строго понижает высоту без выхода на boundary, чего в сбалансированном режиме быть не может. Именно это перекачивание и есть двигатель, запрещённый no_infinite_descent.

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

RH от противного: условная теорема¶

Теперь соберём цепочку. Утверждаем, что при истинности моста RH следует.

Теорема 30.3 (riemannHypothesis_of_engine_bridge). Если TrivialBelowZeroClassification и EngineBridge, то (mathlib-)RiemannHypothesis.

Докажем. Возьмём произвольный нуль \(\rho\), не тривиальный и \(\ne 1\) (это ровно посылка mathlib-RH). Сначала локализуем его в полосу \(0<\mathrm{Re}\,\rho<1\) через nontrivialZero_in_strip (верх — из mathlib, низ — из входа классификации). Предположим от противного \(\mathrm{Re}\,\rho \ne \tfrac12\). Мост даёт \(A\ge 1\) и цепь высот \(H\) с \(\mathrm{DescentStep}\,A\,(H\,t)\,(H(t{+}1))\) — вечный двигатель. Но его не существует: no_infinite_descent, дающая \(\bot\). Откуда \(\mathrm{Re}\,\rho = \tfrac12\):

theorem riemannHypothesis_of_engine_bridge
    (hClass : TrivialBelowZeroClassification) (H_RH : EngineBridge) :
    RiemannHypothesis := by
  intro ρ hz htriv hne1
  have hρ : NontrivialZeroM ρ := ⟨hz, htriv, hne1⟩
  obtain ⟨hpos, hlt⟩ := nontrivialZero_in_strip hClass hρ
  by_contra hne
  obtain ⟨A, Hgt, hA, hchain⟩ := H_RH ρ hz hpos hlt hne
  exact no_infinite_descent hA Hgt hchain

Почему это работает и что это значит. Работает — потому что вся аналитика вынесена в посылку H_RH, а хвост цепочки (двигатель ⟹ \(\bot\)) — уже машинно проверенный факт.

Вывод. Значит это ровно то, что контрапозиция RH сведена к аналитическому мосту EngineBridge, и ни на йоту больше: истинность RH мы здесь получаем условно, при допущении моста.

Полезно выписать контрапозицию и в прямом виде — как «\(\neg\)RH порождает двигатель», без by_contra:

Теорема 30.4 (not_RH_gives_engine). Если EngineBridge и \(\neg\text{RH}\), то существуют \(A\ge 1\) и \(H:\mathbb N\to\mathbb N\) с \(\mathrm{DescentStep}\,A\,(H\,t)\,(H(t{+}1))\) при всех \(t\).

Здесь мы разворачиваем \(\neg\text{RH}\) через not_forall, извлекаем свидетеля-нуль \(\rho\) вне \(\tfrac12\) и подаём его в мост. Эта форма делает явным механизм: отрицание RH — это конкретный асимметричный нуль, а мост превращает его в конкретную бесконечную descent-цепь. Противоречие с no_infinite_descent тогда буквально то же самое, что закрывает близнецов, — общий, а не два разных финала.

Связка с близнецами: один общий узел вместо двух¶

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

Определение 30.5 (TwoTransportLaw, закон переноса двойки абстрактно).

\[\mathrm{TwoTransportLaw}\ :\Longleftrightarrow\ \forall\,m,a,b,v,q,r,s\ge \text{(с }1\le m\text{)},\ 6m-1 = a b v\ \wedge\ 6m+1 = q r s\ \Longrightarrow\ q r s = a b v + 2.\]

Это ровно тождество «правый спутник больше левого на два» на уровне факторизаций. И оно уже доказано — конкретным тождеством det_law_rank33 из Engine/TwoGap.lean:

Теорема 30.6 (twoTransportLaw_holds). TwoTransportLaw выполнен.

theorem twoTransportLaw_holds : TwoTransportLaw :=
  fun _ _ _ _ _ _ _ hm h1 h2 => det_law_rank33 hm h1 h2

Заметим: это не аксиома и не гипотеза, а свидетельствуемая пропозиция — любое из тождеств семейства det_law_* (det_law_rank33, det_law_CD, det_collapse, …) годится в качестве свидетеля.

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

Определение 30.7 (TwoTransportBridge, узел-связка).

\[\mathrm{TwoTransportBridge}\ :\Longleftrightarrow\ \bigl(\mathrm{TwoTransportLaw}\ \Rightarrow\ \mathrm{EngineBridge}\bigr).\]

Подчеркнём: это импликация, а не эквивалентность гипотез. Мы не отождествляем RH с близнецами и не переносим истинность; мы лишь спрашиваем, следует ли из уже доказанного ядра переноса двойки тот самый мост, что нужен RH. Если TwoTransportBridge доказан, RH получается из уже имеющегося:

Теорема 30.8 (riemannHypothesis_of_two_transport). Если TrivialBelowZeroClassification и TwoTransportBridge, то (mathlib-)RiemannHypothesis.

theorem riemannHypothesis_of_two_transport
    (hClass : TrivialBelowZeroClassification) (bridge : TwoTransportBridge) :
    RiemannHypothesis :=
  riemannHypothesis_of_engine_bridge hClass (bridge twoTransportLaw_holds)

Доказательство прозрачно: подставляем в связку уже доказанный twoTransportLaw_holds (Теорема 30.6), получаем EngineBridge, и применяем Теорему 30.3 (riemannHypothesis_of_engine_bridge).

Итог раздела. Значение формулировки в том, что она точно называет цену «одновременности» ветвей: открытыми остаются ровно TwoTransportBridge — одна импликация «перенос двойки ⟹ мост» — и аналитический вход TrivialBelowZeroClassification, а не отдельная дзета-аналитика и не эквивалентность двух гипотез.

Статус честно и открытая гипотеза¶

Подведём границу доказанного, не сдвигая её ни в одну, ни в другую сторону.

Доказано. Условная теорема riemannHypothesis_of_engine_bridge (TrivialBelowZeroClassification ∧ EngineBridge ⟹ mathlib-RH), её контрапозиция not_RH_gives_engine, а также riemannHypothesis_of_two_transport — всё через машинно проверенные no_infinite_descent, twoTransportLaw_holds и mathlib riemannZeta_ne_zero_of_one_le_re (no_zero_of_one_le_re, nontrivialZero_in_strip). Цель — официальная mathlib-RiemannHypothesis (все нетривиальные нули), а не самодельная. Хвост «двигатель ⟹ \(\bot\)» — общий с близнецами.
Открыто. EngineBridge (эквивалентно: TwoTransportBridge) — связь «нуль в полосе вне \(\tfrac12\) ⟹ вечный двигатель» — и аналитический вход TrivialBelowZeroClassification (нули с \(\mathrm{Re}\le 0\) тривиальны; функциональное уравнение, mathlib даёт лишь значения тривиальных нулей). RH здесь условна на этих двух узлах и не доказана.
⚠️ Циркулярность impossible-engine маршрутов (машинно, RiemannImpossibleEngineOff §7bis). offCriticalBridge_iff_RH: раз factory безусловно невозможна, вход OffCriticalRiemannEngineBridge эквивалентен RH дословно (мост выполним лишь вакуумно — то есть даром, без содержательного свидетеля; о вакуумности и переименовании цели см. словарь). Аналогично criticalStripBridge_iff_no_stripZero (strip-вариант) и spectralBridge_forces_no_violation (rank-jump-мост скрыто несёт ¬LiouvilleViolation = RH-содержание). Эти маршруты — точные переформулировки RH, а не понижения сложности; их ценность — форма (двигатель), не редукция.

Гипотеза (узел, подлежащий закрытию). Асимметрия \(\mathrm{Re}\,\rho \ne \tfrac12\) у нетривиального нуля влечёт нарушение баланса переноса двойки такой силы, что порождает бесконечную clean-цепь \(\mathrm{DescentStep}\,A\,(H\,t)\,(H(t{+}1))\), — то есть TwoTransportLaw ⟹ EngineBridge.

План закрытия. Мы намечаем его в терминах уже построенного аппарата, не выдавая набросок за доказательство.

Перевести асимметрию \(\mathrm{Re}\,\rho \ne \tfrac12\) в количественный дисбаланс левого и правого спутников вдоль descent — использовать явную форму \(qrs = abv + 2\) из twoTransportLaw_holds как точку баланса, отклонение от которой оценивается через положение нуля.
Показать, что этот дисбаланс не поглощается boundary-выходом (см. декомпозицию boundary из 24), то есть цепь остаётся clean на каждом шаге.
Собрать из шагов явный свидетель \(H\) и константу \(A\ge 1\), замкнув EngineBridge; далее вся работа делается наличным no_infinite_descent.

Каждый из трёх пунктов — самостоятельная аналитическая задача, и мы не утверждаем, что они малы. Честная оценка прежняя: этот мост, по-видимому, сопоставим по трудности с самой RH.

Мост к следующей главе¶

Итак, ветвь Римана держится ровно на одном арифметическом дисбалансе — отклонении переноса двойки от точной величины \(+2\). Тот же вопрос «насколько велико отклонение и не рвётся ли оно на boundary» возникает и вне дзеты — в чисто мультипликативной статистике знаков делителей. В [31 Лиувилль] мы берём функцию Лиувилля \(\lambda(n)=(-1)^{\Omega(n)}\) и её сумматор — и показываем, как тот же descent-механизм и та же дихотомия «баланс либо двигатель» переносятся на дефект чётности \(\Omega\), давая ещё одну контрапозиционную ветвь на общем EPMI-ядре.