我们近期发布了 我们的P vs NP证明的形式化验证代码。 

具体地址见： https://github.com/zhengbojin/PvsNP

这一形式化验证项目的发布意味着：如果存在NTM能够恰好验证子集和问题，且Lean4系统可靠的前提下， 我们的PvsNP证明是 正确的。 

具体内容见技术报告及代码。

 顺便提一下：  

1 ）存在NTM能够恰好验证子集和问题 这一定理是整个计算复杂性理论的基础。 如果它错了，整个计算复杂性理论就不用玩了。

 2 ） Lean4系统的可靠性 远远超过 专家评审的可靠性。Lean4系统基于严谨的公理系统，其内核只有几百行代码，且这些代码是可审计的。当然，不排除这几百行代码中仍然存在Bug。但从过去几十年的实践来看， Bug出现的概率是很低的。 

====================================================

# 技术报告：P ≠ NP 形式化证明工程（Lean 4）

- **项目**：`D:\lean4\pvsnp`（lake 工程，库名/模块名 `PvsNP`）

- **版本**：commit `7c62750`（全链 0 error、0 sorry、单公理）

- **作者**：Bojin Zheng, Jingwen Zheng

- **日期**：2026-08

- **配套论文**：`measure.C.0.7.tex`、`models.C.0.6.tex`、`MultiType.C1.2.tex`（理念篇）等

---

## 1. 项目概述

在 Lean 4（mathlib）中对"P ≠ NP"给出**单一公理**基础上的完整形式化证明链。核心思想（对应论文框架）：

- 计算模型使用 **CBTM**（复合带图灵机，符号 = 实部 × 虚部，F4 = `Bool × Bool`）；

- 非确定性分支的"虚部"不是外部编码约定，而是**计算模型的内在语义**（数计一体：语义内建于符号）；

- 虚部标记（α = `(false,true)`）携带**不可公度性**语义——每个标记对应一个素数平方根生成元（线性独立），构成**本质维度 κ** 的度量单位；

- 经典 Bool 层 = F4 层的**实部投影**（压平）：虚部与语言无关，只与计算模型有关；

- 分离（P ≠ NP）发生在**虚部语义层**（F4 层，严格可证）；**框架内经典闭合**在 CBTM 内部完成——受限 CBTM 逐一步模拟 DTM（维度 0 保持），选项下界（κ ≥ n）与维度 0 的矛盾传到受限 CBTM（`no_dtm_recognizes_subsetSumF4`，无前提、无新公理，见 §6.5）。

**交付标准**：0 `sorry`、0 error、`lake build` 通过、全部结论由单一公理 `exists_NTM2_solves_subsetSum`（公理 V6，四条款）推出。

---

## 2. 计算模型

### 2.1 NTM2 —— 规范非确定图灵机（`Basic.lean`）

最终模型（经用户多次修正后定型）：

- **输入**：`List Bool`（与经典 P/NP 语言相同；虚部不是输入的一部分，而是计算模型层的标记）；

- **格局** `NTM2Config A x`：`{ state : ℕ, tape : ℤ → F4, headPos : ℤ }`——复合磁带（实部读/写 = 经典语义，虚部 = vb 带值）；

- **转移**：积型签名 `(ℕ × Bool × ℤ) → Finset (ℕ × Bool × Dir)`（状态 × 读到的实部 × 位置 → 有限转移集合）；

- **vb 派生**（`vbAt : ℤ → Bool`）：虚部不由机器存储，而是从转移结构派生（card = 2，与位置绑定；分叉 ⟺ 虚部 = 1）；

- **初始带**：输入区实部 = 输入串，虚部 = `vbAt`；空白格 = `(blankSym, vbAt 0)`（空白区虚部常数化）；

- **接受** `acceptsTape`：存在可达接受路径（磁带语义）。

**规范条款 `NTM2.Canonical`**：

1. 任意可达路径每步磁头位置 ∈ `[0, len)`（只在输入区内活动）；

2. 非空路径的终配置 `headPos < len`；

3. `List.Nodup (π.map pos)`（每格至多读一次）。

支持单位：