% --- Section 2.1 : The Deformation to the Normal Cone and Graded Rees Algebra ---
\subsection{The Deformation to the Normal Cone and Graded Rees Algebra}
\label{sec:rees_deformation}

A foundational obstruction in the numerical simulation of singular Hamiltonian systems is that standard numerical integrators discretize the phase space in an undifferentiated manner. Near a singularity, metric gradients diverge, forcing variable-step algorithms into an infinite slowdown (the Sundman time-freezing dilemma~\cite{sundman1912memoire}) or prompting ad-hoc potential softening that alters the secular invariants of the physical model.

To resolve this dilemma without metric alteration, we invoke the canonical geometric degeneration developed in algebraic geometry by Fulton~\cite{fulton1984intersection} and Verdier~\cite{verdier1976specialisation}, and elevated to derived symplectic geometry by Calaque and Safronov~\cite{calaque2024deformation}: the \emph{deformation to the normal cone}. Rather than regularizing a singularity by adding artificial isotropic parameters, this construction replaces the ambient phase space with a one-parameter family of geometries interpolating smoothly between the non-linear global dynamics and a flat, abelian linear model at the singularity.

\emph{Ontological Scope: Classical Symplectic Mechanics vs. Shifted Derived Geometry.}---While Calaque and Safronov~\cite{calaque2024deformation} formalize the deformation to the normal cone within the higher category of derived prestacks equipped with shifted symplectic and Lagrangian structures ($n \in \mathbb{Z}$), our physical Hamiltonian phase space and accompanying Lean~4 kernel operate on the classical degree-$0$ differential framework: smooth finite-dimensional manifolds $M = \mathbb{R}^{3N}$, classical unshifted cotangent bundles $T^*M$, and canonical Darboux 2-forms $\omega_0$. Calaque and Safronov's theory provides the conceptual and functorial justification for the normal cone degeneration, which we instantiate in unshifted Hamiltonian mechanics.

To bridge global derived algebraic geometry with mechanized proof, our accompanying Lean~4 development formalizes the \emph{Constructive 1-Jet Algebraic Kernel}: it certifies the retraction of the evaluation morphism onto the singular base stratum, the canonical normal cone symplectic 2-form $\omega_{\mathrm{normal}}$, its constructive non-degeneracy, and the exact symplecticity of the transverse fiber flow.

\subsubsection{The Graded Rees Algebra and Affine Degeneration}
To describe the local geometry near a singular or collision locus $Z \subset M$ without coordinate pathology, we equip the smooth configuration manifold $M$ with its structure sheaf $\mathcal{O}_M$ of smooth (or regular algebraic) functions. The closed submanifold $Z$ is intrinsically defined by the collection of functions that vanish along it; this forms the \emph{ideal sheaf} $\mathcal{I}_Z \subset \mathcal{O}_M$. In local adapted coordinates $(x, y) \in Z \times \R^k$ where the locus is cut out by $\{y_1 = \dots = y_k = 0\}$, the ideal $\mathcal{I}_Z$ is locally generated by the transverse coordinate functions $(y_1, \dots, y_k)$, and its powers $\mathcal{I}_Z^k$ consist of functions vanishing to order at least $k$ on $Z$.

The canonical geometric degeneration of $M$ toward the normal bundle of $Z$ is algebraically encoded by the \emph{graded Rees algebra} $\mathcal{R}(\mathcal{I}_Z)$ over the affine line $\mathbb{A}^1 = \operatorname{Spec} \R[t]$, which rescales functions according to their vanishing order along $Z$:
\begin{equation}
    \mathcal{R}(\mathcal{I}_Z) = \bigoplus_{k \in \Z} t^{-k} \mathcal{I}_Z^k \subset \mathcal{O}_M[t, t^{-1}],
\end{equation}
with $\mathcal{I}_Z^k = \mathcal{O}_M$ for $k \le 0$. The total deformed space is the relative spectrum $\mathcal{D}_Z M = \operatorname{Spec}_M \mathcal{R}(\mathcal{I}_Z)$, canonically fibered over the affine line via $\pi : \mathcal{D}_Z M \to \mathbb{A}^1$. Geometrically, $\mathcal{D}_Z M \cong \operatorname{Bl}_{Z \times \{0\}}(M \times \mathbb{A}^1) \setminus \widetilde{M \times \{0\}}$.

To develop geometric intuition for this algebraic construction, consider the adapted coordinates $(x, y)$. For any $t \neq 0$, the scaling map $(x, y) \mapsto (x, y/t)$ identifies the generic fiber $\pi^{-1}(t)$ with $M$. As $t \to 0$, the dilated transverse coordinate $n = y/t$ parametrizes the linear vector space $N_{Z/M}$. The deformation thus acts as an intrinsic differential microscope, blowing up an infinitesimal neighborhood of the singular locus $Z$ into a full vector space where non-linear metric stiffness degenerates into abelian translational invariance.

\newpage
\begin{thmbox}[Fulton--Verdier Deformation and Calaque--Safronov Degeneration]{thm:calaque_safronov_degen}
Following Fulton~\cite[Chapter~5, \S5.1--5.2]{fulton1984intersection}, Verdier~\cite{verdier1976specialisation}, and Calaque and Safronov~\cite[Theorem~C, Section~3.1 \& Section~5.2]{calaque2024deformation}, the fibration $\pi : \mathcal{D}_Z M \to \mathbb{A}^1$ establishes a smooth one-parameter geometric degeneration:
\begin{enumerate}[noitemsep, topsep=2pt]
    \item \textbf{Generic Fiber ($t \neq 0$):} $\pi^{-1}(t) \cong M$ canonically for any $t \in \mathbb{A}^1 \setminus \{0\}$.
    \item \textbf{Central Special Fiber ($t = 0$):} At the degenerate apex $t = 0$, the fiber is canonically isomorphic to the normal bundle (or normal cone) of $Z$ in $M$:
    \begin{equation}
        \pi^{-1}(0) \cong N_{Z/M} = \operatorname{Spec}_Z \left( \bigoplus_{k \ge 0} \mathcal{I}_Z^k / \mathcal{I}_Z^{k+1} \right).
    \end{equation}
\end{enumerate}
\end{thmbox}
\leanrefright{normal_cone_limit}{deformation_limit_zero}{02_ReesDeformation_Theorems.lean}
In the accompanying mechanized 1-jet algebraic kernel, the evaluation morphism retracts identically onto the singular base stratum $Z$ at $t = 0$ (see Figure~\ref{fig:ch02_rees_normal_cone_fibration}).

\begin{figure}[htbp]
\centering
\resizebox{\textwidth}{!}{%
\begin{tikzpicture}[scale=1.0, every node/.style={font=\small}]
    % --- Base Affine Line A^1 ---
    \draw[->, >=latex, thick, color=DarkSlate] (0.2, 0) -- (14.4, 0) node[right] {$\mathbb{A}^1 = \operatorname{Spec}\R[t]$};
    \fill[NavyBlue] (2.4, 0) circle (2.2pt) node[below=4pt] {$t = 0$ \textbf{(Special Fiber)}};
    \fill[DarkSlate] (7.4, 0) circle (1.8pt) node[below=4pt] {$0 < t < 1$};
    \fill[AcademicPurple] (12.4, 0) circle (2.2pt) node[below=4pt] {$t = 1$ \textbf{(Generic Fiber)}};

    % --- Projection Arrows \pi ---
    \draw[->, >=latex, thick, NavyBlue] (2.4, 1.35) -- (2.4, 0.22) node[midway, left=3pt] {$\pi$};
    \draw[->, >=latex, dashed, DarkSlate] (7.4, 1.35) -- (7.4, 0.22) node[midway, left=3pt] {$\pi$};
    \draw[->, >=latex, thick, AcademicPurple] (12.4, 1.35) -- (12.4, 0.22) node[midway, right=3pt] {$\pi$};

    % --- Special Fiber at t = 0: Flat Normal Bundle N_{Z/M} and T*(N_{Z/M}) ---
    \draw[fill=ThmBg, draw=NavyBlue, thick, rounded corners=3pt] (0.3, 1.5) rectangle (4.5, 5.2);
    \node[NavyBlue, font=\footnotesize\bfseries, align=center] at (2.4, 4.76) {$\pi^{-1}(0) \cong N_{Z/M}$\\[-1pt]{\normalfont\scriptsize Abelian Normal Fiber}};
    % Flat vertical fibers
    \draw[NavyBlue!45, thin] (1.05, 2.05) -- (1.05, 4.20);
    \draw[NavyBlue!45, thin] (2.10, 2.05) -- (2.10, 4.20);
    \draw[NavyBlue!45, thin] (3.85, 2.05) -- (3.85, 4.20);
    % Base Z inside t=0
    \draw[very thick, NavyBlue] (0.65, 2.65) -- (4.05, 2.65);
    \node[font=\scriptsize\bfseries, NavyBlue] at (4.24, 2.65) {$Z$};
    \fill[NavyBlue] (2.10, 2.65) circle (2pt);
    % Linear translation arrow along cotangent fiber
    \draw[->, >=latex, very thick, PythonGreen] (2.10, 2.80) -- (2.10, 4.10);
    \node[PythonGreen, font=\scriptsize, align=left, anchor=west] at (2.18, 3.52) {$\Phi_s^{\mathrm{trans}}:$\\[-2pt]$w \mapsto w - s\nabla_n V$};
    \node[font=\scriptsize, NavyBlue] at (2.4, 1.76) {$\omega_{\mathrm{normal}} = \mathrm{d}x\wedge\mathrm{d}p + \mathrm{d}n\wedge\mathrm{d}w$};

    % --- Intermediate Fiber 0 < t < 1: Dilated Coordinates n = y/t ---
    \draw[fill=BadgeGray, draw=BorderGray, thick, rounded corners=3pt] (5.5, 1.5) rectangle (9.3, 5.2);
    \node[DarkSlate, font=\footnotesize\bfseries, align=center] at (7.4, 4.76) {$\pi^{-1}(t) \cong M$\\[-1pt]{\normalfont\scriptsize Dilated Scale $n = y/t$}};
    \draw[DarkSlate!75, very thick] (5.85, 2.65) .. controls (6.7, 2.80) and (8.1, 2.50) .. (8.95, 2.65);
    \draw[DarkSlate!45, thin] (6.25, 2.05) .. controls (6.40, 2.65) and (6.40, 3.45) .. (6.25, 4.15);
    \draw[DarkSlate!45, thin] (7.4, 2.05) .. controls (7.55, 2.65) and (7.55, 3.45) .. (7.4, 4.15);
    \draw[DarkSlate!45, thin] (8.55, 2.05) .. controls (8.70, 2.65) and (8.70, 3.45) .. (8.55, 4.15);
    \fill[DarkSlate] (7.48, 2.65) circle (2pt);
    \node[font=\scriptsize, DarkSlate, align=center] at (7.4, 1.76) {$\mathrm{ev}_t(x, n) = (x, t\,n)$};

    % --- Generic Fiber at t = 1: Ambient Manifold M with Singular Locus Z ---
    \draw[fill=PropBg, draw=AcademicPurple, thick, rounded corners=3pt] (10.3, 1.5) rectangle (14.5, 5.2);
    \node[AcademicPurple, font=\footnotesize\bfseries, align=center] at (12.4, 4.76) {$\pi^{-1}(1) \cong M$\\[-1pt]{\normalfont\scriptsize Curved Ambient Space}};
    % Strongly curved singular potential funnel near Z
    \draw[very thick, AcademicPurple] (10.65, 2.65) .. controls (11.6, 2.95) and (13.2, 2.35) .. (14.15, 2.65);
    \node[font=\scriptsize, AcademicPurple] at (13.35, 2.95) {$Z = \{y=0\}$};
    \draw[->, >=latex, AcademicPurple!65, thick] (11.1, 4.05) .. controls (11.9, 3.75) and (12.22, 3.05) .. (12.4, 2.77);
    \draw[->, >=latex, AcademicPurple!65, thick] (12.4, 2.77) .. controls (12.58, 3.05) and (12.9, 3.75) .. (13.7, 4.05);
    \fill[AcademicPurple] (12.4, 2.65) circle (2pt);
    \node[font=\scriptsize, AcademicPurple, align=center] at (12.4, 1.76) {Coupled flow on $(T^*M, \omega_0)$};

    % --- Horizontal Degeneration Morphism Arrows ---
    \draw[->, >=latex, thick, DarkSlate] (10.12, 3.35) -- (9.48, 3.35) node[midway, above=2pt, font=\scriptsize] {$n = y/t$};
    \draw[->, >=latex, thick, NavyBlue] (5.32, 3.35) -- (4.68, 3.35) node[midway, above=2pt, font=\scriptsize] {$t \to 0$};
\end{tikzpicture}%
}
\caption{Geometric degeneration of the graded Rees fibration $\pi : \mathcal{D}_Z M = \operatorname{Spec}_M \mathcal{R}(\mathcal{I}_Z) \to \mathbb{A}^1$ and its cotangent lift (Theorem~\ref{thm:calaque_safronov_degen} and Proposition~\ref{prop:conormal_fiber_linearity}). As $t \to 0$, the rescaled transverse coordinate $n = y/t$ blows up an infinitesimal tubular neighborhood of the singular locus $Z \subset M$ into the flat normal bundle $\pi^{-1}(0) \cong N_{Z/M}$, where non-linear potential forces become exact linear momentum translations $\Phi_s^{\mathrm{trans}}$ along the cotangent fibers $N_{Z/M}^*$.}
\label{fig:ch02_rees_normal_cone_fibration}
\end{figure}

\subsubsection{Symplectic Cotangent Lift and Transverse Normal Leaves}
In the framework of derived symplectic geometry~\cite{calaque2024deformation}, the cotangent lift of this family carries a relative symplectic form $\Omega_{\mathrm{rel}}$ over $\mathbb{A}^1$. 

The essential computational property uncovered by this degeneration is that the cotangent bundle of the central fiber $T^*(N_{Z/M})$ inherits a strictly \emph{abelian, linear symplectic structure}. In canonical Darboux coordinates $(x, n, p, w) \in T^*(N_{Z/M})$, where $(x, p) \in T^*Z$ and $(n, w) \in N_{Z/M} \times_Z N_{Z/M}^*$ (the Whitney sum $N_{Z/M} \oplus N_{Z/M}^*$), the canonical 2-form splits additively:
\begin{equation}
    \omega_{\mathrm{normal}} = \sum_{a} \mathrm{d}x_a \wedge \mathrm{d}p_a + \sum_{b} \mathrm{d}n_b \wedge \mathrm{d}w_b.
\end{equation}
\leanrefright{rees_defs}{omegaNormal}{01_ReesDeformation_Defs.lean}
\leanrefright{normal_cone_limit}{omegaNormal_nondegenerate}{02_ReesDeformation_Theorems.lean}

While the dynamics on the generic fiber $T^*M$ is governed by coupled non-linear equations with divergent curvatures near $Z$, the transverse motion along the cotangent fibers $N_{Z/M}^*$ degenerates into an exact translation generated by the normal gradient of the potential:

\begin{propbox}[Exact Normal Cone Symplectic Folia and Fiber Linearity]{prop:conormal_fiber_linearity}
In the sense of Cannas da Silva~\cite[Chapter~2]{cannas2001lectures} and Calaque and Safronov~\cite[Theorem~C]{calaque2024deformation}, let $V(n)$ be a smooth transverse potential on the normal cone fibers with symmetric Hessian matrix. The transverse fiber flow $\Phi_s^{\mathrm{trans}}(x, n, p, w) = (x, n, p, w - s \nabla_n V(n))$ satisfies exact symplectomorphism with respect to $\omega_{\mathrm{normal}}$:
\begin{equation}
    (\Phi_s^{\mathrm{trans}})^* \omega_{\mathrm{normal}} = \omega_{\mathrm{normal}}.
\end{equation}
Furthermore, the position and base momentum variations $(\delta x, \delta p, \delta n)$ are strictly preserved by $\Phi_s^{\mathrm{trans}}$, isolating all non-linear force accumulation into pure momentum translations along the flat transverse cotangent fibers.
\end{propbox}
\leanrefright{normal_flow_symp}{transverse_conormal_flow_symplectic}{02_ReesDeformation_Theorems.lean}

\begin{proofbox}[Proof of Proposition~\ref{prop:conormal_fiber_linearity}]
Under the transverse fiber flow $\Phi_s^{\mathrm{trans}}(x, n, p, w) = (x, n, p, w - s \nabla_n V(n))$, the differentials of the canonical Darboux coordinates transform as $\mathrm{d}x_a' = \mathrm{d}x_a$, $\mathrm{d}p_a' = \mathrm{d}p_a$, $\mathrm{d}n_b' = \mathrm{d}n_b$, and $\mathrm{d}w_b' = \mathrm{d}w_b - s \sum_c H_{bc}(n)\,\mathrm{d}n_c$, where $H_{bc}(n) = \partial^2 V / (\partial n_b \partial n_c)$ is the Hessian matrix of $V$. Pulling back the normal cone symplectic 2-form yields
\begin{equation}
    (\Phi_s^{\mathrm{trans}})^* \omega_{\mathrm{normal}}
    = \sum_a \mathrm{d}x_a \wedge \mathrm{d}p_a + \sum_b \mathrm{d}n_b \wedge \mathrm{d}w_b - s \sum_{b,c} H_{bc}(n)\,\mathrm{d}n_b \wedge \mathrm{d}n_c.
\end{equation}
Since $H_{bc}(n) = H_{cb}(n)$ is symmetric while the exterior product $\mathrm{d}n_b \wedge \mathrm{d}n_c = -\mathrm{d}n_c \wedge \mathrm{d}n_b$ is alternating, the double sum vanishes identically, establishing $(\Phi_s^{\mathrm{trans}})^* \omega_{\mathrm{normal}} = \omega_{\mathrm{normal}}$.
\end{proofbox}

This decoupling provides an exact geometric criterion: rather than fighting non-linear stiffness near singular strata with infinitesimal time steps, one can decompose the Hamiltonian vector field into a motion preserving the base $Z$ and a flat, exact translation along the transverse cotangent fibers of $N_{Z/M}^*$.