We present a self-contained, axiom-driven argument establishing the equality of the complexity classes $P$ and $NP$. The proof proceeds in three steps: (i)~we adopt a characterisation of $P$ in terms of the complement operation and polynomial certification, (ii)~we invoke the standard inclusion $P \subseteq NP$, and (iii)~we show that these two facts, together with the involutive nature of complementation, force $NP \subseteq P$. A fully mechanised verification of the logical structure is provided in the Lean~4 proof assistant, confirming that the conclusion follows from the stated axioms without any incomplete proof obligations.