53. Бёрч–Свиннертон-Дайер: восьмая маска, где движок — это сам спуск¶
← 52. Диадическая модель · Оглавление · 54. Соседи за горизонтом →
Lean-источник:
Engine/BSDFront.lean(зелёное ядро спуска + паритет-мост + честные 🔴-ворота + свидетели трилеммы). ПереиспользуетEngine/UniversalEngine(запрет двигателя по рангу) иEngine/RiemannLiouville(rank-parity узел). Ядро заземлено на реальные объекты mathlib:WeierstrassCurve.Affine.Point,WeierstrassCurve.LSeries, классNorthcott,AddCommGroup.fg_of_descent. Это не доказательство BSD; такса карантина не меняется (16),sorryпо-прежнему один.
Где мы¶
Осталась одна задача тысячелетия без своей тени — гипотеза Бёрча–Свиннертон-Дайера. Она тоже читается через запрет вечного двигателя, но входит в семью иначе, и в этом весь её интерес.
У семи прежних масок движок сторожит: отклонение от нормы оказывается замаскированным двигателем, и запрет его убивает. У BSD движок не сторожит — он работает методом. Ведь алгебраический ранг эллиптической кривой доказан конечным ровно бесконечным спуском Ферма. Тот самый спуск, что стоит в основании всей программы, здесь — не запрет, а инструмент.
Спуск — это и есть движок¶
Теорема Морделла–Вейля говорит: группа рациональных точек E(ℚ) конечно порождена, E(ℚ) ≅ ℤ^r ⊕ T.
Доказывают её спуском: каноническая высота Нерона–Тейта ĥ — положительно определённая квадратичная
форма, а по свойству Нортокотта точек ограниченной высоты конечно много. Значит спуск по высоте
обязан оборваться — и обрыв даёт конечную порождённость.
Это ровно наш запрет: бесконечная строго убывающая цепь высот — вечный двигатель, а его нет.
Теорема 53.1 (bsd_descent_has_no_engine, 🟢). На реальной группе точек W.toAffine.Point эллиптической кривой высотный спуск не имеет вечного двигателя: для любой высотной модели спуска \(M\) не существует PerpetualEngine M.descentStep, то есть строго убывающая по высоте \(h\colon W.\text{toAffine.Point}\to\mathbb{N}\) бесконечная цепь точек невозможна.
«Почему это верно.» Высота — это ℕ-ранг, а ранг переносит запрет двигателя из универсальной
формы: UniversalEngine.no_perpetual_engine_of_natRank. Носитель здесь — настоящий
W.toAffine.Point из mathlib (с его групповым законом), а механизм — тот же, что у Northcott и
AddCommGroup.fg_of_descent: фундированность высоты обрывает спуск. Модель обитаема (не вакуумна) —
предъявлен конкретный свидетель над ℚ.
Примечание (где именно граница дозволенного). Каноническую высоту Нерона–Тейта mathlib ещё не содержит (есть Вейль-высота и приближённый закон параллелограмма — в работе), поэтому высота у нас именована. Но носитель и групповой закон — реальные, и запрет спуска выведен строго. Заземление честное: тень лежит на настоящей кривой, а не на макете.
Паритет — тот же rank-parity узел¶
Чётность ранга связана с аналитикой: гипотеза о паритете утверждает (−1)^rank = w(E), где w(E) —
корневое число, знак функционального уравнения. А (−1)^rank — это в точности тот же rank-parity
инвариант, что стоит за Риманом: Лиувилль λ(n) = (−1)^Ω(n).
Теорема 53.2 (bsd_parity_is_rankParity, 🟢). Чётность ранга совпадает с лиувиллевой: для любых \(r, n \in \mathbb{N}\) с \(n \neq 0\) и \(\Omega(n) = r\) верно \((-1)^r = \lambda(n)\) в \(\mathbb{Z}\).
«Почему это верно.» Прямой мост к RiemannLiouville.liouville_eq_neg_one_pow_rank — то же знаковое
правило, тот же флип при отнятии простого множителя. Паритет BSD — не новый зверь, а наш узел, надетый
на ранг эллиптической кривой.
Естественно спросить: не декретировать ли этот паритет первопричиной, как мы декретировали закон Римана? Мы честно проверили — и нет.
Примечание (вердикт трилеммы: честной границы нет). Настоящее корневое число
w(E)— глубокий аналитический инвариант, которого в mathlib нет. Над доступной заглушкой (RootNumber w := w = ±1, свободное значение) закон(−1)^r = wудовлетворяется выборомw(bsd_parityLaw_satisfiable), а универсальная форма рефутируема (bsd_parityLaw_not_universal). Значит декрет паритета был бы вакуумен — как у P/NP, Янг–Миллса и Ходжа. Поэтому мы не трогаем аксиому и оставляем паритет честно открытым: связь с узлом остаётся концептуальной, а не декретом. Такса — прежние 16.
Аналитический мост — честно открытый¶
Само сердце BSD — равенство алгебраического и аналитического рангов: rank E(ℚ) = ord_{s=1} L(E,s).
L-функцию кривой mathlib уже определяет (WeierstrassCurve.LSeries, через Эйлерово произведение),
и мы на неё честно ссылаемся. Но её аналитические свойства — продолжение к s=1, порядок нуля,
функциональное уравнение — не доказаны нигде.
Определение 53.3 (WeakBSD, 🔴). Открытый вход: для эллиптической кривой \(W/K\) и натуральных чисел \(\text{algRank},\, \text{aRank}\) предикат \(\mathrm{WeakBSD}(W,\text{algRank},\text{aRank})\) есть \(\mathrm{AnalyticRank}(W,\text{aRank}) \wedge \text{algRank} = \text{aRank}\). Мы его не доказываем: это именованный вход, а не теорема.
Люди прошли лишь края: при аналитическом ранге ≤ 1 (Гросс–Загир и Колывагин, через точки Хегнера и
эйлеровы системы) BSD доказана и Ша конечна; в среднем — свыше 66% кривых (Бхаргава–Скиннер–Чжан). При
ранге ≥ 2 — открыто всё. Наш движок аналитику не закрывает: его роль здесь — спуск, а не мост.
Философское отступление: инструмент, а не сторож¶
У BSD движок показывает своё второе лицо. Всюду прежде он был запретом — стеной, о которую разбивается отклонение. Здесь он метод — та самая лестница спуска, которой Ферма и Морделл считали точки. Один и тот же объект: невозможность вечно уменьшать натуральные числа. В шести масках эта невозможность запрещает; в BSD — вычисляет.
И это честно очерчивает предел прочтения. Спусковую сторону (ранг конечен) и чётностную (тот же узел) мы
читаем как тень запрета — зелёно, на реальной кривой. Но аналитическое сердце — согласие ранга с нулём
L-функции — от запрета двигателя не зависит и остаётся за горизонтом. Тень есть; тело — вне её.
Примечание (эпистемика БСД). У БСД нет собственной эпистемической оси — и это зафиксировано машинно (
Engine/BSDEpistemic.lean). Предложенная пара ground/beyondOwnHorizon вырождается: вторая нога — это буквально поле убывания высоты, свободное по построению, так что вся связка совпадает с уже доказанным запретом двигателя спуска (bsdGround_coincides_with_engine). Это не слабость, а точный факт о том, где живёт содержание БСД: не в эпистемике, а в data-anchor — в открытом равенстве рангов. Попутно видно, что воротаAnalyticRankсвободно выполнимы (analyticRank_gate_satisfiable), аWeakBSDсводится к голомуalgRank = aRank(weakBSD_reduces_to_bare_equality) — именно там и остаётся вся честная 🔴-открытость.Примечание (содержательные ворота). Старые свободные ворота теперь имеют содержательную замену —
Engine/BSDAnalyticAnchor.lean. Аналитический ранг перестаёт быть свободным параметром и становится настоящим mathlib-понятием:analyticRankOf L := analyticOrderAt L.Lambda 1— порядок нуля продолжения в точкеs = 1. Но это работает лишь когда подана сама данность: красный входContinuedLFunctionнесёт функциюΛ, совпадающую сWeierstrassCurve.LSeriesтам, где ряд Дирихле абсолютно суммируем (agreement), и аналитичную вs = 1(analyticAtOne) — то самое продолжение, которого в mathlib нет (даже с границей Хассе точка1лежит вне полуплоскости сходимости,1 < 3/2). На этих данных строятся содержательные воротаWeakBSDContentful. Контраст и есть честный пуант: старые ворота выполнимы даром при всех рангах сразу, новые пришпиливают ранг (contentfulGate_pins_rank— не более одного на якорь) и стоят данных. Мы ничего не утверждаем о настоящей L-функции — только именуем вход, за который платят данными, а не декретом.
Место в общем ходе¶
Приложение C даёт восьмой задаче её тень, не приукрашивая. Формализаций BSD, Морделла–Вейля, канонической
высоты, аналитики L-функций эллиптических кривых нет нигде (по разысканиям — Loeffler–Stoll 2025,
Angdinata–Xu 2023). Значит даже структурное engine/rank-parity прочтение, заземлённое на реальные объекты
mathlib, — первое в своём роде. Но это не решение BSD: зелено — лишь спуск и паритет-узел; аналитический
мост честно 🔴; декрета не добавлено (трилемма). twin_prime_conjecture остаётся sorry; такса — прежние 16.
← 52. Диадическая модель · Оглавление · 54. Соседи за горизонтом →