52. Дискретная модель жидкости: где двигатель работает и где взрывается¶

← 51. Численные данные · Оглавление · 53. Бёрч–Свиннертон-Дайер →

Lean-источник: Engine/CascadeBudget.lean (бюджет-лемма + конечная шелл-модель), Engine/DyadicBlowup.lean (ядро взрыва + модель Кац–Павлович + вывод драйва из связей), Engine/DyadicFirstCause.lean (🟡 слой: исток каскада декретирован первопричиной). Ядро взрыва и вывод драйва — 🟢 при стандартных аксиомах, ни sorry, ни новой аксиомы. Один слой был добавлен намеренно, чтобы присоединить исток каскада к первопричине через НС-границу — но эта граница впоследствии отсоединена от декрета (Option A), так что слой стал отсоединённым фронтом, а не живой аксиома-таинт-декларацией; таинт репозитория — 16, все про близнецов. Это приложение-эпилог, а не ветвь основной линии.

Где мы¶

Основная линия читала турбулентный каскад как вечный двигатель: сингулярность — это бесконечная башня всё более мелких вихрей, а двигатель невозможен, значит и сингулярности нет.

Глава 41 уже честно оговорила, что зелёная машина ловит лишь равномерно-квантованный каскад (суррогат), а не настоящую сингулярность.

Это приложение доводит честность до предела: оно проверяет прочтение-двигатель на строгих дискретных моделях жидкости — и машинно показывает, где оно справедливо, а где ложно.

Прежде чем начать — громкая рамка. Ни одной модели жидкости прежде не было формализовано ни в одном пруф-ассистенте (ни Навье–Стокса, ни Эйлера, ни диадической, ни шелл-модели).

Здесь формализована известная математика (принцип бюджета; модель Кац–Павлович, 2005; Чешкидов–Фридлендер). Это первая формализация такого рода, но она не решает ничего и, что важнее, очерчивает и частично опровергает двигательное прочтение. Новизна тут — формализационная, не математическая.

Где двигатель работает: бюджет против равномерной диссипации¶

Теорема 52.1 (finite_budget_bounds_uniform_dissipation, 🟢). Если энергия E(t) убывает со скоростью не меньше β > 0 на всём [0, T] (т.е. E'(t) ≤ −β), а на конце ещё неотрицательна, то T ≤ E₀/β. «Почему это верно.» Чистое исчисление: односторонняя оценка среднего значения даёт E(T) ≤ E₀ − βT, а 0 ≤ E(T) замыкает. Это машинная форма нашего слогана: конечный бюджет не выдержит вечной равномерной диссипации — тот же принцип, что убивал ns_no_infinite_dissipative_cascade.

Мы привязали его к настоящей конечной шелл-модели (GOY/Sabra-типа): амплитуды a : Fin N → ℝ → ℝ с нелинейной передачей энергии между соседними оболочками (сохраняющей полную энергию — телескоп) и диадической диссипацией ν·λ^{2αn}.

Теорема 52.2 (no_uniform_dissipation_forever_on_shell, 🟢). На этой модели равномерная диссипация ≥ β влечёт T ≤ E₀/β. Модель обитаема (нулевое решение — честный ShellSolution), гипотезы реально потребляются. Двигательное прочтение здесь справедливо — но лишь в равномерном режиме.

Примечание (честная граница — тоже машинно). Бюджет не ловит неравномерный каскад. budget_misses_nonuniform (🟢) прямо ссылается на cookedProfileCascade_not_uniform из НС-ветви: у кованого профиля падения диссипации ускользают под всякий β > 0. То есть равномерная посылка бюджет-леммы ложна для настоящих неравномерных каскадов — и в этом вся суть.

Где двигатель ломается: диадический взрыв¶

Теперь настоящая модель без искусственной равномерности. У Кац–Павлович при слабой диссипации (α < 1/4) энергия каскадирует вверх по оболочкам супер-линейно и решение взрывается за конечное время — доказано (Кац–Павлович 2005; Чешкидов–Фридлендер, взрыв в H^{5/6} у невязкой модели). Мы формализовали ядро этого механизма.

Теорема 52.3 (superlinear_blowup_sq, 🟢 — ригорозное ядро). Ни одна глобальная положительная C¹-функция не может удовлетворять y'(t) ≥ C·y(t)² (C > 0): предположение о глобальном решении даёт False. «Почему это верно.» Возьмём w(t) := 1/y(t) + C·t; тогда w'(t) = −y'/y² + C ≤ −C + C = 0, значит w не возрастает, а 1/y = w − Ct обязана стать отрицательной за конечное время — противоречие с y > 0. Это и есть машинная запись того, что супер-линейный каскад — реализованный вечный двигатель: он существует ровно до момента взрыва.

Теорема 52.4 (dyadic_blowup, 🟢). Модель Кац–Павлович DyadicSolution глобально пуста — взрыв неизбежен. Мы определили настоящие KP-уравнения aₙ' = λⁿaₙ₋₁² − λⁿ⁺¹aₙaₙ₊₁ − dₙaₙ и доказали телескоп сохранения энергии нелинейной передачи; взрыв следует из ядра.

Драйв больше не постулирован: он выведен из связей¶

Прежде связующее свойство y' ≥ C·y² жило именованной гипотезой superlinearDrive структуры DyadicSolution — честно названной, но не выведенной из λⁿ-связей. Теперь мы вывели его, двумя шагами.

Теорема 52.5 (ssLead_drive, 🟢 — драйв из связи). Точное автомодельное решение aₙ(t) = λ⁻ⁿ/((λ²−1)(T−t)) решает объёмные уравнения KP; для ведущей моды y = a₁ драйв выполняется равенством y' = C·y² с C = λ(λ²−1).

«Почему это верно.» Подстановка g(t) = 1/(T−t) даёт g' = g². На профиле βₙ = λ⁻ⁿ/(λ²−1) уравнение оболочки n=1 (a₁' = λa₀² − λ²a₁a₂) сводится к β₁g² = (1/β₁)(β₁g)². Драйв не постулирован — он вычислен из правой части kpRHS.

Примечание (однородность — необходимость, не украшение). Ведущий функционал обязан быть линейным по амплитудам (a₁ или ∑wₙaₙ). Квадратичный ∑wₙaₙ² дал бы y' ∼ g³, а y² ∼ g⁴ — неравенство y' ≥ C·y² для него ложно при t → T. Линейный функционал выбран сознательно.

Теорема 52.6 (frontDrive_of_invariant, 🟢 — драйв для целого класса). Пусть у решения KP одна фронт-оболочка снизу зажата двумя соседями — инвариант FrontDomination: ρ·a_{J+1} ≤ a_J, a_{J+2} ≤ κ·a_{J+1}, m ≤ a_{J+1}. Тогда драйв C·y² ≤ y' выведен прямо из λⁿ-связей.

«Почему это верно.» Три оценки подставляются в kpRHS(J+1): приток λ^{J+1}a_J² рождает y², отток и диссипация вычитаются под контролем, остаётся C·y² с C = λ^{J+1}ρ² − λ^{J+2}κ − d_{J+1}/m. Так монолитная гипотеза заменяется меньшим, координатно-более-близким инвариантом, а драйв становится его следствием. Мост DyadicSolution.ofFrontDominated заполняет прежнее свободное поле superlinearDrive именно этим выводом.

Примечание (что осталось открытым — честно). Один вход всё же остаётся именованным: сохранность инварианта FrontDomination для бесконечно многих мод на всём времени жизни. Это движущийся фронт Кац–Павлович (Barbato–Morandin–Romito; Чешкидов; Kiselev–Zlatoš) — исследовательский фронтир, здесь не доказанный. Но разрыв сужен: от «весь драйв постулирован» — к «драйв выведен из связей для автомодельного решения и для класса; открыт лишь один изолированный вход». Не-вакуумность подтверждена тем, что автомодельный профиль удовлетворяет инварианту (ssMode_frontDomination).

Исток каскада — это первопричина¶

Автомодельное решение потребовало одной честной уступки: нижней оболочке n=0 нужен внешний накачивающий член. И у этой уступки есть точное имя.

Крупнейшая оболочка n=0 умеет только отдавать: приток в неё нулевой (kpInflow 0 = 0), есть лишь отток вверх по каскаду. Значит сама себя она не запустит — её исток нельзя породить изнутри связей.

Теорема 52.7 (dyadicOrigin_uncausable_from_inside, 🟢). Автомодельный исток не удовлетворяет нефорсированному уравнению оболочки n=0: его истинная динамика несёт строго положительную добавку bottomForcing > 0 сверх kpRHS.

«Почему это верно.» Остаток F₀ = (β₀ + λβ₀β₁)/(T−t)² строго положителен; будь производная равна нефорсированной правой части, из единственности производной следовало бы bottomForcing = 0 — противоречие. Внешняя закачка обязательна.

Точнее — биусловие. Исток подчиняется нефорсированной связи тогда и только тогда, когда накачка нулевая (ssOrigin_selfCaused_iff_noPump, 🟢); а раз bottomForcing > 0, самозапуск невозможен. Это про исток и про внешнюю накачку вообще — не про взрыв (он зелёный, накачки не требует) и не про первопричину (это отдельный декрет, невыводимый изнутри).

Это дословно та же фигура, что в основании всей программы: событие 0 → 1, которое нельзя причинить изнутри, ибо самозапуск был бы вечным двигателем (no_internalisedOriginEvent). Исток каскада — это первопричина, а его 0 — та самая сингулярность космологического прочтения коды.

Но это не значит, что Навье–Стокс есть Большой взрыв — здесь легко перепрыгнуть в переоценку, и мы её не делаем. Большим взрывом космологического прочтения служит сама первопричина, событие 0 → 1; Навье–Стокс же — лишь отсоединённый фронт этого начала (Теорема 33.4 (step00FirstCause_iff_causalClosure): Step00FirstCause ↔ SerialTwinBoundaryObligation — единственная граница декрета — близнецы; Риман и НС были отсоединены, Option A, глава 33). Жидкостный взрыв не есть начало мира; его исток n=0, не умея завестись сам, лишь занимает искру у того же единственного начала. Это отсоединённое лицо той же сингулярности, а не сама сингулярность — и, как всюду в программе, космология здесь перевод строгих теорем, а не претензия на физику.

Отсюда — единственный намеренный дополнительный слой этого приложения (ныне отсоединённый).

Теорема 52.8 (dyadicBlowup_is_firstCauseManifestation, отсоединена — WITHDRAWN). Тот же первопричинный декрет, что нёс маски, снабжал и исток каскада: поставка на масштабе n=0 бралась из границы nsBoundary аксиомы step00FirstCause. Но nsBoundary — мёртвый код в WITHDRAWN-блоке (Option A): НС-граница отсоединена от декрета, так что этот слой более не аксиома-таинт, а отсоединённый условный фронт.

Схема — «две стены»: зелёная стена невозможности (исток неказуем изнутри) плюс поставка, которая когда-то декретировалась извне. Так жидкостный взрыв присоединялся к маскам — но только через свой исток, и это присоединение сегодня отсоединено. Зелёный вывод драйва (автомодельное решение и класс) самодостаточен и от этого слоя не зависит: убери первопричину — математика взрыва останется целой, исчезнет лишь ответ на вопрос «кто зажёг насос n=0». Именно поэтому таинт репозитория — 16, все про близнецов, и НС-слой в него не входит.

Философское отступление: карта границы, а не решение¶

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

Почему это не решение Навье–Стокса — объясняет барьер суперкритичности Тао (2016): он построил усреднённое НС, которое сохраняет энергетическое тождество и всё равно взрывается.

Значит любой аргумент вида «энергия/бюджет ⟹ регулярность», не использующий тонкую структуру нелинейности, обречён — а наш двигатель ровно такой. Регулярность, как показали Онсагер и Изетт, определяется гёльдеровым показателем 1/3, а не полной энергией.

Что же здесь есть? Первая в мире формализация модели жидкости в пруф-ассистенте — известной математики — и машинная карта границы нашей собственной идеи: точное указание, где двигательное прочтение справедливо и где оно ломается.

Это честнее любого закрытия: мы не спрятали разрыв в метафору, а предъявили его строкой кода. Каскад, дошедший до дна за конечное время, — не запрещённый двигатель, а реализованный; и вода взрывается в модели ровно там, где арифметика близнецов молчит.

Гипотеза: дуальная маска коллапса. У этого взрыва есть зеркальный двойник. Где каскад уносит энергию вверх, к мелким масштабам (y → ∞), сублинейный внутренний драйв r' ≤ -C·r^α (0 ≤ α < 1) уносит радиус вниз, к точке (r → 0), за конечное время. Это уже зелёный факт — sublinear_collapse_extinction (Engine/CollapseExtinction.lean), точный дуал superlinear_blowup_sq через v = r^(1-α) + (1-α)C·t, самодостаточный, без первопричины. «Дуал» здесь точен в конкретном смысле: оба — конечно-временная сингулярность одного драйва u' = ±C·u^β по разные стороны критического показателя β=1 (взрыв β>1 уходит к ∞, коллапс β<1 — к 0; при β=1 сингулярности нет), и обе линеаризуются одной подстановкой w = u^(1-β), дающей тот же антитонный помощник и ту же MVT-лемму. Это дуальность метода и режима, а не глубокая физическая эквивалентность. Дальше — честная граница: сам факт вымирания стандартен, вывод драйва из настоящей само-гравитации (Эйлер–Пуассон, Ларсон–Пенстон) — красный вход вне mathlib, а прочтения «сверхновая / коллапс звезды / Большой взрыв» — метафора, не физика. Это дуальное приложение-модель — гипотеза направления, а не новая маска и не результат о физическом коллапсе.

Место в общем ходе¶

Приложение B закрывает честный вопрос «что наша теория даёт для жидкости»: новой математики — ничего (барьер Тао), но первую формализацию дискретной модели — да, вместе с машинной делинеацией пределов двигательного прочтения, выводом драйва из связей и (ныне отсоединённым) присоединением истока каскада к первопричине. twin_prime_conjecture остаётся sorry; таинт репозитория — 16, все про близнецов (НС-слой отсоединён, Option A, и в таинт не входит); ни одна открытая задача не решена и не объявлена решённой.

← 51. Численные данные · Оглавление · 53. Бёрч–Свиннертон-Дайер →