Ходж: квантованные заряды и оплата циклами

← 41. Навье–Стокс: гладкость · Оглавление · 43. Мерсенн через первопричину →

Lean-источник: Engine/HodgeFront.lean — зелёная цепь и трилемма, всё 🟢; Engine/CausalClosureAxiom.lean §14 — одна растяжка. Обозначения статуса: 🟢 — доказано при стандартных аксиомах; 🟡 — доказано условно на аксиому step00FirstCause; 🔴 — открытый вход.

Прочтение: заряд, оплата, полнота

Класс Ходжа мы читаем как квантованный заряд: рациональный класс когомологий выровненного типа (p,p) — «разрешённую величину». Алгебраический цикл — это оплата заряда, его реализация настоящим геометрическим объектом. Гипотеза Ходжа тогда — это утверждение о полноте: всякий квантованный выровненный заряд оплачен. А неоплаченный заряд, если бы он существовал, открыл бы бесконечный строгий спуск по натуральной высоте (знаменателю или сложности остатка) — то есть запрещённый вечный двигатель.

Честная граница — сразу и громко, как в предыдущих трёх главах. В mathlib нет теории Ходжа: мы проверили это дословно — слово «Hodge» встречается в пине ровно трижды, и все три раза мимо (цитата книги Ходжеса по теории моделей и упоминания p-адической теории Ходжа в комментариях периодных колец). Нет ни классов Ходжа, ни алгебраических циклов, ни когомологий многообразий, ни hodge-star-оператора.

Поэтому HodgeLedger — абстрактный леджер, бухгалтерская книга зарядов (см. словарь): классы, предикаты IsHodge и IsAlgebraic, высота height : Cls → ℕ и якорь квантования «оплачен ⟺ высота 0». Проблему тысячелетия мы не решаем и не объявляем решённой; остаток — именованный вход DescentLaw, то есть гейт: честно названное недостающее утверждение.

Двигатель мёртв безусловно — и это заголовок ветви

У Ходжа есть новость, которой не было у остальных ветвей, и стоит начать с неё. Двигатель здесь мёртв всегда, без единой гипотезы.

Теорема 42.1 (isEmpty_unpaidDescentChain, 🟢). Для каждого Ходж-леджера \(S\) тип \(\mathrm{UnpaidDescentChain}(S)\) пуст: бесконечной строго убывающей по высоте цепи неоплаченных зарядов не существует ни в одной модели. Список аксиом — только [propext, Quot.sound], даже без выбора: это чистый EPMI при A = 1.

Сравним с Янг–Миллсом, чтобы увидеть асимметрию. Там вещественная лестница жила ровно при безмассовости и убивалась декретируемым законом квантования — квантование было отдельным входом. Здесь квантование встроено в саму модель: высота — натуральное число height : ℕ, и потому двигатель мёртв в любой модели, безусловно. Вся содержательность ветви от этого сместилась: спорным остаётся не «квантуется ли заряд» (да, по построению), а существование самих шагов оплаты — то есть закон.

Герой и коллапс зеркала стоимости

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

Теорема 42.2 (hodgeProperty_of_descentLaw, 🟢 — герой). Если \(\mathrm{DescentLaw}(S)\), то \(\mathrm{HodgeProperty}(S)\): закон спуска влечёт гипотезу Ходжа модели. Доказательство — сильная индукция по высоте (выбор не нужен); тем же можно пройти и цепным маршрутом через descentSeq — зеркало ladderSeq Янг–Миллса.

Теорема 42.3 (no_unpaid_lawful_model, 🟢). Не существует леджера \(S\) такого, что одновременно \(\mathrm{DescentLaw}(S)\) и \(\mathrm{Nonempty}(\mathrm{UnpaidClass}(S))\): модели «закон плюс неоплаченный заряд» не бывает.

Обратная сторона честно вакуумна: descentLaw_of_hodgeProperty доказывается пустым квантором (если всё оплачено, неоплаченных зарядов нет) — в отличие от Янг–Миллса, где обратный ранг строился по-настоящему. И отсюда — решающий аудит:

Теорема 42.4 (descentLaw_iff_hodgeProperty, 🟢). Для каждого леджера \(S\): \(\mathrm{DescentLaw}(S) \iff \mathrm{HodgeProperty}(S)\) — зелёно и без всякой границы.

Это снова форма осуждённого моста: декретировать закон для модели значило бы декретировать её гипотезу дословно. Шестого поля декрета быть не может; недостающее — не пропозиция, а data anchor, настоящие рациональные (p,p)-классы.

Почему шестой границы нет — и уникальная точка ветви

Трилемма — обязательная трёхсторонняя проверка кандидата в границы (см. словарь) — подтверждает вывод со всех сторон, и одна из её граней здесь особенная. Универсальная форма закона опровержима: кованая модель cookedUnpaid несёт неоплаченный заряд высоты 1, а шаг спуска от него упёрся бы в оплаченность нулевой высоты (тот самый якорь квантования) — декрет взорвал бы карантин. Экзистенциальная форма уже доказана и не зависит вообще ни от каких аксиом (cookedPaid: закон вакуумен, гипотеза дословна) — декрет был бы пустым.

А вот третья грань — уникальная. Механически перенесём с Янг–Миллса манифестационную форму, но над цепями (над двигателем). Она вырождается в зелёную теорему:

Теорема 42.5 (hodgeChainManifestationLaw_green, 🟢). \(\mathrm{HodgeChainManifestationLaw}\): для каждого леджера \(S\) и каждой цепи \(C : \mathrm{UnpaidDescentChain}(S)\) выполняется \(\mathrm{ChainManifests}(C)\). Поскольку по Теореме 42.1 таких цепей не существует ни в одной модели, закон над ними вакуумно истинен.

Это вердикт V2-типа, а не V3 — и вот почему важно не спутать: из пустого типа свидетелей нельзя собрать V3 («несовместимо с границей»), потому что V3 нужен зелёно предъявленный свидетель.

Честный V3-свидетель здесь обязан быть не цепью, а одиночным неоплаченным классом cookedUnpaidClass — он предъявляется конструкцией, без выбора. Тонкая разница между «двигатель предъявим» и «отклонение предъявимо» здесь выходит на поверхность отчётливее, чем где-либо.

Теорема 42.6 (hodgeManifestationLaw_refutes_boundary, 🟢). Если \(\mathrm{HodgeManifestationLaw}\), то \(\neg\,\mathrm{TheStrictLastStep00Obligation}\): манифестационная форма закона несовместима с принятой границей карантина.

Единственное честное 🟡 ветви — растяжка (намеренный детектор взрыва, см. словарь) quarantine_inconsistent_if_hodgeManifestationLaw_decreed (§14): декрет манифестационной формы взорвал бы карантин ровно здесь; её безопасность проверена (закон эквивалентен глобальной заморозке, а зелёный мир знает заморозку лишь при A ≤ 4).

Философское отступление: квантование заряда и полнота спектра

Гипотеза Ходжа кажется чисто геометрической, но её физический смысл — о квантовании заряда и о том, что всякий разрешённый заряд кем-то несётся. В физике многие величины приходят только целыми кратными: электрический заряд — в единицах e; магнитный поток в сверхпроводнике квантуется, Φ = n·h/2e; а аргумент Дирака показывает, что одно существование магнитного монополя заставляет заряд быть квантованным, eg = n·ℏc/2.

Класс Ходжа — это ровно квантованный заряд геометрии: класс когомологий рационального типа (p,p), «разрешённая величина». А гипотеза говорит: каждый такой заряд реализован настоящим геометрическим объектом — алгебраическим циклом. Всякий разрешённый заряд несёт реальный носитель.

У этого есть точный физический аналог — принцип полноты спектра зарядов: в согласованной теории (гипотезы «болота» в квантовой гравитации, отсутствие глобальных симметрий) каждый разрешённый калибровочный заряд обязан быть занят каким-то состоянием — нет «пустых» разрешённых зарядов без частицы, которая бы их несла. Ходж — геометрическое зеркало этой полноты: нет пустого (p,p)-заряда без цикла-носителя. Неоплаченный класс Ходжа — это разрешённый заряд без носителя, дырка в спектре реализаций.

И вот почему двигатель здесь мёртв безусловно, в отличие от Янг–Миллса. Квантование у нас встроено в модель: высота — натуральное число. В физике это соответствует тому, что квантованность заряда — данность постановки, а не предмет спора; спорна лишь полнота — занят ли каждый разрешённый уровень.

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

Вывод. Дискретность решётки — тот же запрет вечного двигателя, что держит всю программу; а полнота её заполнения — открытое сердце, которое ни декретировать честно нельзя (закон эквивалентен цели), ни доказать без настоящих (p,p)-классов, которых в формализации пока нет.

Ходж за тем же горизонтом

У стены, о которую разбились внутренние решения Коллатца и P/NP, есть и ходжев склон — эпистемический комплемент ветви собран в Engine/HodgeEpistemic.lean. Решить фронт изнутри значило бы самообосновать per-model закон спуска: машина несла бы сам закон и вместе с ним свидетельство, что вывела его, пересекая собственный горизонт.

Такая пара (InternalisedHodgeGround) самоуничтожается одной строкой (no_internalisedHodgeGround), и потому «узнать нельзя изнутри» — теорема, а не лозунг:

Теорема 42.7 (hodgeCause_unknowable, 🟢). Для каждого леджера \(S\): \(\neg\,\mathrm{InternalKnowledgeOfHodgeCause}(S)\) — внутреннее самообоснование закона спуска невозможно ни в одной модели, безусловно и без аксиом. Ни статус самой гипотезы, ни её независимость при этом не утверждаются — только невозможность внутреннего самообоснования.

Противоречие оплачено не одной лишь формой пары — у него есть второй, двигательный маршрут. Под per-model законом неоплаченный заряд разворачивается в настоящую бесконечную цепь спуска (unpaidDescentChain_of_descentLaw) и проецируется высотой в вечный двигатель на ℕ (unpaidClass_under_law_carries_perpetual_engine).

Из самой пары двигатель тоже строится подлинно, не ex falso (internalisedHodgeGround_builds_engine) — а сжигает его та же стена вполне-фундированности no_perpetual_engine_on_nat, что у Коллатца и P/NP. Скажем честно, где тут условие: двигатель встаёт из отклонения под законом — у Коллатца хватало голого контрпримера, здесь же без закона у одиночного неоплаченного заряда нет даже первого шага.

И третья створка знакома дословно: универсальная форма закона уже кованно опровергнута — hodgeUniversal_forged_refutation (реэкспорт hodgeLawUniversal_refuted), тот самый cookedUnpaid, где шаг с высоты 1 упирается в якорь квантования. Как у Янг–Миллса и теперь у Коллатца, декретный путь через универсал закрыт машинно; живым остаётся только per-model вход — а он, по Теореме 42.4 (descentLaw_iff_hodgeProperty), равен цели дословно.

Теорема 42.8 (hodge_locked_behind_engine_status, 🟢). Для каждого леджера \(S\): $\((\neg\,\mathrm{HodgeDescentLawUniversal})\;\land\;\mathrm{IsEmpty}(\mathrm{UnpaidDescentChain}(S))\;\land\;(\neg\,\mathrm{InternalKnowledgeOfHodgeCause}(S))\;\land\;(\mathrm{DescentLaw}(S)\iff\mathrm{HodgeProperty}(S)).\)$ Универсал опровергнут / цепи пусты в каждой модели / внутреннее знание невозможно / per-model закон ⟺ гипотеза модели — целиком зелёный, таинт репозитория не растёт.

Примечание (что мы не утверждаем). Это не решение гипотезы Ходжа и не Гёдель: ни неполноты, ни неподвижной точки — только модель-внутренняя эпистемика и ℕ-спуск. Пара самообоснования формально есть «ground + его отрицание»; её содержательность оплачена зелёным отождествлением обеих сторон с содержанием (закон ⟺ гипотеза модели; отрицание ⟺ предъявимость неоплаченного заряда, not_hodgeProperty_iff_unpaidClass) и подлинным двигательным маршрутом. Дихотомической новизны пара не несёт — ценность архитектурная: Ходж встаёт в тот же ряд «заперто за двигателем», что P/NP и Коллатц (hodge_no_internal_decision_without_engine).

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

Ходж — шестой фронт одной машины (близнецы → Риман → P/NP → Янг–Миллс → Навье–Стокс → Ходж), и корень у всех один: невозможность вечного двигателя. Серия трилемм устойчива и складывается в отчётливое правило.

Итог раздела. Честная граница декрета существует только там, где свидетель отклонения зелёно непредъявим — таковы twin-узел и off-critical нуль. А всюду, где отклонение куётся — фреймы у P/NP, спектры у Янг–Миллса, профили у Навье–Стокса, неоплаченные заряды здесь, — декрет либо взрывается, либо пуст, и остаётся зелёная условная теорема с честно названным входом.

Ходж добавил к этому правилу собственную краску: когда квантование встроено в самую модель, двигатель мёртв безусловно, и гипотеза сжимается до одного вопроса — существуют ли шаги оплаты.

---

← 41. Навье–Стокс: гладкость · Оглавление · 43. Мерсенн через первопричину →