\section{Formal verification and reproducibility}\label{sec:formal}
The Lean companion was compiled with Lean~4.19.0 \citep{demoura2021} and a pinned Mathlib dependency \citep{mathlib2020}. It contains 35 checked theorems: the 26 unchanged algebraic results from Part~I and nine new statements in \texttt{MovingComparison.lean}. The new module formalizes current-space projection against a moving comparison, the equivalent physical affine weak equation, one-step and cumulative error estimates retaining the full error jump, and finite weighted Cauchy estimates. In particular, the previous comparison is not assumed to lie in the current subspace. The cumulative bound is derived from an explicit weak scheme and an explicit residual estimate, rather than asserted from the PDE theorem.

\begin{center}
\begin{tabularx}{\textwidth}{@{}p{.27\textwidth}X@{}}
\toprule
Component & Verified scope \\\midrule
Moving comparison & Actual orthogonal projection; ordinary comparison time difference; no nesting or previous-membership assumption.\\
Changing affine lift & Equivalence between the physical affine scheme and the centered error equation with reference $g_h^n+z_h^n$.\\
Error energy & Full squared error jumps and dissipation in one-step and summed estimates, conditional on the stated analytic residual bound.\\
Weighted sums & Finite weighted Cauchy and discrete trajectory-increment inequalities.\\
Inherited results & Linear/affine projection, step energy and discrete interface-error composition from Part~I.\\
\bottomrule
\end{tabularx}
\end{center}

The explicit axiom audit lists only \texttt{propext}, \texttt{Classical.choice} and \texttt{Quot.sound}; there are no \texttt{sorry} proofs or user-declared axioms. Source hashes, commands and actual build logs accompany the release. This does not formalize Sobolev traces, moving geometry, the collar or lift construction, continuous time regularity, or the full PDE convergence proof. Nor does Lean certify the numerical solver.

The repository includes this manuscript, BibTeX records, numerical source and raw results, figure-generation scripts, the Lean project and pinned dependencies, local validation reports, a release manifest, and a frozen Part~I v0.3.2 companion. Reproduction commands write new output to \texttt{build/} instead of overwriting archived data. A clean-source paper build and citation-order audit are part of the package checks. GitHub Actions configuration is provided, but a hosted CI run is not claimed before uploading the repository.

The detailed AI-use and human-understanding declaration at the end of this manuscript applies to this work. The internal mathematical and implementation reviews are not external peer review.