height
plain-language theorem explainer
On the 2D diamond of radius t (the L1 ball of lattice points), height is the L1 norm |x|+|y| of a vertex. It is the graph-distance potential toward the origin used by the descent-connectivity criterion. Anyone proving that the diamond is one component via a unique zero and strict descent edges cites it. The body is a one-line extraction of absolute coordinates from the subtype.
Claim. For radius $t\in\mathbb{N}$ and a lattice point $v=(x,y)$ in the diamond $\{(x,y)\in\mathbb{Z}^2:\,|x|+|y|\le t\}$, define $\mathrm{height}_t(v):=|x|+|y|$.
background
The module proves a dimension-free bound: on any finite connected world, the number of monochromatic (locked-domain) components is at most the number of bichromatic interface edges plus one. Connectivity of the ambient lattice is a hypothesis of the headline; for the engine's 2D diamond it is discharged by a reusable descent criterion.
The diamond of radius $t$ is the finite L1 ball $|x|+|y|\le t$ carved from a bounding box Finset. Its vertices are the subtype of lattice points in that ball (automatically finite and decidably equal). Height is the natural potential on those vertices: the L1 norm, which equals graph distance to the origin in the 4-neighbour grid.
Upstream, ball supplies the Finset and the vertex abbrev packages membership. The same L1 potential appears in the 3D octahedron story; here it is specialized to two coordinates.
proof idea
Pure definition, no proof obligations. Unpack the subtype witness $v.val=(x,y):\mathbb{Z}\times\mathbb{Z}$ and return $x.\mathrm{natAbs}+y.\mathrm{natAbs}$. No lemmas are applied.
why it matters
Height is the potential that makes the diamond satisfy the descent-connectivity hypotheses. Downstream, hzero shows height zero forces the centre; descent builds a 4-neighbour step that strictly lowers height from every off-centre cell; those two facts feed connected_of_descent, which yields a single ambient component. That connectivity closes the hypothesis of the headline mono_components_le_bichromatic_succ (locked domains $\le$ interface edges $+1$) on the 2D diamond, discharging the open connected-graph fact left by the cosmogenesis domain-coarsening scripts. In Recognition terms it is the recognition law's pull toward the coarsest description, read as graph connectivity on the L1 ball.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.