The accompanying Lean project checks the algebraic projection and discrete
energy layer of the analysis. It was compiled with Lean 4.19.0
\citep{demoura2021} and Mathlib \citep{mathlib2020}
at commit \texttt{c44e0c8} (the full hash is pinned in the companion).
The project contains 26 checked theorems in three source modules. The
\texttt{Energy.lean} module proves 12 Hilbert-space identities, scalar
energy estimates, telescoping statements, and a conditional composition of
the two interface bounds. The \texttt{Projection.lean} module proves five
results using Mathlib's actual orthogonal projection onto complete
subspaces, rather than treating all projection properties as hypotheses.
Finite-dimensional spaces such as $Z^n$ are complete and fit that setting. The new \texttt{Affine.lean} module adds nine checked statements for actual affine projections, the change of lifting, the centered prescribed-rotation equation, and its energy balances.

\begin{center}
\begin{tabularx}{\linewidth}{@{}p{0.40\linewidth}X@{}}
\toprule
Mathematical step & Scope of the checked result\\
\midrule
Common functions survive transfer & Subspace inclusion implies that the actual orthogonal projection fixes the common function and preserves its test moment.\\
Backward Euler energy & The Hilbert-space polarization identity and the tested step equation imply the exact energy balance.\\
Projection loss & Orthogonality splits the full jump into a time-step increment and a projection loss.\\
Changing spaces & The exact energy identity telescopes for an arbitrary sequence of complete subspaces; nesting is not assumed.\\
Residual accumulation & A supplied one-step energy inequality yields the cumulative bound without an additional event-count factor.\\
Prescribed rotation & The exact affine projector preserves homogeneous test moments; centering the discrete equation retains the angular-acceleration and endpoint viscous terms.\\
Driven energy & Centered energy and physical kinetic-energy identities include their respective forcing or prescribed-lift work terms; the centered balance telescopes on changing spaces.\\
Interface estimate & Given the regularization and panel-approximation inequalities, the moment constraint and triangle inequality yield the physical trace bound.\\
\bottomrule
\end{tabularx}
\end{center}

The final build and the explicit \texttt{\#print axioms} checks passed.
The listed foundational axioms are only \texttt{propext},
\texttt{Classical.choice}, and \texttt{Quot.sound}; there is no
\texttt{sorryAx} and no user-declared axiom. The companion contains the
pinned project manifests, source hashes, commands, and compiler logs.

This is not a Lean formalization of Theorems~\ref{thm:convergence} ,
\ref{thm:rate}, or the prescribed-rotation extension in their entirety. Zero extension, convolution and trace
estimates, fractional panel approximation, the finite element and collar
construction, solenoidal density, the evolution equation, and passage to
the strong limit are proved in the mathematical text. In particular, the
Lean theorem that composes the interface bounds does not establish its
analytic hypotheses. The verified layer checks an important part of the
argument but does not certify originality or replace review of the
remaining analysis.

The manuscript and companion were developed primarily by AI agents; the detailed disclosure at the end of this manuscript states the author's current understanding of the proofs. The
manufactured-solution computations in Section~\ref{sec:numerics} are
implementation checks and numerical illustrations, not formal proofs.
The reproducibility package contains the complete LaTeX sources,
bibliographic database, Lean sources, numerical solver, raw experiment
data, and independent implementation checks. Downloaded dependency caches
are excluded. The original 17 Lean theorems remain unchanged; nine affine identities were added for version 0.3. None of these theorems certifies the numerical implementation or the analytic construction of the common lifting.