% --- Section Content : Mechanized Deductive Architecture in Lean 4 ---
\subsection{Mechanized Deductive Architecture in Lean 4}
\label{sec:lean4_mechanization}

To guarantee the absolute correctness of our mathematical derivations, the core deformation-to-the-normal-cone desingularization, shifted cotangent lift, and base-fiber symplectic splitting theorems are formally mechanized in Lean 4 without custom axioms.