Навье–Стокс: гладкость через каскад и взятый интеграл¶

← 40. Янг–Миллс · Оглавление · 42. Ходж →

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

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

Прочтение: сингулярность — вечный двигатель, а решение — взятый интеграл¶

Движение двигателя внутри ранга гладко всюду, без точек разрыва; появление такой точки создало бы вечный двигатель; а раз движение гладко, решение можно вывести — взять интеграл. Так мы читаем задачу о существовании и гладкости решений Навье–Стокса, и обе половины этого прочтения реализуются точно.

Гипотетическая сингулярность — это сингулярный каскад SingularCascade: бесконечно много δ-диссипативных стадий, сжатых к одному конечному моменту T. Бесконечная квантованная лестница — тот же вечный двигатель, что и в предыдущих главах. Его невозможность при энергобалансе — зелёная теорема. А «взять интеграл» мы выполняем буквально, и дважды.

Как и с Янг–Миллсом, честная граница проведена сразу и громко: проблему тысячелетия мы не решаем и не объявляем решённой. Существование Лерэ, единственность, настоящая C^∞-регулярность и сам закон EnergyBalanceLaw остаются открытыми (глава 36); мы доказываем структурную половину.

Интеграл взят — дважды¶

Первое взятие интеграла превращает старое неравенство в точное равенство.

Теорема 41.1 (energy_identity_of_energyBalance, 🟢). Энергия подчиняется тождеству E(t₂) = E(t₁) − ∫ D(s) ds — равенством, а не неравенством, через вторую основную теорему анализа. Двухвременное неравенство главы 36 оказывается всего лишь огрублением этого выведенного интегрированием равенства.

Второе взятие интеграла восстанавливает само решение из уравнения.

Теорема 41.2 (isNSSolution_integral_form, 🟢). Решение выражается интегралом своей правой части: u(t,x) = u(0,x) + ∫₀ᵗ (νΔu − ∇p + f − (u·∇)u) ds. Это FTC для функций со значениями в E3 (интеграл Бохнера, банахова версия). Оговорка честна: три гипотезы — что u есть решение, дифференцируемо по времени и правая часть интегрируема — именованы явно; невакуумность проверена на нулевом решении. «Вывести решение — взять интеграл» перестало быть лозунгом и стало теоремой.

Двигатель и его убийца¶

Теперь сингулярный каскад и его смерть.

Теорема 41.3 (no_singularCascade_of_energyInequality, 🟢). При энергетическом неравенстве сингулярных каскадов не существует. Прямое применение уже построенной бюджетной машины (ns_no_infinite_dissipative_cascade, глава 36): бюджет запрещает бесконечный δ-каскад вообще, а сжатый к конечному времени — тем более.

Отсюда — честный суррогат гладкости NoSingularCascade: ни при каком квантовании δ > 0 и ни к какому конечному T лестница не сжимается. Подчеркнём (раскрыто в модуле): это не C^∞, а отсутствие бесконечной равномерно-квантованной диссипативной лестницы.

И герой главы:

Теорема 41.4 (noSingularCascade_of_energyBalance, 🟢). Точечный энергобаланс dE/dt = −D плюс интегрируемость ⟹ точек разрыва каскадного типа нет. «Движение гладко всюду» — на языке программы.

ℝ-предупреждение: почему суррогат именно про равномерность¶

На уровне абстрактных профилей энергии E : ℝ → ℝ (не самих НС-решений — нетривиальные решения вне досягаемости, и это раскрыто) видно, где проходит грань. Равномерный профильный каскад при неотрицательном профиле убивается общей машиной (no_uniform_profileCascade_of_nonneg 🟢).

Но кованый — то есть машинно построенный как контрпример (см. словарь) — каскад на tₙ = 1 − 2⁻ⁿ с профилем max(1−t, 0) — бесконечный, сжатый к T = 1 — не равномерен: его падения 2⁻⁽ⁿ⁺¹⁾ ускользают под всякий δ (cookedProfileCascade_not_uniform 🟢), и бюджет его не берёт.

Это тот же урок, что дала лестница Янга–Миллса: суррогат говорит именно о равномерном квантовании — ровно то, что должен поставить настоящий сертификат регулярности.

Добитие: гейт-закон и самозванец в давлении¶

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

Первое, что вскрылось, — опасность вырождения. Если позволить силе f быть произвольной, предикат «быть решением» вырождается: тотальные операторы mathlib впитывают что угодно, и любое поле оказывается «решением» под подходящую кованую силу (isNSSolution_of_cooked_force 🟢). Значит, гейт — именованное условие-вход, которого требует честная формулировка (см. словарь), — обязан требовать f = 0 — бессиловое решение.

Но и f = 0 мало. Мы построили два самозванца, каждый из которых — бессиловое решение, ломающее баланс.

Первый, dirichletFlow, — это дирихле-мерцание индикаторного поля. Он решает уравнение через junk-производную по времени: функция Дирихле нигде не дифференцируема, а тотальный оператор это проглатывает. Энергобаланс он рушит (dirichletFlow_not_energyBalance 🟢). Урок: гейт f = 0 надо усилить дифференцируемостью по времени.

Второй самозванец оказался главной находкой добития. Возьмём индикаторное давление 2 − y₀ внутри единичного шара. Оно делает поток cookedFlow бессиловым решением, полностью дифференцируемым по времени (cookedFlow_isNSSolution_unforced 🟢), — и всё же ломающим баланс. Junk на этот раз спрятан не в производной по времени, а в градиенте давления на сфере (nsTimeGatedBalanceLaw_refuted 🟢): разрывное давление даёт честный градиент внутри и junk-ноль на границе. Гейта «f = 0 + время» тоже не хватает.

Отсюда — финальный гейт NsSolutionBalanceLaw: f = 0 плюс дифференцируемость и по времени, и по пространству. Оба самозванца им убиты машинно: первый проваливает временной гейт, второй — пространственный. Гейт-класс обитаем — нулевое решение проходит оба гейта и заключение.

Вывод. А сам закон не доказуем: для его вывода нужна теорема о дивергенции на ℝ³, которой в mathlib нет, — и не кован он никаким известным способом. Больше того, его опровержение решило бы открытую проблему Гальди о лиувиллевости стационарного Навье–Стокса. Это ровно тот эпистемический статус, что у twin-узла: не доказуем и не опровержим — а значит, честный кандидат в границы.

Навье-стоксова граница, изъятая (Option A)¶

В одном черновике у первопричины появлялось третье содержательное поле nsBoundary : NsSolutionBalanceLaw, из которого следовали 🟡-теоремы: каскадная гладкость каждого гейт-решения (noSingularCascade_from_firstCause — суррогат, не C^∞), тождество энергии (energyIdentity_from_firstCause) и растяжка — намеренный детектор взрыва на случай опровержения закона (см. словарь) — quarantine_inconsistent_if_nsGatedViolation_exhibited.

При Option A это поле изъято. Структура Step00FirstCause несёт теперь только близнецовую границу causalBoundary (SerialTwinBoundaryObligation); поле nsBoundary, сам NsSolutionBalanceLaw и проекции noSingularCascade_from_firstCause/energyIdentity_from_firstCause — теперь мёртвый код, живущий внутри блока-комментария /- WITHDRAWN -/ (🔵). Ни одна навье-стоксова декларация больше не заражена аксиомой; таинт репозитория (16, все про близнецы) её не включает. Ниже — историческая проекция как запись о том, что было отсоединено.

Особенность, которую надо было назвать честно ещё тогда. У Римана декрет был ровно RH-силы: «закон ⟺ цель» при границе. Здесь такого зеркала не было.

Вывод. Суррогату гладкости хватило бы даже неравенства (noSingularCascade_of_twoTimeInequality 🟢), а гейт-закон утверждал более сильное равенство dE/dt = −D. Обратная импликация неизвестна — то есть декрет, будь он жив, возможно, переплачивал бы за свою цель. Это тот же паттерн, что мы честно отметим у Коллатца: цена может превышать стоимость. При Option A вопрос снят вместе с полем.

Прежний вердикт §13 «пятой границы нет» остаётся в силе для безгейтных и манифестационных форм; nsBoundary выживал как другой кандидат, гейченный, с раскрытой переплатой — но и он при Option A отсоединён.

Философское отступление: турбулентность, каскад Колмогорова и запрет сингулярности¶

Навье–Стокс — это уравнение реальной воды: погоды, крови в сосудах, обтекания крыла, дыма над свечой. И «сингулярность решения», которую мы опровергаем как вечный двигатель, имеет прямой физический образ.

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

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

Вязкость этого не позволяет — это и есть верёвка, δ-диссипация, вытягивающая энергию на каждом переходе к меньшему масштабу; закон энергобаланса говорит, что книги сведены, dE/dt = −D. Водоворот в сливающейся ванне может крутиться быстро, но не бесконечно быстро: трение бесшумно бледит его энергию. Реальные жидкости эмпирически никогда не взрываются именно потому, что вязкость всегда успевает у самых малых масштабов — верёвка всегда выигрывает на дне каскада.

Отдельно стоит наша находка добития — кованое давление. Поток cookedFlow набирает энергию из ничего (размешивается, E = c·t²), и это в точности портрет вечного двигателя: поле, качающее энергию без источника. У настоящего бессилового решения такое невозможно — но тотальные операторы mathlib (junk-производные) впустили самозванца через градиент давления на сфере.

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

Гладкость Навье–Стокса — это, философски, физическая невозможность извлечь бесконечную энергию из вакуума масштабов. Турбулентность — видимое перетягивание каната; регулярность — верёвка, неизменно побеждающая у самого дна.

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

Постскриптум: переход на ℝ³ — интеграл собран на боксе¶

Выше энергия жила абстрактным профилем E : ℝ → ℝ, переданным гипотезой. Модуль Engine/NavierStokesR3Assembly спускает эту абстракцию на землю: он работает на настоящем E3 = EuclideanSpace ℝ (Fin 3) и собирает пространственный интеграл по-настоящему, задействуя теорему mathlib о дивергенции и дифференцирование под интегралом.

Теорема 41.5 (hasDerivAt_kineticEnergy_of_dominated, 🟢). Под честными гейтами доминирования производная кинетической энергии равна dE/dt = ∫ ⟪u, ∂ₜu⟫ — интеграл по всему пространству, а не профиль. «Почему это верно.» Это подлинное дифференцирование под интегралом (hasDerivAt_integral_of_dominated_loc_of_deriv_le mathlib) плюс покомпонентная производная плотности ‖u‖² (HasDerivAt.norm_sq, ровно 2⟪u, ∂ₜu⟫).

Теорема 41.6 (divergence_integral_eq_zero, 🟢). Для C¹-поля с носителем в открытом боксе интеграл дивергенции по всему ℝ³ равен нулю. «Почему это верно.» Здесь теорема о дивергенции задействована по-настоящему (integral_divergence_of_hasFDerivAt_off_countable): шесть граневых интегралов гаснут по носителю — координата грани равна aᵢ или bᵢ, вне открытого бокса, где поле нулевое, — а дополнение замкнутого бокса открыто, и там производная честно ноль.

Отсюда — головной результат, снимающий часть переплаты из предыдущего раздела:

Теорема 41.7 (noSingularCascade_of_r3Assembly, 🟢). Для бокс-носимого C²-решения (сила f = 0) каскадная гладкость выводится зелёно — без декрета nsBoundary. «Почему это верно.» На боксе закон энергобаланса больше не постулируется: energyBalance_of_boxSupported выводит dE/dt = −D из производной под интегралом и трёх интегрирований по частям (давление и конвекция гаснут по бездивергентности, вязкость даёт −энстрофию), а дальше работает уже доказанная бюджетная машина. На этом классе декрет nsBoundary избыточен (nsBoundary_redundant_on_boxClass).

И — доведение «в точности»: три тождества интегрирования по частям больше не входы, а теоремы.

Теорема 41.8 (integral_e3_divergence_eq_zero, 🟢 — несущая лемма). Интеграл E3-дивергенции бокс-носимого C¹-поля по всему ℝ³ равен нулю. «Почему это верно.» Поле переносится с E3 на Fin 3 → ℝ линейной изометрией eL3 (перенос производной — цепное правило ContinuousLinearEquiv.hasFDerivAt + HasFDerivAt.comp, тождество eL3.symm (Pi.single i 1) = e3 i), где живёт зелёная теорема о дивергенции §2. Это тот самый fderiv-мост, которого не хватало.

Теорема 41.9 (pressureKills_of_boxSupported / transportKills_of_boxSupported / viscosityIBP_of_boxSupported, все 🟢). Для бокс-носимого C²-решения ∫ ⟪u, ∇p⟫ = 0, ∫ ⟪u, (u·∇)u⟫ = 0, ∫ ⟪u, Δu⟫ = −∫ ∑ᵢ ‖∂ᵢu‖².

«Почему это верно.» Каждый интегрант — E3-дивергенция подходящего поля (p·u; ½‖u‖²·u; покомпонентно uⱼ·∇uⱼ), сведённая бездивергентностью и цепными тождествами; несущая лемма гасит интеграл в ноль. Вязкостное — покомпонентное интегрирование по частям с перестановкой суммы ∑ⱼ‖∇uⱼ‖² = ∑ᵢ‖∂ᵢu‖². Отсюда killerBundle_of_boxSupported собирает энергобаланс безусловно для бокс-класса: #print axioms показывает стандартную тройку, ни sorry, ни аксиом.

Примечание (что осталось за честной границей). Разряжены ровно три тождества интегрирования по частям; не закрыто иное: сборка живёт на классе финитных по пространству решений, а предельный переход бокс → ℝ³ для лишь убывающих (не финитных) полей в mathlib отсутствует — это внешний разрыв. TimeDomination (локальная мажоранта производной под интегралом) и интервальная интегрируемость диссипации остаются честными аналитическими входами; NoSingularCascade — суррогат, не C^∞; проблема тысячелетия не решается. Но именно «взятие интеграла» на ℝ³ — производная под ним и три интегрирования по частям — теперь доказано, а не предположено.

И одна тихая победа честности: гейт BoxSupportedC2Flow впервые требует гладкости давления (pressDiff, contP') — а значит, самозванец cookedFlow с его разрывным давлением на сфере (канал Ковки-B из «добития» выше) теперь исключён структурно, машинно (cookedFlow_fails_assemblyGates). Движение двигателя внутри ранга гладко всюду — и на ℝ³ мы проверили это на один слой ближе к настоящей воде.

Постскриптум: редукция к одной теореме — и почему двигатель её не закрывает¶

Модуль Engine/NavierStokesClayReduction делает последний честный шаг: кодирует точную постановку Клэя-(A) (данные Шварца, бездивергентность, ∃ гладкое глобальное решение с конечной энергией — через ContDiff ℝ ⊤ и явные оценки убывания) и машинно проверяет логическую редукцию к единственному открытому утверждению.

Теорема 41.10 (clayA_of_regularityTransfer_and_vorticityControl, 🟢). Известная теория переноса (локальное сильное существование Като + продолжение Билла–Като–Майды) плюс единственный критерий GlobalVorticityControl ⟹ Клэй-(A).

«Почему это верно.» Чистый модус поненс: локальное гладкое решение существует; критерий не даёт вихрю взорваться; BKM продлевает решение на всё время. Теорема зелёная и не вакуумная (то есть не выполняется даром, свидетелем-заглушкой): заключение обитаемо (globalSmoothSolution_zero — нулевое поле есть глобальное гладкое решение), а оба входа реально потребляются (убрать любой — не компилируется).

Смысл — изоляция. Всё, что осталось для (A), стянуто в одну именованную теорему GlobalVorticityControl: у всякого гладкого решения шварцевых данных вихрь остаётся ограниченным на каждом конечном промежутке. Это и есть открытое ядро — барьер суперкритичности, уровень Филдсовской медали; доказать его не умеет никто.

Известную теорию переноса (RegularityTransfer, RegularityNecessity) мы называем честно как 🔴-входы: это реальные теоремы литературы, просто не формализованные в mathlib (ярус-1). Карта ярусов: 🟢 доказано (энергобаланс бокс-класса, редукция); известно-но-не-формализовано (Лере, Соболев, BKM); 🔴 открыто (сам критерий вихря).

Примечание (почему прочтение-двигатель не закрывает — машинно). Соблазнительно свести (A) к двигателю, как Коллатца: «опровергнуть = построить вечный двигатель, а значит узнать нельзя». Но у Коллатца этот мост — настоящая теорема (не-останавливающаяся орбита дискретна и буквально есть двигатель на ℕ). У Навье–Стокса он доказуемо рвётся: зелёный суррогат NoSingularCascade убивает лишь равномерно-квантованный каскад, а cookedProfileCascade_not_uniform предъявляет неравномерный каскад, который ускользает. Модуль фиксирует это машинно — greenBudget_strictly_weaker_than_vorticityControl: зелёная двигательная машина строго слабее критерия и его не доказывает. Настоящий взрыв — континуальное явление; дискретный запрет двигателя его не достаёт. Поэтому открытое ядро мы именуем аналитически (вихрь), а не двигательно: честность требует назвать разрыв, а не спрятать его в метафору.

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

← 40. Янг–Миллс · Оглавление · 42. Ходж →