\section{Symplectic framing and freeness in every rank}\label{main:conclusion}
We now assemble the proof. Stable freeness and symplectic completion
settle ranks at least three. For rank two, alternating Witt vanishing
first gives a finite hyperbolic stabilization. We cancel its additional
planes in the stable range, leaving the rank-four frame required by
Theorem~\ref{bridge:criterion}.

Throughout this section, $R$, $r$, and $A$ satisfy the hypotheses of Theorem~\ref{main:quillen}. In particular, $A$ is a domain of dimension at most three. Theorem~\ref{global:naive_mw4} and Theorem~\ref{bridge:criterion} already give
\begin{equation}\label{main:sp4_transitive}
 \Um_4(A)=\Sp_4(A)e_1.
\end{equation}
Thus every unimodular column of length four has a symplectic completion over $A$.

\subsection{Stable freeness}

\begin{lemma}[Stable freeness and freeness in ranks at least three]\label{main:stable_free}
Every projective $A$-module is stably free, and $K_0(A)=\Z$ by rank. Every projective of rank at least three is free.
\end{lemma}
\begin{proof}
Let $P$ be projective. Clear denominators in a finite presentation to obtain a finite $R$-module $M$ with $M[1/r]\simeq P$.
Since $R$ is regular local of dimension four, $M$ has a finite
projective resolution of length at most four. Its projective terms
are finite free because $R$ is local; see \cite[Theorem~19.2 and
Corollary~19.6]{Eisenbud1995}. Localization gives a finite free
$A$-resolution of $P$.
The surjection onto $P$ splits because $P$ is projective. Its kernel
is therefore projective, so the preceding surjection splits in turn.
Proceeding through the finite resolution gives an alternating
direct-sum identity, hence an isomorphism $P\oplus A^a\simeq A^b$. This proves stable freeness and the asserted $K_0$ calculation.

Bass cancellation for a Noetherian ring of dimension at most three makes every stably free module of rank at least four free. If $Q$ has rank three, then $Q\oplus A$ has rank four and is free. A chosen isomorphism $Q\oplus A\simeq A^4$ presents $Q$ as the kernel of a unimodular row of length four. The transpose of a completion in \eqref{main:sp4_transitive} is an invertible completion of that row, and its kernel is free of rank three.
\end{proof}

We will also use Bass's elementary transitivity on rows of length at least $\dim A+2$ \cite[Theorems~9.3 and~11.1]{BassStable}.

\subsection{Metabolic alternating forms split integrally}

To pass from a Witt-class relation to an isometry, we need an explicit
splitting of a metabolic form. The following elementary construction
adjusts a chosen complement by a bilinear form with prescribed
antisymmetrization.

\begin{lemma}[Hyperbolicity of a metabolic alternating form]\label{main:metabolic}
Over an arbitrary commutative ring, a perfect alternating space with a projective Lagrangian is hyperbolic.
\end{lemma}
\begin{proof}
Let $L$ be the Lagrangian. Split the underlying exact sequence with quotient $L^*$. In this decomposition the pairing is
\[
 \langle(l,\alpha),(m,\beta)\rangle
    =\beta(l)-\alpha(m)+c(\alpha,\beta),
\]
where $c$ is an alternating form on $L^*$. There is a bilinear form $b$ on $L^*$ whose antisymmetrization is $-c$. Indeed choose a projective complement so that $L^*\oplus Q$ is free, extend $c$ by zero, choose a strictly triangular matrix with antisymmetrization $-c$, and restrict it to $L^*$.

View $b$ as a map $t:L^*\to L$ by $\beta(t\alpha)=b(\alpha,\beta)$. Replacing the complement by the graph $\alpha\mapsto(t\alpha,\alpha)$ changes its self-pairing by $b-b^t=-c$. The new complement is isotropic and the cross-pairing is unchanged. This is the hyperbolic form on $L\oplus L^*$.
\end{proof}

\begin{lemma}[A rank-four symplectic frame]\label{main:actual_frame}
Every oriented rank-two projective $P$ over $A$ admits an oriented isometry $P\perp \Hyp\simeq \Hyp^2$.
\end{lemma}
\begin{proof}
We first obtain a hyperbolic stabilization from the vanishing of the
alternating Witt group. We then cancel free hyperbolic planes while
the standard target remains in the stable range. The final isometry
retains the given rank-two space as the perpendicular complement.

\proofstep{1. The alternating form on the projective module.}
Write $\theta:\det P\xrightarrow{\sim}A$ for the chosen orientation.
For $p,q\in P$, it defines the pairing
$\langle p,q\rangle=\theta(p\wedge q)$. In an oriented
local basis this pairing is the standard perfect alternating form.
The frame constructed below is an isometry for this form.
By Theorem~\ref{gw:global_walt}, the alternating Witt group is zero. The hyperbolic map $h:K_0(A)\to K_0^{\mathrm{Sp}}(A)$ is therefore onto. Since $K_0(A)=\Z$ by Lemma~\ref{main:stable_free}, rank comparison gives $[P]=[\Hyp]$ in the Grothendieck group of alternating spaces.

\proofstep{2. A finite hyperbolic stabilization.}
Group completion supplies an alternating space $C$ with $P\perp C\simeq \Hyp\perp C$. Add $-C$ to both sides. The diagonal in $C\perp(-C)$ is a projective Lagrangian, so Lemma~\ref{main:metabolic} identifies this sum with the hyperbolic space on the underlying projective module $Q$ of $C$. Choose a finite projective complement $Q'$ with $Q\oplus Q'\simeq A^m$ and add $\Hyp(Q')$. Thus
\begin{equation}\label{main:finite_hyperbolic}
 P\perp \Hyp^m\simeq \Hyp^{m+1}
\end{equation}
for some finite $m$. This also gives the group-completion interpretation when alternating
Witt theory is defined by metabolic relations: each such relation is
hyperbolic by Lemma~\ref{main:metabolic}, and adding a projective
complement turns it into a finite free hyperbolic stabilization.

\proofstep{3. Cancellation in the stable range.}
If $m=0$, the desired conclusion is immediate, and $m=1$ is already the required frame. If $m\geq2$, choose a free hyperbolic pair on the left of \eqref{main:finite_hyperbolic}. Its image is a hyperbolic pair $(u,v)$ in the standard free space of rank $2m+2\geq6$. Bass elementary transitivity and the characteristic-free equality of elementary linear and symplectic column orbits give an elementary symplectic matrix taking $u$ to $e_1$. The latter equality is \cite[Lemma~2.11 and Theorem~3.9]{Gupta}.

\proofstep{4. The partners of the standard columns.}
After that change write $v=e_2+a e_1+w$, with $w$ in the standard perpendicular complement of $Ae_1+Ae_2$. The transformation fixing $e_1$, sending
\[
 e_2\longmapsto e_2+w+a e_1,
 \qquad z\longmapsto z+\langle w,z\rangle e_1
\]
on that complement is symplectic, with inverse obtained by replacing $(w,a)$ by $(-w,-a)$. Its inverse sends $v$ to $e_2$. Restricting the resulting isometry to the perpendicular complements gives
\[
 P\perp \Hyp^{m-1}\simeq \Hyp^m.
\]
Repeat until $m=1$. At each step the standard target has rank at least six, so the stable-range theorem applies. The final isometry is the required rank-four frame.
\end{proof}

\subsection{Completion of the theorem}

Stable freeness trivializes $\det P$ for every rank-two projective. Fix any of its orientations and apply Lemma~\ref{main:actual_frame}. Theorem~\ref{bridge:criterion}, with Theorem~\ref{global:naive_mw4}, shows that $P$ is free. The orientation can be realized by its basis as in the criterion's proof. Rank-one projectives are free because taking determinants in a stable trivialization gives $P\simeq A$. Rank-zero projectives are zero, since their localizations at all primes are zero. Ranks at least three are covered by Lemma~\ref{main:stable_free}. Together with \eqref{main:sp4_transitive}, this proves every assertion of Theorem~\ref{main:quillen}.

\begin{remark}
For a rank-two projective module, the proof constructs an isometry
$P\perp \Hyp\simeq \Hyp^2$ and applies the completion criterion to the
corresponding framed complement. The resulting basis can be rescaled
to induce any chosen determinant orientation.
\end{remark}