Initial exponents at a node lie in a quadrilateral

In $\mathbb C[[x,z]]$, let $u$ be a unit, $f$ with nonzero restrictions to both axes, and $g$ associated to $(u\cdot xz)^jf$. Let $d,H,t,k>0$ and $n$ with $\dim\mathbb C[[x,z]]/(f,xz)\le ndH$ and $n+jd=k$. If $p$ is the lexicographic initial exponent of $g$ for weight $t$, then $p$ lies in nodeQuadrilateral with vertices $(0,0)$, $(kdHt/(1+t),0)$, $(k/d,k/d)$, $(0,kdH/(1+t))$.

Notation. sectionIdeal k s hs v is the comap along sectionsMorphism of the ideal sheaf of the hyperplane with coefficients $v$; sectionCombination k s v is $\sum_j k(v_j)s_j$. nodeQuadrilateral a b c is the convex hull of $(0,0),(a,0),(c,c),(0,b)$. LexInitial c t e says that $c_e\ne0$ and $e$ minimizes $p_1+tp_2$ among exponents with nonzero coefficient, ties broken by the smaller second coordinate.

Formalization Note The statement is verbatim from OpenAI's Lean development, with Definitions files of this development imported in place of the upstream modules; these are supporting code for the statement.