$L^2$ budget for the high remainder of the differentiated Darboux equation

Notation. $S=[-3,3]^2$ is the model square; a metric is a smooth positive matrix field $g$; $z$ is a scalar height; $H=\nabla_g^2z$ is its covariant Hessian; $K_g$ is the Gaussian curvature; $E=\det g\,(1-|dz|_g^2)$; $q=H_{xy}/H_{yy}$ is the Hessian quotient; $\kappa(x^2-h(y))$ is the model curvature; the patch box and the central box are the squares $[-1/10,1/10]^2$ and $[-1/5,1/5]^2$; the sheared coordinates are $\xi=x,\ \theta=y+q_0x$, with sheared height $z_s$; $L$ and $v_*$ are the class width and speed of (4.2); $\tilde g_\tau$ is the test metric (4.12) built from $g_*$; a bounded admissible height of bound $M$ is an admissible height with (4.1).

Fix $G,Z,M\ge0$, $d,c>0$ and $m$ with $m+3\ge8$. There is $C\ge0$ with the following property. Let $g$ be smooth and positive on an open $U\supseteq S$ and $z$ smooth on $U$, with $C^4$ bound $G$ for $g$ on $S$, $C^8$ bound $Z$ for $z$ on $S$, $|\det g|\ge d$ and $|H_{yy}|\ge c$ on $S$. Let $V\subseteq S$ be measurable with finite volume, suppose the derivatives of $g$ through order $m+5$ are bounded by $M$ on $V$, the height state factors of total order at most $m+1$ are bounded by $B\ge1$ on $V$, and those of order at most $m+3$ have $L^2(V)$ norm at most $H$. Then the remainder $\mathcal R_m$ in the $(m+3)$-times differentiated equation satisfies

where $\mathcal B$ is an explicit finite budget, and in particular $\mathcal R_m\in L^2(V)$.

This is the Sobolev product estimate for the lower-order terms in Lemma 3.3.

Formalization Note. This is the upstream Lean declaration OAI.SmoothLocal.HighEquation.exists_localized_actualHighRemainder_bound in lean/OAI/Geometry/IsometricImmersion/Energy/LocalizedRemainderL2.lean, stated verbatim; the Lean statement is authoritative for the precise hypotheses. It is an intermediate result of OpenAI's formalization.