P ≠ NP from Six Cited Axioms: A Machine-Verified Conditional Proof via Partition Function Analyticity

We formalize a conditional proof of \(\mathrm{P} \neq \mathrm{NP}\) in a Python-native proof language with Lean 4 export. The proof connects computational complexity to partition function analyticity: for each decision problem \(L\), the analyticity radius \(\rho(L) = \mathrm{ar}(Z_L)\) satisfies \(L \in \mathrm{P} \Leftrightarrow \rho(L) > 1\) (Barvinok 2016). NP-complete problems have Lee-Yang zeros on the unit circle, forcing \(\rho \leq 1\), hence \(\mathrm{NPC} \cap \mathrm{P} = \varnothing\).

The headline theorem (p_neq_np_core) depends on a minimal chain of 7 individually citable bootstrap axioms, with no proof-level sorrys on the critical path. The formalization contains 289 kernel-verified theorems and 59 derived lemmas spanning 14 complexity classes. The proof depends on 136 domain axioms: 87 standard complexity-theoretic facts, 14 partition function / power series axioms (partially novel), 6 Lee-Yang + Ising axioms (published), 7 Barvinok axioms (2 unrestricted + 5 scoped via Barvinok.admissible), and 22 type/predicate declarations. Of these, 3 are admitted without proof (Millennium Problem bridges, §6). The formalization exports to 1,804 lines of Lean 4 syntax (not yet compiled against Mathlib; see §7.3 for export limitations). Beyond the separation, it derives the complete 4-way \(\rho \Leftrightarrow \mathrm{P}\) characterization, \(\rho\)-portraits for Factoring and Graph Isomorphism, NP-intermediate placement (Ladner), universal polynomial hierarchy \(\rho\)-landscapes (\(\forall k,\, \Sigma_{k+1}\) has both regimes, via Nat.rec induction), and schematic cross-domain bridges to three other Millennium Problems (§6).

Keywords: P vs NP, formal verification, partition function, analyticity radius, Lee-Yang theorem, Barvinok, proof language

MSC 2020: 68Q15, 68Q17, 03B35, 82B20, 30B10