edges
plain-language theorem explainer
For each radius t, the diamond lattice supplies an explicit list of every ordered pair of vertices at L1 distance one (the 4-neighbour graph). Cosmology and alpha-derivation code cite it as the ambient edge set when counting monochromatic components against the bichromatic interface. The body is a one-line Finset filter of the universal product by the adjacency predicate, then toList.
Claim. For each $t \in \mathbb{N}$, $\mathrm{edges}(t)$ is the list of all ordered pairs $(p,q)$ of lattice points in the diamond $\{(x,y)\in\mathbb{Z}^2 : |x|+|y|\le t\}$ such that the L1 distance between $p$ and $q$ equals $1$.
background
The 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. That closes an open connected-graph fact from the cosmogenesis domain-coarsening scripts.
Local geometry for the 2D case is the diamond: vertices are integer points in the L1 ball of radius $t$, and adjacency is L1 distance exactly one (the usual 4-neighbour grid relation). The edge list is the concrete adjacency the component-counting theorems consume: monochromatic edges generate locked domains; bichromatic edges form the interface.
Connectivity of the diamond itself is later discharged by a height argument (L1 norm toward the origin), so the headline inequality applies to the lattices the engine actually runs.
proof idea
Pure definition, not a proof. Take the finite type of all ordered pairs of diamond vertices, keep those pairs whose underlying integer points satisfy the 4-neighbour adjacency predicate, and materialize the resulting Finset as a List. Noncomputable only because Finset.toList is.
why it matters
This edge list is the ambient graph for the 2D diamond instance of the module headline: monochromatic components are at most interface size plus one. Downstream, AlphaDerivation and AlphaGenesis.LoopCertificate reuse the same geometric edge-counting language (active vs passive edges, cube edges at $D=3$, geometric seed factor 11) when deriving the fine-structure seed from $Q_3$ geometry and the eight-tick / $D=3$ forcing chain. Without an explicit ordered edge list, the monochromatic/bichromatic split and the merge-bound induction have nothing to iterate over.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.