Янг–Миллс: безмассовый спектр как вечный двигатель¶
← 39. P/NP: оплата сертификатов · Оглавление · 41. Навье–Стокс: гладкость →
Lean-источник:
Engine/YangMillsFront.lean— зелёная цепь и трилемма, всё 🟢;Engine/CausalClosureAxiom.lean§12 — ЯМ-язык декрета. Обозначения статуса: 🟢 — доказано при стандартных аксиомах; 🟡 — доказано условно на аксиомуstep00FirstCause; 🔴 — открытый вход.
Прочтение: безмассовость — это вечный двигатель¶
Задача Янга–Миллса о массовой щели просит доказать, что у квантовой калибровочной теории есть щель — минимальная положительная цена возбуждения над вакуумом. Отрицание щели — безмассовость: возбуждения сколь угодно малой положительной энергии.
И вот наблюдение, вокруг которого построена вся глава: безмассовый спектр — это вечный двигатель. Если над вакуумом есть возбуждения любой, сколь угодно малой энергии, то из вакуума можно черпать работу без нижнего предела — бесконечная башня всё более дешёвых мод, бесконечная перекачка из «ничего».
Существование щели — это ровно запрет такой башни.
Сразу очертим честную границу, как в главе 36 про Навье–Стокса: проблему тысячелетия мы не решаем и не объявляем решённой. В mathlib нет калибровочной теории — ни гамильтониана, ни спектра настоящей КТП.
Мы работаем с абстрактной спектральной моделью и доказываем ту половину, что от конкретной теории не зависит.
Спектр, щель, безмассовость¶
Абстрагируемся до необходимого. Спектральная модель SpectralModel — это множество уровней энергии Energy : Set ℝ с вакуумом 0 и неотрицательностью (никакого содержания Янга–Миллса сверх будущей инстанциации — раскрыто в докстринге).
На ней два понятия. Масс-щель MassGap S — существование Δ > 0 ниже всех ненулевых уровней. Безмассовость Gapless S — наличие уровней сколь угодно малой положительной энергии. Они — точные отрицания друг друга:
Теорема 40.1 (not_massGap_iff_gapless, 🟢). Отсутствие щели эквивалентно безмассовости (и, что
приятно, без всякого выбора): \(\neg\,\mathrm{MassGap}(S) \iff \mathrm{Gapless}(S)\), где \(\mathrm{MassGap}(S) := \exists\,\Delta>0,\ \forall E\in S.\mathrm{Energy},\ E\neq 0 \Rightarrow \Delta \le E\) и \(\mathrm{Gapless}(S) := \forall \varepsilon>0,\ \exists E\in S.\mathrm{Energy},\ 0<E<\varepsilon\).
Двигатель: лестница безмассовости¶
Что именно делает безмассовость двигателем? Из неё строится лестница — halving-цепочка уровней,
на каждом шаге падающая не меньше чем вдвое: 2·E(n+1) ≤ E(n), все члены положительны. Это не что
иное, как ℝ-контрпример real_positive_work_not_wellfounded из каскадного предупреждения главы 36:
положительная работа без нижнего предела, бесконечный мультипликативный спуск в вещественных числах,
где ацикличность не работает.
Теорема 40.2 (gapless_iff_nonempty_ladder, 🟢). Безмассовость эквивалентна существованию лестницы: \(\mathrm{Gapless}(S) \iff\) тип лестниц \(\mathrm{GaplessLadder}(S)\) непуст, где лестница — это последовательность \(E:\mathbb{N}\to\mathbb{R}\) с \(E(n)\in S.\mathrm{Energy}\), \(E(n)>0\) и \(2\cdot E(n+1)\le E(n)\) для всех \(n\).
Прямое направление строит лестницу выбором — это зеркало экстракции нуля у Римана; обратное показывает,
что лестница опровергает любой кандидат-Δ (геометрической мажорантой). Лестница и есть двигатель, и
пока она живёт в вещественных числах, ацикличность её не берёт.
Закон квантования и герой: квантованность ⟹ щель¶
Двигатель убивается ровно тогда, когда лестницу удаётся отразить в натуральный ряд. Это и есть физический вход ветви — закон квантования.
Определение 40.3 (QuantizationLaw, 🔴 — вход, паттерн EnergyBalanceLaw). Каждое положительное
состояние несёт натуральный ранг, и мультипликативный спуск энергии отражается в строгий спуск
ранга: \(\mathrm{QuantizationLaw}(S) := \exists\,\mathrm{rank} : \mathrm{PositiveState}(S)\to\mathbb{N},\ \forall x,y,\ 2\cdot(y:\mathbb{R})\le(x:\mathbb{R}) \Rightarrow \mathrm{rank}(y) < \mathrm{rank}(x)\).
Как только это есть, лестница из вещественной становится натуральной — и обрывается:
Теорема 40.4 (no_quantizedLadder, 🟢). Квантованной лестницы не существует: \(\mathrm{QuantizationLaw}(S) \wedge \mathrm{GaplessLadder}(S) \Rightarrow \bot\). Она была бы бесконечной
строго убывающей цепью натуральных рангов — то есть вечным двигателем Евклида, — а его убивает корень
всего репозитория no_infinite_descent (глава 01). Отметим честно инвертированную асимметрию: убийца
здесь — чистая вполне-фундированность натурального ряда, и мы не подмешивали фальшивой гипотезы
«двигателей нет» ради красоты.
Теорема 40.5 (massGap_of_quantizationLaw, 🟢 — герой главы). Квантованность ⟹ масс-щель: \(\mathrm{QuantizationLaw}(S) \Rightarrow \mathrm{MassGap}(S)\). Нет щели →
есть безмассовость → строится лестница → квантование делает её натуральным спуском → EPMI-противоречие.
Почему границы Янг–Миллса у декрета нет¶
Как и с P/NP, возникает соблазн добавить границу Янг–Миллса к первопричине. И снова — нет, машинно. Причина глубже, чем у P/NP, и вскрывается одной теоремой.
Теорема 40.6 (quantizationLaw_iff_massGap, 🟢). Для каждой модели закон квантования эквивалентен
наличию щели — зелёно и без всякой границы: \(\mathrm{QuantizationLaw}(S) \iff \mathrm{MassGap}(S)\).
Это форма осуждённого моста (offCriticalBridge_iff_RH), а не честного римановского зеркала. У Римана эквивалентность «закон ⟺ цель» достигалась только при границе; здесь она зелёная сама по себе.
А значит, декретировать закон квантования для модели значило бы декретировать её щель дословно — переименовать цель, а не добавить причину. Трилемма — обязательная трёхчастная проверка кандидата в границы (см. словарь) — подтверждает это со всех сторон:
- универсальная форма закона опровержима — кованая (то есть машинно построенная как контрпример) безмассовая модель
{0} ∪ {2⁻ⁿ}несёт явную лестницуcookedLadder, и декрет взорвал бы карантин; - экзистенциальная уже доказана — кованая щелевая модель
{0,1}, декрет был бы пустым; - манифестационная форма несовместима с уже принятой границей.
Последний пункт стоит выделить — в нём точная асимметрия с Риманом. Off-critical нуль зелёно непредъявим (предъявить его значило бы опровергнуть RH), и потому у Римана манифестационный закон был честной второй границей (впоследствии отсоединённой от декрета, Option A).
А кованая безмассовая лестница предъявлена конструкцией — и потому тот же приём здесь взрывает карантин: ymManifestationLaw_refutes_boundary 🟢.
Вывод. Тот же, что в P/NP: честного декретного поля нет, недостающее — не пропозиция, а data anchor, построенный спектр или гамильтониан, которого в mathlib нет.
Раскол по масштабам и §12¶
Единственное 🟡-содержание ветви — то, что декрет утверждает сам, на своём масштабе. При A ≤ 4 поставка отклонений — то, чем отклонение «расплачивается» (см. словарь), — реальна (smallScale_deviationSupply 🟢, пятиадическая цепь — объект манифестации, не пустая форма).
А при декретном A ≥ 5 поставки нет ни на одном пороге (decreedScale_no_deviationSupply 🟡): мир первопричины гэпнут в языке поставок — в нём нет бесконечной башни сколь угодно дешёвых возбуждений.
Мы намеренно не добавили фальшивого 🟡 «масс-гэп ранго-мира»: натуральная щель ранго-мира тривиально зелёная. Растяжка — намеренный детектор взрыва (см. словарь) — quarantine_inconsistent_if_supply_at_every_scale 🟡 держит точку взрыва видимой.
Мост к Навье–Стоксу: два спасения одного предупреждения¶
Контрпример каскадного предупреждения — (1/2)^n, положительная работа без конечности — это буквально лестница Янга–Миллса. Но спасают от него две ветви по-разному, и это стоит увидеть рядом.
Навье–Стокс спасается δ-квантованием диссипации: равномерно-диссипативная лестница невозможна (no_uniformlyDissipative_ladder 🟢). Однако реальная лестница (1/2)^n не равномерно диссипативна — её шаги убывают под всякий δ (cookedLadder_not_uniformlyDissipative 🟢), — и потому НС-сертификат её не убивает. Убивает её только ранговое квантование через EPMI.
Корень у обеих ветвей один — невозможность вечного двигателя; но сертификаты разные: у НС — энергобаланс с δ-диссипацией, у ЯМ — квантованность спектра.
Янг–Миллс за тем же горизонтом¶
У стены, о которую разбиваются внутренние решения Коллатца и P/NP (глава 56), есть и спектральный склон — эпистемический комплемент ветви собран в Engine/YangMillsEpistemic.lean.
«Решить Янг–Миллса изнутри» на нашем языке значило бы самообосновать закон квантования: нести сам per-model закон (поле ground) и вместе с ним опровержение щели, добытое из-за собственного горизонта (поле beyondOwnHorizon).
Такая связка (InternalisedYMGround) самоуничтожается: no_internalisedYMGround 🟢, откуда ymCause_unknowable 🟢 — зеркало collatzCause_unknowable и pnpCause_unknowable, — и потому «узнать нельзя изнутри» и здесь теорема, а не лозунг. Изнутри спектральной модели закон квантования не самообосновать: попытка стоит ровно вечного двигателя.
Чем оплачено противоречие — конструкцией, и у Янга–Миллса она нагляднее, чем где-либо: опровержение щели не пассивно, оно предъявляет объект. Из отсутствия щели строится halving-лестница (точная характеризация — not_massGap_iff_nonempty_ladder 🟢), а лестница сама по себе — подлинный вечный двигатель на вещественных числах: not_massGap_carries_real_engine 🟢, свидетель — сама последовательность уровней, без единого False.elim.
На ℝ такой двигатель законен (perpetualEngine_on_real 🟢) — континуум стены не ставит. Стена возникает, лишь когда закон квантования переводит энергию в натуральный ранг: композиция «ранг ∘ лестница» становится бесконечным ℕ-спуском (quantizedLadder_carries_perpetual_engine 🟢) и сгорает об no_perpetual_engine_on_nat — второй маршрут quantizedLadder_impossible_via_engine 🟢.
Оговорка обязательна: пара «закон + лестница» в репозитории совместно опровергнута (no_quantizedLadder), так что логически этот носитель — переупаковка убийцы; подлинность здесь — свойство терма-свидетеля, а не антецедента, который у Коллатца оставался открытым.
И третья створка развилки ym_no_internal_decision_without_engine 🟢 — фирменная особенность именно этой ветви. Решает вопрос только per-model закон, но Теорема 40.6 (quantizationLaw_iff_massGap) 🟢 зелёно и без всякой границы: закон решает вопрос ровно потому, что он и есть вопрос.
Через эту эквивалентность (вместе с not_massGap_iff_nonempty_ladder) связка самообоснования семантически сворачивается в MassGap S ∧ ¬ MassGap S — у Коллатца и P/NP стороны не были зелёно эквивалентны цели и её отрицанию, у Янга–Миллса эквивалентны.
Потому декретная дверь закрыта дважды: универсальная форма опровергнута кованым свидетелем (ymGround_universal_refuted 🟢, дословно ymLawUniversal_refuted), а per-model декрет переименовал бы цель, не добавив причины. Единственный вход остался внешним — data anchor, построенный спектр настоящей неабелевой теории, которого в mathlib нет.
Итог раздела. Всё сведено в ym_locked_behind_engine_status 🟢: универсал опровергнут, внутреннее знание невозможно, закон влечёт щель, кованые свидетели обеих сторон живы, ℕ-двигатель запрещён — модуль целиком зелёный, карантин не импортируется, таинт репозитория не растёт.
Примечание (что мы не утверждаем). Это не решение проблемы Клэя и не Гёдель: ни неполноты, ни неподвижной точки — только вполне-фундированность, и вся эпистемика модель-внутренняя: о настоящей квантовой теории Янга–Миллса теоремы этой секции не говорят ничего, она остаётся открытой 🔴. Условность названа: сам закон квантования — 🔴-вход per-model, и всё «при законе» здесь импликация; а тавтологизация связки через
quantizationLaw_iff_massGapне спрятана — она и есть причина, почему выход один и он внешний.
Философское отступление: масса как щель, вакуум как отказ от даровой работы¶
Эта глава ближе всех к настоящей физике, и связь здесь не метафорическая, а буквальная. Масс-щель Янга–Миллса — не абстрактное «Δ > 0 ниже уровней»; это утверждение о том, почему у материи есть масса.
Протон весит ≈ 938 МэВ, и лишь около процента этого — массы покоя кварков (хиггсовский вклад); всё остальное — энергия конфайнмента, энергия запертого глюонного поля. Масса адрона — это и есть щель: минимальная цена возбуждения над вакуумом.
Нет щели — нет и массы: вселенная была бы прозрачным супом безмассовых глюонов, без протонов, без ядер, без нас.
Почему природа обязана иметь щель? Потому что безщелевой спектр — вечный двигатель, и в самом физическом смысле. Возбуждения сколь угодно малой энергии над вакуумом означают, что из вакуума можно черпать работу без нижнего предела: бесконечно много всё более дешёвых мод, бесконечная перекачка энергии из «ничего».
Наша halving-лестница 2·E(n+1) ≤ E(n) — это в точности «сколь угодно мягкий глюон», башня всё более дешёвых возбуждений, которую безщелевая теория разрешила бы. Квантованность спектра — то, что энергия приходит дискретными порциями, ранжированными натуральным числом, — обрывает лестницу ровно так же, как гитарная струна не может звучать сколь угодно тихо над состоянием покоя: у неё есть основной тон. Безмассовое поле — это струна без нижней ноты.
Здесь и лежит смысл центрального результата Теорема 40.5 (massGap_of_quantizationLaw): квантованность запрещает вечный двигатель, а запрет вечного двигателя и есть масса. Ранговое квантование, убивающее ℝ-лестницу через EPMI, — математическая тень физического факта, что энергия квантуется.
Клэй просит доказать, что для настоящей неабелевой калибровочной теории эта квантованность действительно имеет место (наш 🔴 data-anchor — построенный гамильтониан КТП). Мы доказали структурную половину, ту, что от конкретной теории не зависит: где есть квантованный ранг — там нет безщелевой лестницы, там есть масса.
Вселенная устойчива, потому что вакуум берёт плату за первое возбуждение — и эта плата, в переводе на язык программы, есть невозможность вечного двигателя Евклида.
← 39. P/NP: оплата сертификатов · Оглавление · 41. Навье–Стокс: гладкость →