hzero
plain-language theorem explainer
On the 2D L1 diamond of radius t, the only lattice vertex of height zero is the origin. Cosmology proofs that need a unique root for the descent criterion cite this. The argument is a direct omega discharge of |x|+|y|=0 on the integer coordinates.
Claim. For every radius $t \in \mathbb{N}$ and every lattice point $v$ in the diamond $\{(x,y)\in\mathbb{Z}^2 : |x|+|y|\le t\}$, if the L1 height of $v$ is zero then $v$ is the origin (the diamond centre).
background
The module proves a dimension-free bound on locked domains: monochromatic components of a charge field are at most the number of bichromatic (interface) edges plus one, on any connected finite world. Connectivity of the ambient lattice is discharged by a reusable descent criterion rather than by ad-hoc casework.
For the 2D engine lattice the world is the diamond: integer points inside the L1 ball of radius $t$, with 4-neighbour adjacency. Vertices are the subtype Vtx t of that ball. Height is the L1 norm $|x|+|y|$, which is graph distance to the origin. The centre is the origin, packaged as a vertex of every ball.
The descent package needs a unique zero of height: every positive-height cell steps along an edge to a strictly lower cell, and height zero occurs only at one root. That unique-zero fact is exactly the present lemma.
proof idea
Tactic proof by destructuring the subtype. A vertex is a pair $(x,y)$ in the ball; height expands to $x.\mathrm{natAbs}+y.\mathrm{natAbs}$. The hypothesis that this sum is zero forces $x=0$ and $y=0$ by omega. Subtype extensionality and substitution finish the equality with the centre.
why it matters
Feeds the diamond instance of the descent connectivity criterion. Downstream, clos_root_of_descent takes a unique-zero hypothesis of this shape and concludes every cell is in the equivalence closure of the root; connected_of_descent and mono_le_interface_of_descent then give the locked-domain bound on the diamond.
That bound closes the open connected-graph obligation left by the 2D/3D domain-coarsening scripts: components of the monochromatic graph are at most interface size plus one. In Recognition terms this is the recognition law's pull to the coarsest description, read as graph connectivity on the L1 ball, supporting the interface-cost accounting used elsewhere in the cosmology stack (total cost equals interface cost when bulk edges carry zero cost).
The lemma itself is elementary lattice arithmetic; its value is as the unique-root pin in the reusable connectivity package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.