Patch obstruction: metrics with no admissible height are dense

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_0$ be a metric on an open set $V$ with model curvature $K_{g_0}=\kappa(x^2-h(y))$ (and the standing hypotheses on $V\supseteq S$). For every nonempty open subset $O$ of the patch perturbation set, there is $\eta\in O$ such that $g=g_0+\eta$ is smooth and positive on $V$, satisfies $K_g<-\kappa/2$ on the central box, and admits no admissible height: for every $z$, there is no open $U\supseteq S$ on which $z$ is smooth and on $S$

This is the density assertion in Proposition 2.2, the whole-patch obstruction on the fixed square.

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