Перейти к содержанию

36. Навье–Стокс: уравнение и честные интегралы

← 35. P/NP: локальный узел · Оглавление · 37. Римановы фронты →

Lean: Engine/NavierStokes.lean (само уравнение, mathlib-анализ; всё доказанное — 🟢 при стандартных аксиомах, без step00), NS-часть Engine/DissipativeCascade.lean (§2: ℝ-предупреждение real_positive_work_not_wellfounded; квантизация no_infinite_uniform_dissipative_cascade). Проза-контекст: 24. Декомпозиция boundary, раздел «Навье–Стокс: само уравнение + честность интегралов».

Почему в репозитории о простых числах вообще живёт гидродинамика? Потому что DissipativeCascade — единый blueprint трёх веток (Step00, Риман, Навье–Стокс) с одним лозунгом: дефект не исчезает; не закрылся — плати. Для близнецов «платой» служит регенерация носителя, для Римана — платная динамика двигателя, а для Навье–Стокса плата буквальна: вязкая диссипация энергии.

Но чтобы аналогия не осталась метафорой, нужно предъявить само уравнение — не абстрактный интерфейс «какой-то диссипативной системы», а классическую сильную форму НС в терминах mathlib. Эта глава — о том, что из этого удалось сделать честно, и где проходит граница.

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

Само уравнение

Engine/NavierStokes.lean работает в E3 := EuclideanSpace ℝ (Fin 3) и собирает дифференциальные операторы из голого fderiv: дивергенция NSdiv (след Якобиана, \(\sum_i \partial_i u_i\)), векторный лапласиан vectorLaplacian (\(\sum_i \partial_i(\partial_i u)\)), конвективный член convectiveTerm (производная \(u\) вдоль самого \(u\), т.е. \((u\cdot\nabla)u\)). Из них — предикат.

Определение 36.1 (IsNSSolution). Для вязкости \(\nu\), внешней силы \(f\), поля скоростей \(u\) и давления \(p\)

\[\texttt{IsNSSolution}\ \nu\ f\ u\ p \;:=\; \Bigl[\partial_t u + (u\cdot\nabla)u = \nu\,\Delta u - \nabla p + f\Bigr] \;\wedge\; \bigl[\mathrm{div}\,u = 0\bigr]. \tag{36.1}\]

Это несжимаемые уравнения Навье–Стокса в классической сильной форме — поле скоростей u : ℝ → E3 → E3, давление p : ℝ → E3 → ℝ, вязкость ν, внешняя сила f. Никаких слабых решений и распределений: сильная форма выбрана сознательно, чтобы предикат читался глазами.

Первый обязательный вопрос к любому такому предикату — не пуст ли он. Ответ машинный.

Теорема 36.2 (zero_is_NSSolution). \(\texttt{IsNSSolution}\ \nu\ 0\ 0\ 0\) для любого \(\nu\in\mathbb{R}\): нулевое поле с нулевым давлением и без силы есть решение при любой вязкости. 🟢

Скромно, но это ровно та прививка от вакуумности — ситуации, когда предикат выполняется даром, свидетелем-заглушкой (см. словарь), — которой не хватало близнецовой ветке до починки №1: предикат обитаем, уравнение настоящее.

Честность Бохнера: тихий ноль

Энергетика задаётся интегралами Бохнера по объёму: кинетическая энергия kineticEnergy \(= \tfrac12\int\|u\|^2\) и скорость диссипации dissipationRate \(= \nu\int\sum_i\|\partial_i u\|^2\) (энстрофийная форма); неотрицательность обеих — kineticEnergy_nonneg и dissipationRate_nonneg 🟢.

Здесь спрятана ловушка, и репозиторий вскрывает её машинно. Интеграл Бохнера в mathlib молча равен нулю на неинтегрируемой функции (MeasureTheory.integral_undef).

Теорема 36.3 (kineticEnergy_of_not_integrable). Если \(\|u\|^2\) не интегрируемо (нет предиката FiniteKineticEnergy; парный предикат для градиентов — FiniteEnstrophy), то \(\texttt{kineticEnergy}\ u = 0\). 🟢 Равенство kineticEnergy u = 0 тем самым может означать не «энергия нулевая», а «энергия бесконечна или не определена». «Нулевая энергия» неинтегрируемого поля — артефакт определения, не физика.

Для контраста — честный ноль нулевого поля.

Теорема 36.4 (kineticEnergy_zero_field). \(\texttt{kineticEnergy}\ (\lambda x.\,0) = 0\). 🟢

Мораль та же, что и в эпизодах вакуумности 24: всякое энергетическое утверждение обязано идти в паре с именованной интегрируемостью — иначе оно хрупко-вакуумно. Это здесь не пожелание, а доказанное предупреждение.

Сужение входа: от монолита к точечному балансу

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

\[E(u(t_2)) + \int_{t_1}^{t_2} D(u(s))\,ds \le E(u(t_1)). \tag{36.2}\]

Сессия его не доказала — она его сузила.

Вся аналитика сжата в один точечный вход EnergyBalanceLaw: HasDerivAt-тождество \(dE/dt = -D(t)\), классический энергобаланс гладкого быстро убывающего решения (конвекция и давление не работают благодаря \(\mathrm{div}\,u=0\)).

Глюа от него доказана.

Теорема 36.5 (twoTimeEnergyInequality_of_energyBalance). Если выполнен точечный баланс \(\texttt{EnergyBalanceLaw}\ \nu\ u\) и диссипация \(s\mapsto D(u(s))\) интервально интегрируема на всех \([t_1,t_2]\), то верно \((36.2)\): \(\texttt{TwoTimeEnergyInequality}\ \nu\ u\). 🟢

Доказательство — точечный баланс плюс интегрируемость диссипации дают двухвременное неравенство (на деле равенство) через FTC (intervalIntegral.integral_eq_sub_of_hasDerivAt). Вход стал строго у́же: не интегральное неравенство по всем парам времён, а одно дифференциальное тождество.

Цепь до каскада

Зачем всё это бюджетной программе: DissipativeStage ν u δ t₁ t₂ — временной интервал, на котором накоплено диссипации не меньше \(\delta\).

Теорема 36.6 (ns_no_infinite_dissipative_cascade). Пусть \(\delta>0\) и выполнено двухвременное неравенство \(\texttt{TwoTimeEnergyInequality}\ \nu\ u\). Тогда не существует последовательности времён \((t_k)_{k\in\mathbb{N}}\) с \(\texttt{DissipativeStage}\ \nu\ u\ \delta\ t_k\ t_{k+1}\) для всех \(k\): бесконечной последовательности \(\delta\)-диссипирующих шагов не существует. 🟢 (условно на входе-неравенстве) — накопленная плата превысила бы стартовую энергию \(E(u(t_0))\).

Это прямое применение no_infinite_uniform_dissipative_cascade из DissipativeCascade — квантизация в действии на настоящем уравнении, а не на интерфейсе. Полная цепь от узкого входа склеивает Теорему 36.5 (twoTimeEnergyInequality_of_energyBalance) с Теоремой 36.6 (ns_no_infinite_dissipative_cascade).

Теорема 36.7 (ns_no_infinite_dissipative_cascade_of_balance). Пусть \(\delta>0\), выполнен \(\texttt{EnergyBalanceLaw}\ \nu\ u\) и диссипация интервально интегрируема. Тогда не существует последовательности \((t_k)\) с \(\texttt{DissipativeStage}\ \nu\ u\ \delta\ t_k\ t_{k+1}\) для всех \(k\): EnergyBalanceLaw + интегрируемость ⟹ нет бесконечного \(\delta\)-каскада. 🟢

«Нет бесконечного каскада к мелким масштабам при квантованной диссипации» — по форме ровно тот сертификат, которого требует регулярность; по содержанию — см. границу ниже.

ℝ-предупреждение: почему нужна квантизация

Слово «квантованной» выше несёт всю нагрузку, и это тоже зафиксировано машинно.

Теорема 36.8 (real_positive_work_not_wellfounded). Существует \(a:\mathbb{N}\to\mathbb{R}\) такое, что \(a_{n+1}<a_n\), \(a_n>0\) и \(a_n-a_{n+1}>0\) для всех \(n\) (DissipativeCascade, §2): ℝ-последовательность со строго положительной работой на каждом шаге, но конечным суммарным спадом — банальное \(a_n = 1/2^n\). 🟢

Для ℕ-движка близнецов Total y + Work ≤ Total x при 0 < Work даёт строгий спуск и well-foundedness даром; для ℝ строго положительная работа не запрещает бесконечный ряд убываний. Потому НС-аналогия с ℕ-движком — только структурная: конечность каскада покупается равномерной нижней гранью \(\delta > 0\), а не положительностью как таковой.

Вопрос «откуда взять \(\delta\) для реального решения» — аналитика, не структура, и он здесь открыт.

Честная граница

Что не доказано — явно, без приукрашивания:

  • 🔴 Существование и регулярность решений НС — проблема тысячелетия. Формализовано уравнение и бюджетный каркас над ним; ни одного шага к самой регулярности здесь нет. Каскадные теоремы говорят «если решение удовлетворяет балансу, то нет бесконечного равномерного каскада» — посылку для нетривиального решения никто не предъявил.
  • 🔴 EnergyBalanceLaw — именованный вход. Его честная стоимость: дифференцирование под интегралом (hasDerivAt_integral_of_dominated_loc_of_deriv_le) + интегрирование по частям + \(\mathrm{div}\,u=0\); причём теорема о дивергенции в mathlib существует лишь в box-форме (integral_divergence_of_hasFDerivAt_off_countable), и предельный переход от боксов к \(\mathbb{R}^3\) не формализован. Вход узкий и классический, но он вход.
  • Красная линия: файл не упоминает простые числа, и никакой перенос НС-результатов на близнецов не подразумевается. Единственная общность — blueprint DissipativeCascade.

Итог раздела. Всё перечисленное доказанным (Теорема 36.2 (zero_is_NSSolution), Теорема 36.3 (kineticEnergy_of_not_integrable), Теорема 36.5 (twoTimeEnergyInequality_of_energyBalance), обе каскадные теоремы 36.6–36.7, Теорема 36.8 (real_positive_work_not_wellfounded)) — 🟢: стандартные аксиомы Lean, без step00FirstCause, без sorry.

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

Постскриптум (глава 40): два спасения одного предупреждения

ℝ-контрпример предупреждения §2 каскада — последовательность (1/2)^n с положительной работой, но без конечности — это буквально безмассовая лестница Янга–Миллса (глава 40, GaplessLadder/cookedLadder).

Спасения разошлись. НС спасается δ-квантованием диссипации (no_infinite_uniform_dissipative_cascade — и no_uniformlyDissipative_ladder 🟢 главы 40 показывает, что равномерно диссипативная лестница невозможна). Янг–Миллс — ранговым квантованием спектра (massGap_of_quantizationLaw 🟢: лестница не равномерно диссипативна — cookedLadder_not_uniformlyDissipative — и убивается только ℕ-рангом через EPMI).

Общий корень обеих физических ветвей — невозможность вечного двигателя; сертификаты различны и оба честно именованы.

Постскриптум (глава 41): интеграл взят

FTC-глюа §5ter поднята до тождества.

Теорема 36.9 (energy_identity_of_energyBalance). При \(\texttt{EnergyBalanceLaw}\ \nu\ u\) и интервальной интегрируемости диссипации для всех \(t_1,t_2\) выполнено \(E(u(t_2)) = E(u(t_1)) - \int_{t_1}^{t_2} D(u(s))\,ds\). 🟢 То есть E(t₂) = E(t₁) − ∫D равенством (двухвременное неравенство \((36.2)\) этой главы — огрубление).

Решение выведено интегрированием уравнения.

Теорема 36.10 (isNSSolution_integral_form). Если \(\texttt{IsNSSolution}\ \nu\ f\ u\ p\), каждое \(s\mapsto u(s)(x)\) дифференцируемо и правая часть интервально интегрируема, то для всех \(t,x\)

\[u(t)(x) = u(0)(x) + \int_0^t \bigl(\nu\,\Delta u - \nabla p + f - (u\cdot\nabla)u\bigr)(s)(x)\,ds. \tag{36.3}\]

🟢 (mild-форма, банахово-значный FTC).

Сингулярность как вечный двигатель (сингулярный каскад) и трилемма пятой границы декрета — обязательная трёхветочная проверка кандидата в границы перед намеренным принятием закона аксиомой (см. словарь) — в главе 41_NSSmoothness.md. EnergyBalanceLaw остаётся именованным 🔴-входом этой главы.

← 35. P/NP: локальный узел · Оглавление · 37. Римановы фронты →