Finite-order bounds of the height on the lower cut $\theta=-r$

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 $g_*$ be smooth and positive on an open $V\supseteq S$ and fix $G,Z,d,c,e_0,\kappa,q_0,L,r$ with $|q_0|\le1/20$, $0<r<1/2$, $Lr\le1/20$ and $r$ small. For each order $n$ there is $C\ge0$ such that for all $N$ and $\delta>0$, for all sufficiently large $\tau$, the following holds for every metric $g_\tau$ with $C^4$ bound $G$ and $|\det g_\tau|\ge d$ on $S$, every cap-induction height $z$ and cap-induction flow $Y$ for $g_\tau$ with $|q(0)-q_0|\le1/(100L)$, whenever $g_\tau$ is within $\tau^{-\tau}$ in $C^\tau(S)$ of the test metric $\tilde g_\tau$: every coordinate derivative of order at most $n$ of $z$ at the sheared point $(x,-r)$, $|x|\le Lr$, is bounded by $C$.

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