The Membership Problem for Pedigree Polytope (M3P) asks, given $X\in\mathbb{Q}^{\binom{n}{3}}$, whether $X\in\mathrm{conv}(P_n)$, where $P_n$ is the set of all pedigrees. A pedigree is a structured encoding of a Hamiltonian cycle construction in $K_n$. We establish that M3P is solvable in strongly polynomial time via a recursively constructed layered network $(N_k, R_k, μ)$ and a multicommodity flow problem MCF$(k)$. The necessary and sufficient condition for membership established is that the optimal total flow in MCF$(n-1)$ equals the maximum possible flow $z_{\max}$. The complexity analysis, grounded in Tardos's strongly polynomial algorithm for combinatorial linear programs (1986), shows that this condition can be checked in strongly polynomial time in the dimension of the matrix involved. By sufficiency, this implies M3P~$\in$~P. Since the Symmetric Travelling Salesman Problem (STSP) reduces to M3P via the Multistage Insertion (MI) formulation (Arthanari 1983), STSP is solvable in polynomial time, and the P vs.NP question is resolved. The proofs leading to this result are fully machine-verified in Lean~4/Mathlib4, with zero unresolved \texttt{sorry}s in the main proof chain. The main contribution is the Lean~4 machine verification of all proofs in the main chain, resulting in \texttt{theorem p\_equals\_np}: P = NP. The Lean~4 formal verification covers the sufficiency of MCF(n-1) for membership in $\mathrm{conv}(P_n)$, and the P = NP chain via Maurras (2002), Grötschel--Lovász--Schrijver (1988), Cook (1971), and Karp (1972). The complete lean project (36 Lean~4 files, 2968/2968 build targets clean) is available at https://github.com/TiruArt/Pedigree-Polytopes-Lean4.

翻译：谱系多面体成员问题 (M3P) 询问：给定 $X\in\mathbb{Q}^{\binom{n}{3}}$，是否存在 $X\in\mathrm{conv}(P_n)$，其中 $P_n$ 为所有谱系构成的集合。谱系是 $K_n$ 中哈密顿圈构造的结构化编码。我们证明，通过递归构建的分层网络 $(N_k, R_k, μ)$ 及多商品流问题 MCF$(k)$，M3P 可在强多项式时间内求解。所建立的成员关系充要条件为：MCF$(n-1)$ 的最优总流量等于最大可能流量 $z_{\max}$。基于 Tardos (1986) 组合线性规划强多项式算法的复杂度分析表明，该条件可在涉及矩阵维度的强多项式时间内检验。由充分性可知，M3P~$\in$~P。由于对称旅行商问题 (STSP) 可通过多阶段插入 (MI) 形式 (Arthanari 1983) 归约为 M3P，STSP 可在多项式时间内求解，从而 P vs. NP 问题得以解决。证明该结果的全部过程在 Lean~4/Mathlib4 中完成机器验证，主证明链中零未解决 \texttt{sorry}。主要贡献在于主证明链所有步骤的 Lean~4 机器验证，最终得到 \texttt{theorem p\_equals\_np}: P = NP。Lean~4 形式化验证覆盖 MCF(n-1) 对 $\mathrm{conv}(P_n)$ 成员关系的充分性，以及通过 Maurras (2002)、Grötschel--Lovász--Schrijver (1988)、Cook (1971) 和 Karp (1972) 构建的 P = NP 链条。完整 Lean 项目 (36 个 Lean~4 文件，2968/2968 构建目标无错误) 见 https://github.com/TiruArt/Pedigree-Polytopes-Lean4。