Every local immersion yields an admissible height on an oriented patch

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 a metric on the plane, $U$ a set containing $0$, and $F:\mathbb R^2\to\mathbb R^3$ a map which is a smooth isometric immersion of $(U,g)$ in the sense of the standing hypotheses. Let $D_n$ be the accumulating round disks and suppose $K_g<0$ in each open $D_n$ and $K_g=0$ on $\partial D_n$. Then for all $n_{\min},k_{\min}$ there are $n\ge n_{\min}$, $b\in\partial D_n$ and a unit vector $e\in\mathbb R^3$ normal to $F$ at $b$ with second fundamental form $\mathrm{II}_e(b)$ of rank exactly one, a rotation $R$ of the finite net, $k\ge k_{\min}$ and a centre $c$ among the oriented exterior centres such that the closed patch $\Phi(c,R,k)$ lies in $U$ and

where $\Phi(p)=c+\lambda_{n,k,R}Rp$. This is the geometric step reducing Theorem A to the whole-patch obstruction.

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