\section{Machine-checked algebra and scope of verification}
\label{sec:formal-status}

The accompanying Lean project contains 48 kernel-checked theorems:
35 unchanged declarations inherited from Part~II and 13 additions for
the coupled formulation. The complete project was compiled with Lean
4.19.0 and a pinned Mathlib revision. The six proof modules were then
checked separately and their axiom dependencies printed. Every
declaration passed; the reported foundations are only
\texttt{propext}, \texttt{Classical.choice}, and \texttt{Quot.sound}.
There are no proof admissions or custom axioms. The compiler output,
dependency lockfile, source hashes, and exact commands are included
in the repository. Lean and Mathlib provide the verification framework
\citep{demoura2021,mathlib2020}.

The nine additions in \texttt{Coupled.lean} construct a genuine
Hilbert product using square-root mass coordinates, identify its
inner product and squared norm, and prove positive definiteness
under positive excess mass and inertia. The fluid Hilbert norm may
already contain $\rho_f$; a separate checked identity makes the
explicit encoding
$(\sqrt{\rho_f}\,u,\sqrt{m_e}\,V,\sqrt{I_e}\,\omega)$
and all three coefficients of \eqref{eq:mass-inner-product} visible.
The module also checks the exact step and cumulative energy identities
with Mathlib's actual orthogonal projector, the zero work of the
planar quarter-turn, and reaction-power cancellation using genuine
adjoint operators. At finite resolution the resulting positive norm
is the discrete energy surrogate; its identification with physical
energy requires the analytical interior-rigidity argument.

The four additions in \texttt{Recurrence.lean} combine energy and
pose-error inequalities and establish a discrete Gronwall estimate
with cumulative dissipation and the factor
$\exp(\sum_n\gamma_n)$. The nonnegative growth coefficients need
not have a uniformly bounded maximum. Their analytic bounds and the
consistency residuals are explicit hypotheses. A vector estimate for
the lagged kinematic update is checked with the stated normalization
$0<\tau_n\le1$; this normalization belongs to that error estimate,
not to the unrestricted discrete energy identity.

These checks establish the indicated algebra and finite-sum arguments,
not a formal proof of the full PDE convergence theorem. The physical
Eulerian inertia derivation, regularized volume and surface estimates,
pose alignment, moving-collar recovery, regularity assumptions, and
clearance bootstrap remain ordinary mathematical proofs. In particular,
zero gyroscopic work does not prove that the gyroscopic coefficient
has been derived correctly from the physical equations. The numerical
checks supply a further, finite-resolution assessment of the implemented
scheme; neither compiler acceptance nor those computations replace the
analytical hypotheses of the convergence theorem.