P/NP: полная оплата против быстрого проезда

← 38. Риман через первопричину · Оглавление · 40. Янг–Миллс →

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

Где мы

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

Прочтение простое и физичное. NP-задача — это полная оплата всех сертификатов ранга: решить поиск значит учесть каждого свидетеля по отдельности. P — это быстрый проезд по рангу: движение двигателя, которое пролетает ранг, не посещая все состояния. А неравенство между ними — из того, что быстрый проезд физически не может оплатить неограниченное семейство сертификатов. Всё это мы сейчас и докажем, машинно и без всякой аксиомы.

Две стороны на языке ранга

Переведём метафору в точные определения — прямо над структурами, которые у нас уже есть.

P-сторона. Быстрый проезд — это RankFastTraversal: всякий легальный путь PathN короче своего стартового ранга, n ≤ lexRank x. Двигатель не обходит все состояния — он ограничен рангом, с которого стартовал. И это не гипотеза, а закон самой машины:

Теорема 39.1 (rankFastTraversal_holds, 🟢). Всякий ранжированный граф проезжает ранг быстро: для любого ранжированного графа \(G\) всякий легальный путь PathN длины \(n\) из \(x\) удовлетворяет \(n \le \operatorname{lexRank}(x)\). Прямое следствие того, что длина пути не превосходит стартового ранга (len_le_lexRank, глава 01). P-сторону нам дарит сама конструкция.

NP-сторона. Полная оплата — это FullRankCertificatePayment: существование инъективного конечноключевого сжатия всей семьи генеалогий, где каждый сертификат учтён индивидуально. Проверить одного свидетеля дёшево (verificationEasy_always 🟢 — проверка сертификата легка всегда); дорого — учесть их всех.

Между ними — понятие неограниченной поставки (поставка — это семья сертификатов, которой отклонение «расплачивается», см. словарь): UnboundedCertificateSupply — семья сертификатов бесконечна.

Сердце неравенства: пигеонхол

Теперь ключевая зелёная теорема, из-за которой всё и работает.

Теорема 39.2 (no_fullPayment_of_unboundedSupply, 🟢). Быстрый конечноключевой двигатель не может полностью оплатить неограниченное семейство сертификатов: если семья генеалогий \(F\) удовлетворяет UnboundedCertificateSupply (бесконечна), то FullRankCertificatePayment для \(F\) не выполнено, то есть не существует инъективного конечноключевого сжатия \(F\).

Почему это верно. Это чистый пигеонхол. Конечный ключ, пытающийся сжать бесконечную поставку, обязан столкнуть двух разных свидетелей в один — иначе он различал бы бесконечно много объектов конечным числом ярлыков. А столкновение — это двойная бухгалтерия, невозможная оплата. Дёшево проехать ранг, дорого коснуться каждого; и второе несовместимо с первым при бесконечной поставке.

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

Теорема 39.3 (concreteSupply_unbounded_smallScale, 🟢). При \(A \le 4\) конкретная семья сертификатов бесконечна: тип concreteFamily A 1.Index бесконечен, свидетель — инъекция пятиадической цепи fiveAdicChainFlow (та самая, что опровергла ветвь \(A \le 4\) в главе 24).

Следствие 39.4 (concrete_noFullPayment_smallScale, 🟢). При \(A \le 4\) полная оплата конкретной семьи невозможна: FullRankCertificatePayment (concreteFamily A 1) не выполнено. Прямо из Теоремы 39.2 (no_fullPayment_of_unboundedSupply), применённой к бесконечной поставке Теоремы 39.3.

«NP = полная оплата» — теорема, а не метафора

Осталось связать «полную оплату» с локальным P-успехом, чтобы фраза из заголовка перестала быть образом. И она связывается — на каждом масштабе:

Теорема 39.5 (concrete_localPSuccess_iff_fullPayment, 🟢). Локальный P-успех эквивалентен полной оплате сертификатов: для любых \(A, M_0\) выполнено LocalPSuccess (concreteProblem A M0) \(\iff\) FullRankCertificatePayment (concreteFamily A M0).

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

Теорема 39.6 (pnp_rank_separation_smallScale, 🟢 — то самое неравенство). При \(A \le 4\) одновременно выполнены пять утверждений: RankFastTraversal (concreteGraph A 1) (двигатель проезжает ранг быстро), VerificationEasy для каждого сертификата (concreteFamily A 1).cert i (проверка легка), UnboundedCertificateSupply (concreteFamily A 1) (поставка неограничена), \(\lnot\) FullRankCertificatePayment (concreteFamily A 1) (полная оплата невозможна) и LocalSearchIncompressible (concreteProblem A 1) (локальный поиск несжимаем).

Итог раздела. Пять граней метафоры сошлись в одном зелёном утверждении: быстрый проезд, лёгкая проверка, бесконечная поставка, невозможность полной оплаты, несжимаемость. Это и есть «P ≠ NP» в ранговой модели — доказанное, без аксиом.

Раскол по масштабам

Тут возникает законный вопрос: если несжимаемость доказана, не противоречит ли она декрету близнецов, который на своём масштабе как раз разрешает коллизии? Нет — и разводит их простое наблюдение, что локальный P-успех и несжимаемость суть строгие отрицания друг друга, а живут они на разных масштабах.

Декрет близнецов работает при A ≥ 5 (маленькую ветвь мы опровергли), и там он даёт локальный P-успех на каждом пороге — то есть на своём масштабе первопричина полностью оплачивает сертификаты (decreedScale_fullPayment 🟡). А несжимаемость живёт при A ≤ 4, где поставка бесконечна и оплата невозможна, — безусловно, зелёно, декрету не принадлежит. Один и тот же язык описывает оба мира; они просто разнесены по масштабу.

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

Почему границы P/NP у декрета нет

У близнецов декрет несёт живую границу, а Риман был честной второй границей, впоследствии отсоединённой от декрета (Option A). Естественно спросить: не стоит ли добавить P/NP-границу? Ответ — нет, и это доказано машинно. Мы проверили все три мыслимые формы такого поля, и каждый вердикт оказался зелёной теоремой:

• универсальная форма (во всяком добросовестном фрейме P-решатель извлекает резолвер) опровержима (pnpLawUniversal_refuted): для фрейма allPFrame она сделала бы карантин противоречивым немедленно;
• decider-форма (реконструкция резолвера из голого решателя) тоже опровержима (pnpLawDeciderGated_refuted): голый PDecider существует классически для любого языка, а извлечённый из него резолвер бьётся о несжимаемость при A ≤ 4;
• экзистенциальная форма уже доказана (pnpLawExistential_green, свидетель constantsFrame) — а декретировать зелёную теорему бессмысленно: декрет был бы пустым.

Зеркало стоимости здесь схлопывается само: pnpLaw_asserts_separation 🟢 показывает, что закон эквивалентен разделению без всякой границы, и обе стороны — уже теоремы.

Вывод. Честного третьего поля не существует. Подлинно недостающий объект — не пропозиция над абстрактными фреймами, а привязанная к данным реальная машинная модель (в mathlib есть Turing.TM2ComputableInPolyTime, но даже композиция машин там ещё proof_wanted). Это тот же урок, что дал спектральный аудит Римана: «невакуумность на уровне пропозиций» — неверный критерий, нужен якорь в данных.

Примечание (якорь машинной модели). Этот недостающий объект теперь именован — Engine/PNPDataAnchor.lean ставит два красных входа над реальными структурами TM2. Первый, TM2CompositionLaw, называет вход ровно там, где у самого mathlib стоит proof_wanted (TM2ComputableInPolyTime.comp — композиция polytime-машин): proof_wanted не создаёт декларации, сослаться не на что, вход честно красный.

И здесь же — красивый улов честности: соблазнительная ∃-форма «язык TM2-разрешим с какой-нибудь кодировкой» машинно опровергнута как переименование True (tm2DecidesWithSomeEncoding_free) — жульническая кодировка enc x := encodeBool (run x) протаскивает ответ во вход, и тождественная машина его «вычисляет». Именно поэтому настоящий мост TM2FrameBridge обязан жить над фиксированной канонической кодировкой encodeNat, а не над экзистенциальной; это тот же урок кодировок, что дал спектральный аудит Римана на уровне пропозиций.

Пластичность фреймов и вакуумность №4

Отсюда — важная честная оговорка о том, чего мы не доказали. Абстрактный слой «классов сложности» пластичен: его можно скроить и так, что классы совпадают даром (allPFrame), и так, что разделяются даром (constantsFrame, свидетель — язык boolLanguage). Значит, никакое утверждение о настоящих классических P и NP из абстрактного слоя не следует, и мы его не делаем.

Попутно адверсариальный аудит вскрыл в уже написанном коде четвёртый эпизод вакуумности (вакуумность — когда утверждение выполняется даром, свидетелем-заглушкой; см. словарь): голый PDecider не несёт содержания сложности и строится классически для любого языка (classicalPDecider); поэтому над несжимаемым узлом не существует ни CanonicalResolverReconstruction, ни DeciderGuidedSelfReduction (оба типа доказуемо пусты).

Как следствие, decider-фронты FaithfulSelfReductionFront и CurrentExtractionFront классически пусты — их выводы о разделении вакуумны. Затронут только этот decider-канал; InP-мост Step00ToClassicalBridge остаётся честной условной формой (InP абстрактен). Вакуумность вскрыта и зафиксирована, а не спрятана.

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

У P/NP есть физическая изнанка, и она ложится на образ двигателя точнее, чем кажется. Ландауэр показал: стереть один бит информации стоит не меньше kT·ln 2 энергии — вычисление физично, у информации есть термодинамическая цена.

В нашем прочтении это выходит на первый план. NP-задача — это полная оплата всех сертификатов, учёт каждого свидетеля по отдельности; P — это быстрый проезд по рангу, движение, которое пролетает мимо, не касаясь всех состояний. Быстрый двигатель дёшев по «энергии» — число шагов ограничено стартовым рангом, — и именно поэтому он не может оплатить неограниченную поставку: конечный ключ, сжимающий бесконечное семейство, обязан столкнуть два разных свидетеля в один.

Аналогия прямая: нельзя за конечную энергию перебрать бесконечно много различимых состояний, не спутав часть из них. Быстрый проезд экономит топливо ровно ценой того, что проезжает мимо; полная оплата требует коснуться каждого. Разрыв между «проехать ранг» и «оплатить все сертификаты» — это и есть разрыв между P и NP в физической одежде: между дешёвым движением и дорогим полным учётом.

И только здесь, единственный раз из семи ветвей, неравенство оказалось зелёной теоремой без всякого декрета: в ранговой модели быстрый двигатель доказуемо не оплачивает неограниченную поставку. Термодинамическая интуиция — «полный учёт дороже быстрого движения» — доказана в ранговом мире; её перенос в мир машин Тьюринга остаётся тем самым недостающим data-anchor, как настоящий гамильтониан у Янга–Миллса и настоящие (p,p)-классы у Ходжа.

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

Три великих вопроса теперь стоят в одной архитектуре, но с тремя разными честными исходами: близнецы — живая граница декрета (узел, 🟡), Риман — риманова граница, отсоединённая от декрета (Option A — закон манифестации, отсоединённый фронт, а не живая граница), а P/NP — зелёная теорема в ранговой модели, без всякого декрета (🟢), с машинным доказательством того, что декретный путь для неё либо противоречив, либо пуст. Классическое P ≠ NP не доказано и не объявляется.

Есть и эпистемический двойник этого запрета: внутреннее, на конечном топливе, решение P/NP было бы вечным двигателем — недостижимым изнутри, «за тем же горизонтом», что и причина Коллатца (глава 56, Engine/PNPFirstCause); зелёно, без декрета, таинт — след аксиомы в списке зависимостей (см. словарь) — не растёт.

Дальше — Янг–Миллс (глава 40), где двигатель встречает спектр, и бесщелевой спектр оказывается вечным двигателем в чистом виде.

---

← 38. Риман через первопричину · Оглавление · 40. Янг–Миллс →