54. Соседи за горизонтом: тени открытых задач

← 53. Бёрч–Свиннертон-Дайер · Оглавление · 55. Коллатц →

Lean-источники: Engine/ChowlaFront.lean, Engine/AbcFront.lean, Engine/BealFront.lean, Engine/LehmerFront.lean, Engine/LandauFront.lean. Каждая тень заземлена на реальную доказанную теорему mathlib (🟢), а сама открытая гипотеза остаётся честным именованным 🔴-гейтом. Ни одна не решена; такса карантина не меняется (16), sorry по-прежнему один. Новизна формализационная.

Где мы

Восемь масок позади — среди них все шесть открытых проблем тысячелетия. Но запрет вечного двигателя — спуск, высота, паритет ранга — живёт и в соседних открытых задачах. Здесь мы даём тень пяти из них одним приёмом: реальный якорь mathlib плюс честный гейт. Якорь — доказанная теорема (полиномиальный аналог, конечность, структура), которая и есть прочтение через движок; гейт — сама открытая гипотеза, названная и не доказанная.

Чоула и Сарнак: тот же rank-parity узел

Функция Лиувилля λ(n) = (−1)^Ω(n) — это в точности наш rank-parity инвариант, что стоит за Риманом. Гипотеза Чоулы говорит: паритет Ω не коррелирует по сдвигам, ∑_{n≤x} λ(n)λ(n+h) = o(x). Это тот же запрет коллапса паритета в одну чётность, что охраняет и близнецов, и Римана.

Теорема 54.1 (chowlaCorrelation_zero_eq_card, 🟢). Диагональ h=0 даёт совершенную само-корреляцию: ∑_{n≤x} λ(n)² = x.

«Почему это верно.» λ(n)² = 1 для n≥1 (λ есть ±1), так что диагональ вырождается в подсчёт. Это резкий контраст тому, что Чоула запрещает при h>0: там сумма обязана гаситься. Флип знака при умножении на простое (chowla_parity_flip, реюз RiemannLiouville) — тот же ход спуска.

Гейт (ChowlaConjecture, SarnakConjecture, 🔴). Корреляции o(x) и ортогональность Мёбиуса — открыты. Тао доказал лишь логарифмически-усреднённый и нечётный случаи; полностью — нет.

Примечание. У этого узла есть и эпистемический склон (Engine/ChowlaEpistemic.lean): совершенный коллапс паритета — хвост, на котором знак Лиувилля постоянен, — невозможен, потому что удвоение аргумента флипает знак, и константа гибнет о ту же флип-стену (no_parityCollapse_of_flip). Оттого узел непознаваем изнутри (chowlaCause_unknowable), а сама корреляция ещё и жёстка точечно: на нечётном срезе она никогда не ноль (chowlaCorrelation_ne_zero_of_odd), тогда как оба знака Лиувилля достигаются кофинально (liouville_two_pow). Мы честны в охвате: связка покрывает лишь коллапс-моду, двигательного факта у Чоулы в репозитории нет — и сводка так и названа, chowla_locked_behind_flip_wall, без слова «двигатель». Это не решение Чоулы и не Гёдель; красные гейты остаются красными.

abc: полиномиальный аналог доказан

Гипотеза abc: для взаимно простых a+b=c число c ограничено радикалом, c < K_ε·rad(abc)^{1+ε}. Полиномиальный аналог — теорема Мейсона–Стотерса — доказан, и он в mathlib.

Теорема 54.2 (polynomial_abc_shadow = Polynomial.abc, 🟢). Для взаимно простых многочленов a+b+c=0 над полем степень ограничена радикалом произведения (либо все производные нулевые).

«Почему это верно.» Это готовая теорема mathlib (вронскиан + взаимная простота). Степенная граница через радикал — и есть engine-прочтение: качество тройки не может убежать в бесконечность, оно конечно. Радикал целого числа (Int.radical, Nat.radical) — тоже реальный, не заглушка.

Гейт (AbcConjecture, 🔴). Интегральный abc — открыт. Заявка Мочидзуки (IUT) сообществом не принята; приз не востребован.

Примечание. Эпистемику (Engine/AbcEpistemic.lean) мы строим только вокруг наивной формы ε = 0, и это важно проговорить. Наивный закон опровергнут одним свидетелем (abc_exponent_one_counterexample: 1 + 8 = 9, rad(72) = 6 < 9), а поставка качества при ε = 0 неограниченна — LTE-семейство 3^(2^k) пробивает любой линейный горизонт (unboundedQualitySupplyExponentOne). Отсюда линейного заземления изнутри нет (abcCause_unknowable); попутно вырос радикальный инструментарий над mathlib — natRad_pow, natRad_mul_of_coprime. Настоящий abc-гейт (ε > 0) этим не тронут: там такой поставки нет и быть не обязано, вся открытость живёт в ε-слабине.

Бил и Ферма–Каталан: чистый Ферма-спуск

Метод бесконечного спуска Ферма — буквально наш движок. И его полиномиальная форма доказана.

Теорема 54.3 (polynomial_fermat_catalan_shadow = Polynomial.flt_catalan, 🟢). При 1/p+1/q+1/r<1 уравнение u·aᵖ+v·bᵍ+w·cʳ=0 для взаимно простых многочленов вынуждает a,b,c быть константами.

«Почему это верно.» Готовая теорема mathlib, её доказательство — бесконечный спуск по характеристике p. Рядом — fermatLastTheoremFour/Three (flt_four_is_descent), доказанные тем же спуском; мы честно предъявляем их и выводим descent-без-двигателя через EPMI/UniversalEngine.

Гейт (BealConjecture, FermatCatalanConjecture, 🔴). Интегральный Бил (Aˣ+Bʸ=Cᶻ, x,y,z>2, взаимно просты ⟹ общий делитель) и полный Ферма–Каталан — открыты. Дармон–Гранвиль доказали конечность лишь для фиксированных показателей (через Фалтингса); приз $1M не востребован.

Примечание. Этой волной фронт починился в нескольких местах. Сам гейт Ферма–Каталана мы переписали на тройки значений, а прежнюю кортежную форму зелёно опровергли (fermatCatalan_tupleForm_refuted: 1^m + 2^3 = 3^2 даёт бесконечно много кортежей при одной тройке (1,8,9)) — честный урок формализации. Диагональные классы показателей закрыты через спуск Ферма: при (3,3,3) и (4,4,4) решений нет вовсе (beal_no_solution_exponent_three, beal_no_solution_exponent_four), а «теорема Била над k[X]» предъявлена как polynomial_beal_shadow. Множество обитаемо (fermatCatalan_value_witness), гипотеза взаимной простоты несуща (beal_common_factor_witness: 2^3 + 2^3 = 2^4). Эпистемическая связка bealCause_unknowable честно формальна — пара ground/¬ground без двигательной оплаты; содержательное живёт рядом, отдельными теоремами, а не в ней.

Лемер: высота-конечность как в BSD

Мера Малера — это высота, и тот же Нортокотт, что вычислял ранг у BSD, работает здесь.

Теорема 54.4 (mahler_northcott_shadow = finite_mahlerMeasure_le, 🟢). Многочленов ограниченной степени и ограниченной меры Малера — конечно много.

«Почему это верно.» Это Нортокотт (готовая теорема mathlib): высота фундирована, бесконечного высотного спуска нет — то самое ядро, что у BSD и универсального движка. Граница снизу даётся Кронекером (kronecker_boundary): мера Малера равна 1 тогда и только тогда, когда корни — корни из единицы (циклотомический случай).

Гейт (LehmerConjecture, 🔴). Равномерный зазор c>1 над единицей для нециклотомических — открыт. Наименьшее известное — число Лемера ≈ 1.17628; Кронекер закрывает лишь границу M=1.

Примечание. У этой конечности мы читаем и эпистемический склон (Engine/LehmerEpistemic.lean): Нортокотт-коробка конечна зелёно (mahlerBox_finite), и потому удержать под одним таким горизонтом подлинно бесконечное семейство многочленов изнутри нельзя — инъекция бесконечного в конечное гибнет о ту же пижонхол-стену вечного двигателя, и «узнать нельзя изнутри» здесь теорема, а не лозунг (lehmerCause_unknowable). Это модель-внутренняя эпистемика, не Гёдель и не решение: о самом зазоре c>1 не утверждается ничего, гейт остаётся красным, а декрета здесь нет и не было — модуль зелёный целиком. Без двигателя остаётся только внешняя проверка: на каждом конечном степенном горизонте зазор находится перебором Нортокотт-каталога (lehmer_at_bounded_degree); открыт лишь побег степени за всякий горизонт.

Примечание (граница зелёного и красного проведена машинно). Модуль Engine/LehmerBoundedDegree.lean фиксирует эту границу точно. Лемер при ограниченной степени — уже зелёная теорема: для каждой степени n существует c > 1 без мер Малера в интервале (1, c) (lehmer_at_bounded_degree). Доказательство фольклорное — окно (1, 2] конечно по Нортокотту, у конечного множества есть минимум, ниже него мер нет. Но константа c = c(n) зависит от степени: единая c на все степени сразу (UniformLehmerGap, 🔴) — и есть сама гипотеза Лемера. Аудит на переименование раскрывает это машинно-точно: uniformLehmerGap_iff_all_degrees доказывает, что якорь равносилен «в lehmer_gap_at_bounded_degree можно взять одну константу на все степени», — то есть красный вход это в точности равномерная версия зелёной теоремы, и его имя не провозит контрабандой никакого прогресса.

Landau: простые n²+1

Дирихле (в mathlib, реально) даёт простые в арифметических прогрессиях — на этом стоят «стороны» 6m±1. Но n²+1 — не прогрессия, и его бесконечность остаётся честным гейтом.

Теорема 54.5 (landauPrimes_infinite_of_unbounded, 🟢). Если простых n²+1 неограниченно много, то их множество бесконечно. Плюс oddLandauPrime_even_k: при нечётном k число k²+1 чётно, так что простое k²+1 > 2 требует чётного k — настоящий вычет, а не украшение.

«Почему это верно.» Чистая структурная переупаковка (как в ветви Полиньяка): из неограниченности следует бесконечность. Никакого нового содержания — вся суть в гейте.

Гейт (Landau4thUnbounded, 🔴). Бесконечность простых n²+1 (Харди–Литтлвуд) — открыта. Иванец: бесконечно много n²+1 с не более чем двумя простыми множителями.

Примечание. Эпистемический слой (Engine/LandauEpistemic.lean) канонизирует гейт: неограниченность простых k²+1 равносильна бесконечности множества (landau4thUnbounded_iff_infinite), красный вход остаётся ровно одним. Вычетный факт перестал быть украшением — гейт локализован на чётный канал (landauPrime_even_of_two_lt), а сами простые Ландау лежат в реальном дирихлетовском классе 1 mod 4, который бесконечен по mathlib (landau_lives_in_dirichlet_class); открыта именно селекция внутри шеренги. В отличие от Била, здесь мы построили двигательный факт — landauRefutation_carries_engine: опровержение при законе манифестации предъявляет вечный двигатель как объект. Честно: закон (LandauManifestationLaw) не декретирован (полиньяк-класс, слабее безусловных стен), а landauCause_unknowable — не решение 4-й проблемы и не Гёдель.

Общая мораль

Пять теней — один приём: где у людей есть доказанный якорь (полиномиальный abc и Ферма–Каталан, Нортокотт и Кронекер, Дирихле, структура Лиувилля), мы предъявляем его зелёно как прочтение через движок; где стоит открытая гипотеза — называем её честным гейтом и не притворяемся, что закрыли. Ни одна из пяти не решена, декретов первопричины не добавлено (как в арифметическом зоопарке), такса — прежние 16. По разысканиям, ни Чоула, ни abc, ни Бил, ни Лемер, ни Landau прежде так не читались; новизна — формализационная, не математическая. Один и тот же запрет узнаётся и за горизонтом восьми масок.

---

← 53. Бёрч–Свиннертон-Дайер · Оглавление · 55. Коллатц →