\subsection{Outline of the proof}\label{intro:roadmap}

The proof begins with the distinction between stable freeness and
freeness. A finite free resolution over $R$ shows that every projective
module over $A$ is stably free (Lemma~\ref{main:stable_free}). The remaining
rank-two problem is treated by alternating forms. Lemma~\ref{main:actual_frame}
constructs an isometry $P\perp\Hyp\simeq\Hyp^2$, and
Theorem~\ref{bridge:criterion} shows that its rank-two complement $P$ is
free. The two vanishings in \eqref{main:arithmetic_endpoints} supply the
hypotheses for these steps.

\paragraph{Symplectic completion.}
Under its hypotheses, Theorem~\ref{bridge:criterion} applies to an integral
affine scheme of dimension at most three. Given the first vanishing in
\eqref{main:arithmetic_endpoints} and an isometry $P\perp \Hyp\simeq \Hyp^2$,
it proves that $P$ is free. Local symplectic stability places the first
obstruction in degree three. Milnor--Witt multiplication describes its
generic image in a space that classifies the underlying vector bundle;
a support argument then makes the induced map on degree-three
cohomology zero.

\paragraph{Integral degree-two $K$-theory.}
Part~II proves generic injectivity and image purity for Quillen
$K$-theory in degree two. Integral Adams operations with support give
finite-exponent bounds for the kernel and the image-purity defect.
Divisibility arguments eliminate torsion of order prime to the residue characteristic, and
local motivic comparisons treat the residue-prime part. At the dyadic
prime, explicit Dennis--Stein symbols supply the required torsion lifts.

\paragraph{Hermitian and local cohomological calculations.}
Part~III develops the comparison between genuine symmetric and
homotopy-symmetric theories. Supported genuine lifting and the local
comparison range give $W_{\mathrm{alt}}(A)=0$ in
Theorem~\ref{gw:global_walt}. Local motivic calculations identify the
edge maps and the residue exactness for the Milnor--Witt sheaf. In
degree four, the field comparison has cokernel
$H^0_{\mot}(F,\Z(2))$, whose local extension controls the residue image.

\paragraph{Global vanishing and freeness.}
Part~IV proves the field-complex vanishing and passes to the sheaf
cohomology in Theorem~\ref{global:naive_mw4} by bounding the supports
of the augmentation kernel and cokernel and the remaining cohomology
sheaves. Stable freeness and alternating Witt vanishing then give a
rank-four symplectic frame. The completion criterion trivializes its
rank-two complement and completes the proof.

The following table summarizes the principal results and their inputs.
\begin{center}
\renewcommand{\arraystretch}{1.18}
\begin{tabularx}{\textwidth}{@{}>{\raggedright\arraybackslash}p{0.36\textwidth}>{\raggedright\arraybackslash}X>{\raggedright\arraybackslash}p{0.22\textwidth}@{}}
\toprule
Result & Principal ingredients & Location\\
\midrule
Integral degree-two generic exactness & Supported operations, finite coefficients, and torsion lifts & Theorem~\ref{k2:thm:main}\\
Genuine lifts of supported symmetric classes & Coconnective surgery and the Frobenius grade bound & Theorem~\ref{gw:supported_lift}\\
$W_{\mathrm{alt}}(A)=0$ & Local negative groups and descent for the comparison fibre & Theorem~\ref{gw:global_walt}\\
Local Milnor--Witt residue exactness & Low-degree symbol maps and motivic edges & Theorems~\ref{loc:mw4_h2}, \ref{loc:mw4_h1}\\
$H^3_{\Zar}(A,\mathcal K_4^{\mathrm{MW}})=0$ & Field-complex vanishing and support bounds & Theorem~\ref{global:naive_mw4}\\
Freeness of the rank-two complement & Symplectic framing and the image criterion & Theorem~\ref{bridge:criterion}; Lemma~\ref{main:actual_frame}\\
\bottomrule
\end{tabularx}
\end{center}

Section~\ref{main:conclusion} assembles the argument. The completion
criterion of Section~\ref{bridge:section} is independent of the calculations
in Parts~II and~III: it uses their output only through the first vanishing
in \eqref{main:arithmetic_endpoints}. The alternating Witt vanishing is
used to construct the frame to which that criterion applies.