\documentclass[11pt,a4paper]{article} \usepackage[T1]{fontenc} \usepackage{lmodern,amsmath,amssymb,amsthm,mathtools} \usepackage[margin=27mm]{geometry} \usepackage{microtype,booktabs,tabularx,enumitem,graphicx,placeins} \usepackage[numbers,sort&compress]{natbib} \usepackage{xcolor} \usepackage[colorlinks=true,linkcolor=blue!45!black,citecolor=blue!45!black,urlcolor=blue!45!black]{hyperref} \hypersetup{pdfauthor={Sida He},pdftitle={Stability and Convergence of a Regularized Immersed Boundary Method under Dynamic Cartesian Refinement. Part I: Fixed Geometry},pdfsubject={Research manuscript v0.3.3: fixed geometry, prescribed disk rotation, numerical verification and Lean-checked algebra},pdfkeywords={immersed boundary, adaptive mesh refinement, Stokes, convergence, Lean, manufactured solution}} \usepackage{fancyhdr} \pagestyle{fancy}\fancyhf{}\fancyhead[L]{\small Regularized immersed boundaries on changing Cartesian spaces} \fancyhead[R]{\small Research draft v0.3.3}\fancyfoot[C]{\thepage} \setlength{\headheight}{14pt} \setlength{\parskip}{3pt} \setlist{nosep,leftmargin=*} \newtheorem{theorem}{Theorem}[section] \newtheorem{lemma}[theorem]{Lemma} \newtheorem{proposition}[theorem]{Proposition} \newtheorem{corollary}[theorem]{Corollary} \theoremstyle{definition}\newtheorem{definition}[theorem]{Definition} \theoremstyle{remark}\newtheorem{remark}[theorem]{Remark} \newcommand{\R}{\mathbb R} \newcommand{\N}{\mathbb N} \newcommand{\eps}{\varepsilon} \newcommand{\Om}{\Omega} \newcommand{\Gam}{\Gamma} \newcommand{\curl}{\operatorname{curl}} \newcommand{\divg}{\operatorname{div}} \newcommand{\supp}{\operatorname{supp}} \newcommand{\dist}{\operatorname{dist}} \newcommand{\ip}[2]{\left(#1,#2\right)} \newcommand{\norm}[1]{\left\lVert#1\right\rVert} \newcommand{\dual}[2]{\left\langle#1,#2\right\rangle} \newcommand{\ubar}{\overline u} \newcommand{\Q}{\mathbb Q} \newcommand{\calA}{\mathcal A} \newcommand{\calT}{\mathcal T} \newcommand{\calD}{\mathcal D} \newcommand{\calS}{\mathcal S} \newcommand{\calX}{\mathcal X} \newcommand{\calZ}{\mathcal Z} \DeclareMathOperator*{\esssup}{ess\,sup} \title{Stability and Convergence of a Regularized Immersed Boundary Method\protect\\under Dynamic Cartesian Refinement.\protect\\Part I: Fixed Geometry} \author{Sida He\\[3pt] \small Huawei Technologies Co., Ltd.\\ \small\href{mailto:hesida1@huawei.com}{\texttt{hesida1@huawei.com}}\\ \small ORCID: \href{https://orcid.org/0000-0003-0849-6592}{0000-0003-0849-6592}} \date{27 October 2026\\\small Research preprint, version 0.3.3} \begin{document} \maketitle \noindent{\small\textbf{Disclosure:} Primarily AI-generated text. The author reports no understanding of the proofs; see the disclosure at the end of this manuscript.}\par\medskip \begin{abstract} We analyze a conforming variational immersed boundary discretization of the two-dimensional unsteady Stokes equations with a fixed interface. Exactly divergence-free velocities are obtained from Cartesian bicubic Hermite streamfunctions; regularized surface moments impose the boundary condition, and backward Euler time stepping uses constrained orthogonal transfer. Arbitrary local fine-scale enrichments may be added or removed at every step while the complete coarse space is retained. For homogeneous interface data, a common coarse comparison family yields an exact energy identity, a physical no-slip defect of order $\sqrt{\eps}+\sqrt{\ell}$, and velocity convergence without a restriction coupling the time step to the number of mesh changes. We extend this analysis to a disk with prescribed time-dependent angular velocity. A coarse lifting reproduces rigid rotation exactly throughout every regularization support, independently of the refinement pattern and surface partition. Subtracting this lifting reduces the driven problem to the homogeneous constraint spaces with an explicitly controlled forcing perturbation. This gives driven stability, physical slip control, and a quantitative energy error estimate without assuming a uniform multiplier inf--sup condition. The method assumes exact integration and is not a standard staggered-grid AMR scheme. Manufactured unsteady stationary and rotating-disk calculations test the implementation and its quadrature sensitivity. General changes of interface geometry and fluid-driven rigid-body motion remain outside the analysis. \end{abstract} \noindent\textbf{Keywords:} immersed boundary method; dynamic mesh refinement; Stokes equations; prescribed rotation; constrained projection; regularization; convergence. \section{Introduction and precise scope} Regularized immersed boundary (IB) methods transfer information between a background fluid discretization and an independently represented interface. Adaptive mesh refinement introduces a second transfer: the fluid state must be represented in a different discrete space after refinement or coarsening. Stability of either transfer in isolation does not settle the accuracy of their composition. In particular, a small bulk $L^2$ error may remain appreciable after averaging across a thin regularization layer. The relevant ingredients have substantial prior theory. Peskin's formulation supplies the regularized coupling structure \citep{peskin2002}. Rigorous IB convergence theory includes Mori's velocity estimates for periodic Stokes flow and a small-amplitude dynamic problem \citep{mori2008}, the analysis of discrete-delta properties and local accuracy by Liu and Mori \citep{liumori2012}, and their stationary Stokes velocity and pressure estimates in $L^p$ \citep{liumori2014}. More recently, Li, Pan, and Ruiz-\'{A}lvarez analyzed stationary Stokes discretizations with prescribed outer boundary velocity \citep{lipan2025}. In that setting the singular interface force is given; here the interface reaction is determined through regularized velocity constraints. These works establish essential IB accuracy results, but do not supply the changing-space argument used below. Prescribed rigid motion in a background-domain multiplier formulation also has a long history \citep{glowinski1997}. Constraint formulations for rigid bodies and their mobility operators were studied by Kallemov et al.\ \citep{kallemov2016}; their reported implementation used uniform grids. Dynamic-mesh Stokes error analysis, including errors introduced by Helmholtz and Stokes projections, predates the present work \citep{brenner2014}. General stable transfer operators for dynamic AMR were analyzed by Lundquist et al.\ \citep{lundquist2021}, and projection jumps also appear in analyses of remeshed moving-domain problems \citep{gawlik2015}. Neither projection contractivity nor the observation that remeshing errors can accumulate is a new claim here. The neighboring adaptive fictitious-domain literature is equally important. Berrone et al.\ \citep{berrone2019} proved optimal adaptive convergence for an elliptic fictitious-domain formulation with an unknown boundary multiplier. Heltai and Lei developed regularization error estimates \citep{heltai2020} and an adaptive analysis for regularized forcing data \citep{heltai2023}. Their setting emphasizes that the regularization width and the bulk mesh size must be tracked separately. On the algorithmic side, adaptive IB methods go back at least to Roma, Peskin, and Berger \citep{roma1999}. Zeng, Bhalla, and Shen developed a DLM--IB framework on dynamically adaptive collocated grids, including subcycling and non-subcycling time advancement \citep{zeng2022}; IB, multiple resolution levels, and lattice Green functions have also been combined \citep{hou2024}. The present analysis is for a different conforming realization and is not a convergence proof for those implementations. It does not claim that IB with AMR is new. Computational IB studies also motivate distinguishing boundary enforcement from bulk flow accuracy. He, Yang, Sotiropoulos, and Shen \citep{he2022multiphase} introduced an explicit immersed pressure boundary condition to mitigate spurious penetration through thin flexible structures in two-phase flow. For fixed geometries, Yang et al.\ \citep{yang2021step} coupled large-eddy simulation with IB for a backward-facing step, while Chen et al.\ \citep{chen2025airfoil} used a level-set-based IB method to study airfoil flow transition and vortex evolution. He, Liu, and Shen \citep{he2022canopy} resolved flexible-stem canopy flows with IB, and Zheng et al.\ \citep{zheng2024swimmers} studied a prescribed flapping plate near a free surface using the two-phase IB framework. These studies provide methodological and application context for accurate interface treatment; their turbulent, multiphase, or deforming-body configurations are not covered by the present Stokes analysis. In particular, their computational results are not used as analytical premises for our convergence proof. Our result concerns a deliberately specified conforming method. The main construction is a family of coarse, divergence-free comparison functions that vanishes on a collar containing every regularization support used during the computation. These functions satisfy all discrete boundary moments exactly, even when the regularization width and surface partition change. Orthogonal transfer preserves their inner products. We use this fact to obtain estimates with no factor counting refinement or coarsening events. The approximation is constructed, rather than postulated through a mesh-uniform constraint inf--sup assumption. There are three restrictions with practical consequences. First, the Cartesian velocity space is generated by $C^1$ streamfunctions and is not a MAC space. Second, boundary conditions are variational moments with exact integrals, not point-marker equations evaluated by a quadrature rule. Third, the interface geometry is fixed. The stationary-body analysis is extended to prescribed rotation of a circular disk, whose boundary as a geometric set does not move. The common collar construction does not provide the corresponding argument for translation or rotation of a noncircular body. These restrictions make it possible to separate a complete theorem from implementation-specific questions that remain open. The prescribed-rotation extension is a fixed-geometry result, not a general moving-body theorem. We construct a common discrete lifting from a cutoff quadratic streamfunction, so that the nonzero regularized moments are feasible for every admissible mesh configuration. The transformed forcing retains both the angular-acceleration term and the endpoint viscous lifting term. The resulting convergence proof uses the homogeneous theory with a vanishing forcing perturbation. The background-domain extension includes prescribed interior forcing to represent rigid rotation; no conclusion about a physical torque is inferred from an uncorrected interface multiplier. The analysis does not prescribe an error-based marking rule. It permits arbitrary choices of the admissible local enrichments, and therefore concerns stability and convergence under dynamic adaptation, not adaptive optimality. The spatial rate is expressed in the size of the retained coarse grid. Refining a small patch while holding the coarse grid fixed is not a convergence sequence covered by our limit theorem. \section{Continuous problem and regularized constraints}\label{sec:setting} Let $\Omega=(0,1)^2$. Let $B\Subset\Omega$ be a simply connected body with a connected $C^5$ boundary $\Gamma$, and put $F=\Omega\setminus\overline B$. The smoothness assumption is convenient for the quantitative collar construction; weaker assumptions suffice for several intermediate results. Define \begin{align} U&=\{v\in H^1_0(\Omega)^2:\divg v=0\}, &\norm v_U&=\norm{\nabla v}_{L^2(\Omega)},\label{eq:U}\\ V&=\{v\in U:\gamma_\Gamma v=0\}, &H&=\overline V^{\,L^2(\Omega)^2},\label{eq:V}\\ a(v,w)&=\nu\ip{\nabla v}{\nabla w}_{L^2(\Omega)},&&\nu>0.\label{eq:a} \end{align} We write $\norm\cdot_0$ for the bulk $L^2$ norm. By Poincare's inequality, $\norm\cdot_U$ is equivalent to the $H^1$ norm on $U$. Given $u_0\in H$ and $f\in L^2(0,T;U')$, the target problem is \begin{equation}\label{eq:weak} u\in L^2(0,T;V)\cap C([0,T];H),\qquad \dual{\partial_t u}{v}+a(u,v)=\dual f v\quad(v\in V),\qquad u(0)=u_0. \end{equation} The derivative belongs to $L^2(0,T;V')$. Applying the coercive evolution-form theorem of J.-L.\ Lions to $V\subset H\subset V'$ gives a unique solution; see \citet[Theorem 10.9]{brezis2011}. The Hilbert-triple chain rule for variational evolution equations \citep[Chapter 3]{lionsmagenes1972} then gives the energy identity \begin{equation}\label{eq:continuous-energy} \tfrac12\norm{u(t)}_0^2+\int_0^t a(u,u)\,ds =\tfrac12\norm{u_0}_0^2+\int_0^t\dual f u\,ds. \end{equation} This is a background-domain description. To represent a rigid solid rather than a second interior fluid, take $u_0=0$ in $B$ and require $f$ to vanish on tests supported in $B$. The interior subproblem then has zero data and its solution is zero. In particular, a bulk force supported in $F$, extended by zero into $B$, has the required property. The pressure is eliminated by testing in $U$; the theory below does not establish a pressure estimate. Fix a nonnegative, even $\rho\in C_c^\infty(\R^2)$ with $\int\rho=1$ and support in the unit ball. Set $\rho_\eps(x)=\eps^{-2}\rho(x/\eps)$. If $Ev$ is the zero extension of $v\in H^1_0(\Omega)^2$, define \begin{equation}\label{eq:J} J_\eps v=\gamma_\Gamma(\rho_\eps*Ev),\qquad b_\eps(v,\mu)=\int_\Gamma \mu\cdot J_\eps v\,ds. \end{equation} The force operator is the adjoint of this variational interpolation, retaining the power-compatible coupling of the IB formulation \citep{peskin2002}. Kernel moment conditions and their consequences for discrete IB accuracy are studied in \citet{liumori2012}; our operator is instead an exact continuum convolution. No sampling or quadrature operator is included in \eqref{eq:J}. Let $\mathcal P$ partition $\Gamma$ into arclength panels, and let $\ell$ be the largest panel length. Let $\Lambda_\mathcal P$ be the space of vector-valued panelwise constants and $\Pi_\mathcal P$ the $L^2(\Gamma)^2$ orthogonal projector onto it. The constraint is \begin{equation}\label{eq:moments} b_\eps(v_h,\mu)=0\quad\hbox{for all }\mu\in\Lambda_\mathcal P, \qquad\hbox{equivalently }\Pi_\mathcal P J_\eps v_h=0. \end{equation} The surface panels need not coincide with bulk cell intersections. Throughout a run the widths $\eps$, the panels, and the local refinement patches may change. Their maximal widths over that run will be denoted by $\bar\eps$ and $\bar\ell$. \section{A physical interface-defect estimate}\label{sec:trace} \begin{lemma}[Uniform regularized trace and moment defect]\label{lem:trace} For sufficiently small $\eps>0$ and $v\in U$, \begin{align} \norm{J_\eps v}_{H^{1/2}(\Gamma)}&\le C\norm v_U,\label{eq:uniformtrace}\\ \norm{\gamma_\Gamma v-J_\eps v}_{L^2(\Gamma)}&\le C\sqrt\eps\,\norm v_U.\label{eq:tracediff} \end{align} If \eqref{eq:moments} holds, then \begin{equation}\label{eq:slip} \norm{\gamma_\Gamma v}_{L^2(\Gamma)} \le C(\sqrt\eps+\sqrt\ell)\norm v_U. \end{equation} The constants depend on the fixed geometry and kernel, not on the bulk mesh, panel positions, or the number of panels. \end{lemma} \begin{proof} Zero extension is bounded from $H^1_0(\Omega)$ into $H^1(\R^2)$ \citep[Theorems 3.18--3.19]{ern2021}. Young's convolution inequality, also used in \citet[Lemma 3]{heltai2020}, gives uniform $H^1$ boundedness of convolution. The trace theorem \citep[Theorem 3.10(iii)]{ern2021}, applied on a fixed neighborhood of $\Gamma$, proves \eqref{eq:uniformtrace}. For $w=Ev-\rho_\eps*Ev$, the first-order mollification bound \citep[Lemma 4, equation (8), with $s=1$]{heltai2020} and convolution boundedness give \[ \norm w_{L^2(\R^2)}\le C\eps\norm v_U, \qquad \norm w_{H^1(\R^2)}\le C\norm v_U. \] The multiplicative trace inequality yields the following bound on a fixed neighborhood of $\Gamma$. One obtains this version by transferring the face inequality of \citet[Lemma 12.15]{ern2021}, with $p=2$, through fixed smooth charts and a finite partition of unity; chart derivatives are absorbed into the $H^1$ norm: \[ \norm{\gamma_\Gamma w}_{L^2(\Gamma)}^2 \le C\norm w_{L^2(\R^2)}\norm w_{H^1(\R^2)} \le C\eps\norm v_U^2. \] This proves \eqref{eq:tracediff}. The panel estimate is the fractional Poincare inequality \citep[Lemma 3.26]{ern2021}. For completeness, its direct proof here is short: on an arclength interval $I$ of length $\ell_I$, the panel average $z_I$ satisfies \[ \int_I|z-z_I|^2\,ds =\frac1{2\ell_I}\int_I\!\int_I|z(s)-z(t)|^2\,ds\,dt \le\frac{\ell_I}{2}\int_I\!\int_I \frac{|z(s)-z(t)|^2}{|s-t|^2}\,ds\,dt. \] Summing over panels, with the equivalent arclength definition of the surface fractional norm, proves \[ \norm{(I-\Pi_\mathcal P)z}_{L^2(\Gamma)} \le C\sqrt\ell\,\norm z_{H^{1/2}(\Gamma)}. \] Under \eqref{eq:moments}, $J_\eps v=(I-\Pi_\mathcal P)J_\eps v$. Combine this observation with \eqref{eq:uniformtrace}, \eqref{eq:tracediff}, and the triangle inequality. \end{proof} Estimate \eqref{eq:slip} concerns the physical trace of the reconstructed conforming velocity, not a discrete residual that vanishes by definition. No multiplier inf--sup estimate is used. The estimate is useful in a time-integrated norm: viscous dissipation bounds $\int\norm{u_h}_U^2$, but does not by itself bound the gradient at each isolated remeshing instant. The distinction between a satisfied discrete boundary equation and physical impermeability is also relevant to the spurious-penetration issue addressed computationally by \citet{he2022multiphase}. Their remedy acts through an immersed pressure boundary condition in a two-phase finite-difference solver. Here \eqref{eq:slip} controls the full velocity trace by regularized moments and viscous energy; it is a different mechanism and does not analyze that pressure-boundary algorithm. \input{sections/spaces} \section{Time stepping and exact energy balance}\label{sec:energy} Choose a time partition $0=t_0<\cdots0$, and any surface panel partition $\mathcal P^n$. Let \begin{equation}\label{eq:Z} Z^n=\{v_h\in X_{h,\mathcal A^n}:\Pi_{\mathcal P^n}J_{\eps_n}v_h=0\}, \qquad P^n:L^2(\Omega)^2\longrightarrow Z^n \end{equation} be the exact bulk $L^2$ orthogonal projector. All spaces use the same physical integrals and the same bilinear form $a$; in particular the mass inner product is not changed by mass lumping. Set $u^0=P^0u_0$ and $f^n=\tau_n^{-1}\int_{t_{n-1}}^{t_n}f(t)\,dt$. The scheme is \begin{equation}\label{eq:scheme} u^n\in Z^n,\qquad \ip{(u^n-P^nu^{n-1})/\tau_n}{v_h}+a(u^n,v_h)=\dual{f^n}{v_h} \quad(v_h\in Z^n). \end{equation} All bulk inner products without subscripts are in $L^2(\Omega)^2$. Backward Euler with projection of the old velocity onto the new space is an established dynamic-mesh Stokes construction; compare \citet[Algorithm 2.2]{brenner2014}. Here the projector also enforces the regularized interface moments. Because the mass form plus $\tau_na$ is positive definite on $Z^n$, this problem has a unique velocity, whether or not the surface constraints are linearly independent. Equivalently, one may solve on $X_{h,\mathcal A^n}$ with a multiplier in $\Lambda_{\mathcal P^n}$. In finite dimensions, the residual functional of the constrained minimizer vanishes on the kernel of the constraint map and therefore belongs to the range of its transpose. A multiplier exists, although it may not be unique. This observation is not a claim of uniform conditioning or convergence of that multiplier. Testing by the current velocity and using dual coupling to cancel constraint terms are established energy arguments; see, for example, \citet[Proposition 3]{boffi2015} in a distributed-multiplier elastic FSI setting. We use the same elementary energy principle, not their elastic-body theorem. The identity below additionally keeps the loss from transfer between our changing constraint spaces; its contractive-transfer mechanism is consistent with \citet[Section 2]{lundquist2021}. \begin{proposition}[Energy identity]\label{prop:energy} For every step of \eqref{eq:scheme}, \begin{equation}\label{eq:energy} \norm{u^n}_0^2-\norm{u^{n-1}}_0^2 +\norm{u^n-u^{n-1}}_0^2+2\tau_na(u^n,u^n) =2\tau_n\dual{f^n}{u^n}. \end{equation} Moreover, \begin{equation}\label{eq:lossdecomposition} \norm{u^n-u^{n-1}}_0^2 =\norm{u^n-P^nu^{n-1}}_0^2 +\norm{(I-P^n)u^{n-1}}_0^2. \end{equation} Consequently, \begin{equation}\label{eq:energybound} \max_{0\le n\le N}\norm{u^n}_0^2 +\sum_{n=1}^N\tau_n\norm{u^n}_U^2 +\sum_{n=1}^N\norm{u^n-u^{n-1}}_0^2 \le C_\nu\left(\norm{u_0}_0^2+\norm f_{L^2(0,T;U')}^2\right). \end{equation} \end{proposition} \begin{proof} Orthogonality gives $\ip{P^nu^{n-1}}{u^n}=\ip{u^{n-1}}{u^n}$. Test \eqref{eq:scheme} with $u^n$ and apply \[ 2\ip{x-y}{x}=\norm x_0^2-\norm y_0^2+\norm{x-y}_0^2. \] This is \eqref{eq:energy}. The two terms $u^n-P^nu^{n-1}\in Z^n$ and $P^nu^{n-1}-u^{n-1}\perp Z^n$ are orthogonal, proving \eqref{eq:lossdecomposition}. Sum \eqref{eq:energy}, use Young's inequality on the right-hand side, and use Jensen's inequality for the time averages of $f$. \end{proof} \begin{corollary}[Time-integrated physical no-slip defect]\label{cor:slip} Let $U_h(t)=u^n$ on $(t_{n-1},t_n]$. Then \begin{equation}\label{eq:integratedslip} \norm{\gamma_\Gamma U_h}_{L^2(0,T;L^2(\Gamma))} \le C_{\nu,\Gamma,\rho}(\sqrt{\bar\eps}+\sqrt{\bar\ell}) \left(\norm{u_0}_0+\norm f_{L^2(0,T;U')}\right). \end{equation} \end{corollary} \begin{proof} Apply Lemma~\ref{lem:trace} on each time interval and then \eqref{eq:energybound}. \end{proof} \begin{lemma}[The common comparison cancels transfer]\label{lem:cancel} If $w_h\in Z^n$ for every $n$, then \begin{equation}\label{eq:cancel} \ip{P^nu^{n-1}}{w_h}=\ip{u^{n-1}}{w_h},\qquad \ip{u^n-u^{n-1}}{w_h} =\tau_n\{\dual{f^n}{w_h}-a(u^n,w_h)\}. \end{equation} If $z_h(t)$ takes values in a fixed subspace of every $Z^n$, then also $P^nz_h(t)=z_h(t)$ at all times. Thus no jump of the comparison function is introduced at a mesh change. \end{lemma} \begin{proof} Both statements follow directly from the defining orthogonality of $P^n$. The collar construction in Section~\ref{sec:spaces} supplies the comparison functions required by this lemma. \end{proof} \input{sections/convergence} \input{sections/rates} \input{sections/fixed_geometry} \input{sections/numerics} \input{numerics/rotation/rotation_section} \section{What the result does and does not imply}\label{sec:limits} The estimates permit a completely different set of enriched coarse cells at every time step. Neither nesting in time nor a bound on the number of coarsening events is required. Surface panels and regularization widths may change at the same instants. Their influence enters through their maximal widths and through the common collar used in the proof, rather than through a sum of eventwise consistency errors. This conclusion is conditional on a concrete structural choice, not on arbitrary interpolation: the full coarse space is retained, the method is conforming in a common physical Hilbert space, and transfer is the exact constrained $L^2$ projection. General remeshing methods need not share a dense fixed family of test functions. The error accumulation documented in dynamic-mesh analyses \citep{brenner2014,gawlik2015} is therefore not contradicted. The half-order spatial estimate does not quantify the gain obtained by an adaptive marking rule. It is a robust upper bound in terms of the coarse grid and a collar construction. It does not establish optimality, a pointwise velocity rate, a uniform-in-time physical trace rate, pressure convergence, or convergence of the multiplier. The results do not imply that a poorly conditioned multiplier system is harmless for finite-precision computation. They show that velocity convergence can be proved without assuming an inf--sup estimate for that system. The exact-integration qualification is essential. A marker implementation introduces an additional consistency term, for example \[ J_{h,\eps}^{\mathrm{quad}}v_h-J_\eps v_h, \] after an appropriate surface reconstruction. That term is absent from the exact-integral method and has not been estimated here. Section~\ref{sec:numerics} checks quadrature sensitivity for the reported computations, without adding a quadrature-consistency theorem. The same theoretical limitation applies to approximate projections, changing mass quadrature, solver tolerances, subcycling, and conventional coarse--fine MAC stencils. Proving bounds for these modifications is a separate extension, not a consequence of replacing their matrices by the notation in this paper. Prescribed rotation of a fixed disk is covered by the common lifting constructed in Section~\ref{sec:fixed-geometry}. For general prescribed rigid-body motion, the interface itself moves; a collar of the entire swept interface is generally too large to be a dense approximation device. A time-dependent recovery construction and its transport estimates are therefore needed. Fluid-driven motion also requires consistent momentum and total-energy coupling, including the treatment of fictitious interior fluid. These are future research modules, not consequences asserted by the fixed-geometry theorem. For example, the prescribed heave and pitch of a plate in \citet{zheng2024swimmers} change its geometric interface, unlike rotation of a circular disk about its center. That application therefore requires a moving-geometry analysis even before its free-surface and nonlinear-flow effects are considered. Likewise, the flexible stems in \citet{he2022canopy} require structural dynamics beyond the rigid-body scope of this series. \section{Formal verification and reproducibility}\label{sec:lean} \input{sections/formal_status} \appendix \section{A kernel obstruction to an unrestricted multiplier assumption}\label{app:kernel} The following elementary calculation motivates avoiding an unproved multiplier stability hypothesis. It is a diagnostic example, not a separate claim of novelty; Fourier analysis of IB kernels and planar boundaries has an established literature \citep{hua2022}, and rigid-body mobility conditioning is discussed in \citet{kallemov2016}. On an even periodic row with $N$ aligned markers at spacing $h$, the integer samples of the standard four-point Peskin kernel are $\phi(0)=1/2$, $\phi(\pm1)=1/4$, and zero at all other integers. The tangential convolution is therefore \[ (A\lambda)_j=\tfrac14\lambda_{j-1}+\tfrac12\lambda_j+\tfrac14\lambda_{j+1}. \] For $\lambda_j=(-1)^j$, $A\lambda=0$. A tensor-product spreading operator on a straight aligned interface consequently has a nonzero alternating force mode whose spread is zero. This is a genuine kernel of the coupling map, independent of the downstream fluid solver. The Fourier symbol is \[ m(\theta)=\tfrac12+\tfrac12\cos\theta=\cos^2(\theta/2). \] After deleting the exact Nyquist mode, the neighboring mode still has \[ m(\pi-2\pi/N)=\sin^2(\pi/N)\longrightarrow0. \] Thus deleting the exact kernel alone does not produce a uniform $\ell^2$ inverse bound for this tangential smoothing map. This calculation does not determine the inf--sup constant of every IB formulation, every marker placement, or every Sobolev-scaled multiplier norm. Nor does a multiplier null mode prevent existence or uniqueness of the constrained velocity. It does rule out an unrestricted claim that all marker-force modes remain uniformly observable for all familiar kernel/grid configurations. \input{sections/publication_disclosure} \begin{thebibliography}{34} \providecommand{\natexlab}[1]{#1} \providecommand{\url}[1]{\texttt{#1}} \expandafter\ifx\csname urlstyle\endcsname\relax \providecommand{\doi}[1]{doi: #1}\else \providecommand{\doi}{doi: \begingroup \urlstyle{rm}\Url}\fi \bibitem[Peskin(2002)]{peskin2002} Charles~S. Peskin. \newblock The immersed boundary method. \newblock \emph{Acta Numerica}, 11:\penalty0 479--517, 2002. \newblock \doi{10.1017/S0962492902000077}. \bibitem[Mori(2008)]{mori2008} Yoichiro Mori. \newblock Convergence proof of the velocity field for a {Stokes} flow immersed boundary method. \newblock \emph{Communications on Pure and Applied Mathematics}, 61\penalty0 (9):\penalty0 1213--1263, 2008. \newblock \doi{10.1002/cpa.20233}. \bibitem[Liu and Mori(2012)]{liumori2012} Yang Liu and Yoichiro Mori. \newblock Properties of discrete delta functions and local convergence of the immersed boundary method. \newblock \emph{SIAM Journal on Numerical Analysis}, 50\penalty0 (6):\penalty0 2986--3015, 2012. \newblock \doi{10.1137/110836699}. \bibitem[Liu and Mori(2014)]{liumori2014} Yang Liu and Yoichiro Mori. \newblock {\(L^p\)} convergence of the immersed boundary method for stationary {Stokes} problems. \newblock \emph{SIAM Journal on Numerical Analysis}, 52\penalty0 (1):\penalty0 496--514, 2014. \newblock \doi{10.1137/130911329}. \bibitem[Li et~al.(2025)Li, Pan, and Ruiz-{\'A}lvarez]{lipan2025} Zhilin Li, Kejia Pan, and Juan Ruiz-{\'A}lvarez. \newblock Convergence study of {IB} methods for {Stokes} equations with prescribed velocity boundary conditions. \newblock \emph{IMA Journal of Numerical Analysis}, 45\penalty0 (6):\penalty0 3766--3799, 2025. \newblock \doi{10.1093/imanum/drae101}. \bibitem[Glowinski et~al.(1997)Glowinski, Pan, and P{\'e}riaux]{glowinski1997} Roland Glowinski, Tsorng-Whay Pan, and Jacques P{\'e}riaux. \newblock A {Lagrange} multiplier/fictitious domain method for the numerical simulation of incompressible viscous flow around moving rigid bodies: {(I)} case where the rigid body motions are known a priori. \newblock \emph{Comptes Rendus de l'Acad{\'e}mie des Sciences, S{\'e}rie I, Math{\'e}matique}, 324\penalty0 (3):\penalty0 361--369, 1997. \newblock \doi{10.1016/S0764-4442(99)80376-0}. \bibitem[Kallemov et~al.(2016)Kallemov, Bhalla, Griffith, and Donev]{kallemov2016} Bakytzhan Kallemov, Amneet Pal~Singh Bhalla, Boyce~E. Griffith, and Aleksandar Donev. \newblock An immersed boundary method for rigid bodies. \newblock \emph{Communications in Applied Mathematics and Computational Science}, 11\penalty0 (1):\penalty0 79--141, 2016. \newblock \doi{10.2140/camcos.2016.11.79}. \newblock URL \url{https://arxiv.org/abs/1505.07865}. \bibitem[Brenner et~al.(2014)Brenner, B{\"a}nsch, and Bause]{brenner2014} Andreas Brenner, Eberhard B{\"a}nsch, and Markus Bause. \newblock A priori error analysis for finite element approximations of the {Stokes} problem on dynamic meshes. \newblock \emph{IMA Journal of Numerical Analysis}, 34\penalty0 (1):\penalty0 123--146, 2014. \newblock \doi{10.1093/imanum/drt001}. \newblock URL \url{https://d-nb.info/1113290293/34}. \bibitem[Lundquist et~al.(2021)Lundquist, Nordstr{\"o}m, and Malan]{lundquist2021} Tomas Lundquist, Jan Nordstr{\"o}m, and Arnaud Malan. \newblock Stable dynamical adaptive mesh refinement. \newblock \emph{Journal of Scientific Computing}, 86:\penalty0 43, 2021. \newblock \doi{10.1007/s10915-021-01414-1}. \bibitem[Gawlik and Lew(2015)]{gawlik2015} Evan~S. Gawlik and Adrian~J. Lew. \newblock Unified analysis of finite element methods for problems with moving boundaries. \newblock \emph{SIAM Journal on Numerical Analysis}, 53\penalty0 (6):\penalty0 2822--2846, 2015. \newblock \doi{10.1137/140990437}. \newblock URL \url{https://webpages.scu.edu/ftp/egawlik/pdf/GaLe2015c.pdf}. \bibitem[Berrone et~al.(2019)Berrone, Bonito, Stevenson, and Verani]{berrone2019} Stefano Berrone, Andrea Bonito, Rob Stevenson, and Marco Verani. \newblock An optimal adaptive fictitious domain method. \newblock \emph{Mathematics of Computation}, 88:\penalty0 2101--2134, 2019. \newblock \doi{10.1090/mcom/3414}. \bibitem[Heltai and Lei(2020)]{heltai2020} Luca Heltai and Wenyu Lei. \newblock A priori error estimates of regularized elliptic problems. \newblock \emph{Numerische Mathematik}, 146\penalty0 (3):\penalty0 571--596, 2020. \newblock \doi{10.1007/s00211-020-01152-w}. \newblock URL \url{https://arxiv.org/abs/1911.02293}. \bibitem[Heltai and Lei(2023)]{heltai2023} Luca Heltai and Wenyu Lei. \newblock Adaptive finite element approximations for elliptic problems using regularized forcing data. \newblock \emph{SIAM Journal on Numerical Analysis}, 61\penalty0 (2):\penalty0 431--456, 2023. \newblock \doi{10.1137/21M1455991}. \newblock URL \url{https://arxiv.org/abs/2110.15029}. \bibitem[Roma et~al.(1999)Roma, Peskin, and Berger]{roma1999} Alexandre~M. Roma, Charles~S. Peskin, and Marsha~J. Berger. \newblock An adaptive version of the immersed boundary method. \newblock \emph{Journal of Computational Physics}, 153\penalty0 (2):\penalty0 509--534, 1999. \newblock \doi{10.1006/jcph.1999.6293}. \bibitem[Zeng et~al.(2022)Zeng, Bhalla, and Shen]{zeng2022} Yadong Zeng, Amneet Pal~Singh Bhalla, and Lian Shen. \newblock A subcycling/non-subcycling time advancement scheme-based {DLM} immersed boundary method framework for solving single and multiphase fluid--structure interaction problems on dynamically adaptive grids. \newblock \emph{Computers \& Fluids}, 238:\penalty0 105358, 2022. \newblock \doi{10.1016/j.compfluid.2022.105358}. \bibitem[Hou and Colonius(2024)]{hou2024} Wei Hou and Tim Colonius. \newblock An adaptive lattice {Green's} function method for external flows with two unbounded and one homogeneous directions. \newblock \emph{Journal of Computational Physics}, 519:\penalty0 113370, 2024. \newblock \doi{10.1016/j.jcp.2024.113370}. \newblock URL \url{https://arxiv.org/abs/2402.13370}. \bibitem[He et~al.(2022{\natexlab{a}})He, Yang, Sotiropoulos, and Shen]{he2022multiphase} Sida He, Zixuan Yang, Fotis Sotiropoulos, and Lian Shen. \newblock Numerical simulation of interaction between multiphase flows and thin flexible structures. \newblock \emph{Journal of Computational Physics}, 448:\penalty0 110691, 2022{\natexlab{a}}. \newblock \doi{10.1016/j.jcp.2021.110691}. \bibitem[Yang et~al.(2021)Yang, He, Shen, and Luo]{yang2021step} Dandan Yang, Sida He, Lian Shen, and Xianwu Luo. \newblock Large eddy simulation coupled with immersed boundary method for turbulent flows over a backward facing step. \newblock \emph{Proceedings of the Institution of Mechanical Engineers, Part C: Journal of Mechanical Engineering Science}, 235\penalty0 (15):\penalty0 2705--2714, 2021. \newblock \doi{10.1177/0954406220954892}. \bibitem[Chen et~al.(2025)Chen, Lu, Wu, He, Xiao, Tong, and Kan]{chen2025airfoil} Jichang Chen, Zhiwei Lu, Bin Wu, Sida He, Tianhang Xiao, Mingbo Tong, and Kan Kan. \newblock Flow transition and vortex evolution of a symmetric airfoil at low {Reynolds} number and high angle of attack. \newblock \emph{Physics of Fluids}, 37\penalty0 (2):\penalty0 023603, 2025. \newblock \doi{10.1063/5.0246708}. \bibitem[He et~al.(2022{\natexlab{b}})He, Liu, and Shen]{he2022canopy} Sida He, Han Liu, and Lian Shen. \newblock Simulation-based study of turbulent aquatic canopy flows with flexible stems. \newblock \emph{Journal of Fluid Mechanics}, 947:\penalty0 A33, 2022{\natexlab{b}}. \newblock \doi{10.1017/jfm.2022.655}. \bibitem[Zheng et~al.(2024)Zheng, He, Zhao, Shen, and Zhu]{zheng2024swimmers} Kaiyuan Zheng, Sida He, Xizeng Zhao, Lian Shen, and Xiaojue Zhu. \newblock Free-surface-induced ground effect for flapping swimmers. \newblock \emph{Journal of Fluid Mechanics}, 997:\penalty0 A36, 2024. \newblock \doi{10.1017/jfm.2024.830}. \bibitem[Brezis(2011)]{brezis2011} Haim Brezis. \newblock \emph{Functional Analysis, {Sobolev} Spaces and Partial Differential Equations}. \newblock Universitext. Springer, New York, 2011. \newblock \doi{10.1007/978-0-387-70914-7}. \bibitem[Lions and Magenes(1972)]{lionsmagenes1972} Jacques-Louis Lions and Enrico Magenes. \newblock \emph{Non-Homogeneous Boundary Value Problems and Applications, Volume {I}}, volume 181 of \emph{Grundlehren der mathematischen Wissenschaften}. \newblock Springer, Berlin--Heidelberg, 1972. \newblock \doi{10.1007/978-3-642-65161-8}. \bibitem[Ern and Guermond(2021{\natexlab{a}})]{ern2021} Alexandre Ern and Jean-Luc Guermond. \newblock \emph{Finite Elements {I}: Approximation and Interpolation}, volume~72 of \emph{Texts in Applied Mathematics}. \newblock Springer, Cham, 2021{\natexlab{a}}. \newblock \doi{10.1007/978-3-030-56341-7}. \bibitem[Burman et~al.(2020)Burman, Hansbo, and Larson]{bfs2020} Erik Burman, Peter Hansbo, and Mats~G. Larson. \newblock Cut {Bogner--Fox--Schmit} elements for plates. \newblock \emph{Advanced Modeling and Simulation in Engineering Sciences}, 7:\penalty0 27, 2020. \newblock \doi{10.1186/s40323-020-00164-3}. \bibitem[Galdi(2011)]{galdi2011} Giovanni~P. Galdi. \newblock \emph{An Introduction to the Mathematical Theory of the {Navier--Stokes} Equations: Steady-State Problems}. \newblock Springer, 2 edition, 2011. \newblock \doi{10.1007/978-0-387-09620-9}. \bibitem[Boffi et~al.(2015)Boffi, Cavallini, and Gastaldi]{boffi2015} Daniele Boffi, Nicola Cavallini, and Lucia Gastaldi. \newblock The finite element immersed boundary method with distributed {Lagrange} multiplier. \newblock \emph{SIAM Journal on Numerical Analysis}, 53\penalty0 (6):\penalty0 2584--2604, 2015. \newblock \doi{10.1137/140978399}. \newblock URL \url{https://arxiv.org/abs/1407.5184}. \bibitem[Ern and Guermond(2021{\natexlab{b}})]{ern2021ii} Alexandre Ern and Jean-Luc Guermond. \newblock \emph{Finite Elements {II}: {Galerkin} Approximation, Elliptic and Mixed {PDEs}}, volume~73 of \emph{Texts in Applied Mathematics}. \newblock Springer, Cham, 2021{\natexlab{b}}. \newblock \doi{10.1007/978-3-030-56923-5}. \bibitem[Salari and Knupp(2000)]{salari2000} Kambiz Salari and Patrick Knupp. \newblock Code verification by the method of manufactured solutions. \newblock Technical Report SAND2000-1444, Sandia National Laboratories, 2000. \bibitem[de~Moura and Ullrich(2021)]{demoura2021} Leonardo de~Moura and Sebastian Ullrich. \newblock The {Lean} 4 theorem prover and programming language. \newblock In \emph{Automated Deduction---{CADE} 28}, volume 12699 of \emph{Lecture Notes in Computer Science}, pages 625--635, Cham, 2021. Springer. \newblock \doi{10.1007/978-3-030-79876-5_37}. \bibitem[{The mathlib Community}(2020)]{mathlib2020} {The mathlib Community}. \newblock The {Lean} mathematical library. \newblock In \emph{Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs}, CPP '20. ACM, 2020. \newblock \doi{10.1145/3372885.3373824}. \bibitem[Hua and Peskin(2022)]{hua2022} Mengjian Hua and Charles~S. Peskin. \newblock An analysis of the numerical stability of the immersed boundary method. \newblock \emph{Journal of Computational Physics}, 467:\penalty0 111435, 2022. \newblock \doi{10.1016/j.jcp.2022.111435}. \newblock URL \url{https://arxiv.org/abs/2111.15065}. \bibitem[He(2026{\natexlab{a}})]{partii2026} Sida He. \newblock Stability and convergence of a regularized immersed boundary method under dynamic cartesian refinement. {Part II}: General prescribed motion, 2026{\natexlab{a}}. \newblock Unpublished companion manuscript, preparation version 0.1.1, 27 October 2026. \bibitem[He(2026{\natexlab{b}})]{partiii2026} Sida He. \newblock Stability and convergence of a regularized immersed boundary method under dynamic cartesian refinement. {Part III}: Fluid-driven rigid-body motion, 2026{\natexlab{b}}. \newblock Unpublished companion manuscript, preparation version 0.1.1, 27 October 2026. \end{thebibliography} \end{document}