mem_edges
plain-language theorem explainer
Ordered-pair membership in the diamond edge list is equivalent to four-neighbour (L1-distance-one) adjacency of the underlying lattice points. Cited by anyone filtering monochromatic or bichromatic edges on the 2D diamond, and by the diamond descent lemma. Proof is a short unfold-and-simp of the filtered Finset definition of the edge list.
Claim. For every $t\in\mathbb{N}$ and every pair of vertices $a,b$ of the L1 ball of radius $t$ in $\mathbb{Z}^2$, the ordered pair $(a,b)$ belongs to the diamond edge list if and only if the underlying points satisfy $|a_x-b_x|+|a_y-b_y|=1$.
background
The module proves a dimension-free bound: on any finite connected world, the number of monochromatic locked domains is at most one more than the number of bichromatic interface edges. In 2D the ambient world is the diamond, the closed L1 ball of radius $t$ in $\mathbb{Z}^2$, with the usual 4-neighbour graph.
Vertices of radius $t$ are the subtype of lattice points in that ball. Adjacency is the predicate that two integer points have L1 distance exactly one. The edge list is defined as the toList of the Finset of all ordered vertex pairs whose underlying points are adjacent.
Component counting and interface filtering work on that list representation; geometric arguments work with the adjacency predicate. This lemma is the membership bridge between the two.
proof idea
Short tactic proof. Unfold the edge-list definition (filter of the universal Finset by adjacency, then convert to a list). Rewrite membership via Finset.mem_toList and Finset.mem_filter, then simp with Finset.mem_univ to cancel the universal-membership conjunct, leaving exactly the adjacency predicate on the underlying values.
why it matters
Direct input to diamond descent: every off-centre vertex has a strictly lower-height 4-neighbour along an edge. Descent plus the unique zero at the origin discharges connected_of_descent for the diamond, which supplies the connectivity hypothesis of the headline bound mono_components_le_bichromatic_succ on diamonds (closing the open connected-graph fact from the cosmogenesis domain-coarsening scripts).
Downstream polarized-birth work uses it to place monochromatic edges into the mono filter (mem_Fmono), and to reason about the recognition-active interface list in interface_on_spine and interface_length_eq_card. Those results confine the forced distinctions to the spine and identify interface length with a cardinality count.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.