Vtx
plain-language theorem explainer
Vertices of the 2D diamond of radius t are the integer lattice points inside the L1 ball. Cosmology proofs of locked-domain bounds and diamond connectivity cite this type as the finite vertex set. It is a subtype abbreviation over the Finset ball, so Fintype and DecidableEq arrive automatically from the coercion.
Claim. For each $t\in\mathbb{N}$, the diamond vertex type is the subtype $\{(x,y)\in\mathbb{Z}\times\mathbb{Z}: |x|+|y|\le t\}$ of lattice points in the $\ell_1$ ball of radius $t$.
background
This module proves a dimension-free bound on locked domains: on any finite connected world, the number of monochromatic components is at most the number of bichromatic (interface) edges plus one. Connectivity of the ambient lattice is discharged by a height-descent criterion rather than by ad hoc casework.
The 2D diamond is the L1 ball of radius $t$ on $\mathbb{Z}^2$. Upstream, ball t builds that set as a filtered bounding box Finset: points of the integer square $[-t,t]^2$ with $|x|+|y|\le t$. The vertex type is exactly the subtype of membership in that Finset.
Height on a vertex is the L1 norm (graph distance toward the origin). The same pattern appears for the 3D octahedron elsewhere in the module; here only the planar diamond is wired.
proof idea
Pure abbreviation: the type is the subtype {p : ℤ × ℤ // p ∈ ball t}. No proof obligations. Finiteness and decidable equality are inherited from the Finset carrier via the standard subtype coercion, as the doc-comment notes.
why it matters
This is the carrier type for the entire 2D diamond instance of the interface-component theorem. Downstream definitions and lemmas are typed over it: the origin center, the L1 height, the 4-neighbour edges list, and the descent theorem (every off-centre vertex has a neighbour of strictly smaller height).
Those pieces feed connected_of_descent, which closes ambient connectivity for the diamond and unlocks Diamond.mono_le_interface_succ. That inequality is the Lean discharge of the open connected-graph fact left numeric-only in the cosmogenesis domain-coarsening scripts: locked domains ≤ interface size + 1. In Recognition terms it is the graph reading of the pull toward the coarsest description on a finite world.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.