adj
plain-language theorem explainer
Two integer lattice points are 4-neighbours when their Manhattan distance is exactly one. Cosmology proofs on the 2D diamond (L1 ball) cite this as the ambient adjacency of the world graph. The body is a one-line Prop definition plus a DecidableRel instance.
Claim. For lattice points $p,q\in\mathbb{Z}\times\mathbb{Z}$, write $p\sim q$ when $|p_1-q_1|+|p_2-q_2|=1$ (axis-aligned unit steps only).
background
The module proves a dimension-free bound on locked domains in a coloured finite world: the number of monochromatic components is at most the number of bichromatic (interface) edges plus one, once the ambient graph is connected. In 2D the engine's world is the diamond, the closed L1 ball $|x|+|y|\le t$ on $\mathbb{Z}^2$, with the standard 4-neighbour grid graph.
Adjacency here is pure L1 geometry: two cells share an edge precisely when their coordinate-wise absolute differences sum to one. That is the discrete Neumann neighbourhood (no diagonals). The same relation later filters the finite vertex type of the diamond into an explicit edge list, and supplies the steps used by the height-descent connectivity argument (L1 norm as height, origin as unique zero).
proof idea
Pure definition: the predicate is the equality of the sum of natAbs coordinate differences with 1. A DecidableRel instance is inferred after unfolding, so filters and membership proofs can decide adjacency by computation.
why it matters
This is the atomic edge relation for the 2D diamond world. Downstream, edges builds the ordered pair list of all adjacent diamond vertices by filtering on this predicate; mem_edges rewrites list membership to the predicate; and descent constructs, from any off-centre vertex, a 4-neighbour step that strictly lowers L1 height toward the origin.
Those pieces feed connected_of_descent and then Diamond.mono_le_interface_succ, closing the connected-graph hypothesis left open in the domain-coarsening scripts. In Recognition terms this is the 2D lattice substrate on which monochromatic locked domains and the bichromatic interface are counted; the headline inequality is the higher-D analogue of the 1D identity runs = boundaries + 1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.