Recovering all derivatives of order $N$ from the top $y$-derivatives

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).

Let $z$ be smooth on an open set $U$ and satisfy $\det H=KE$ with $H_{yy}\ne0$ there. Let $V\subseteq U\cap S$ be measurable, $N\ge7$, $C\ge0$, $B\ge1$. Suppose the derivatives through order $N-2$ of the six-variable function $P$ at the solution jet are bounded by $C$ on $V$, that $z$ has coordinate derivatives through order $N-3$ bounded by $B$ on $V$, that all derivatives of order at most $N-1$ have $L^2(V)$ norm at most $H$, and that $\partial_y^Nz$ and $\partial_x\partial_y^{N-1}z$ have $L^2(V)$ norm at most $H_{\mathrm{top}}$. Then all coordinate derivatives of $z$ of order at most $N$ have $L^2(V)$ norm at most an explicit budget depending only on $C,B,H,H_{\mathrm{top}},N$.

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