E
plain-language theorem explainer
Total ordered adjacency set of the 2D L1 diamond of radius t: the Finset of vertex pairs at L1 distance one. Cosmology and coarsening arguments cite it as the bulk edge ledger against which the polarized interface is subtracted. Built by filtering the universal product of ball vertices by the 4-neighbour adjacency predicate; it is the Finset form of the engine edge list.
Claim. For each $t\in\mathbb{N}$, $E(t)$ is the finite set of ordered pairs $(u,v)$ of lattice points in the L1 ball of radius $t$ (the diamond $|x|+|y|\le t$) such that the L1 distance between $u$ and $v$ equals $1$.
background
This module splits the adjacency ledger of the coarsening world into total edges versus forced interface edges. The ambient geometry is the 2D diamond: the L1 ball $|x|+|y|\le t$ on $\mathbb{Z}^2$, packaged as a Finset (ball). Vertices of radius $t$ are the points of that ball. Four-neighbour adjacency means L1 distance exactly one: $|\Delta x|+|\Delta y|=1$.
Upstream, InterfaceComponentBound already exposes the same filter as a List (the engine edge list). The present definition keeps the Finset form so cardinalities and bijections with (cell, direction) pairs can be stated cleanly. The module target is the closed form for the total ordered edge count in 2D, then carried $=$ total $-$ interface.
proof idea
Definitional construction, not a theorem proof. Form the universal Finset of ordered pairs of vertices of the radius-$t$ ball, and retain those pairs whose underlying integer coordinates satisfy the 4-neighbour adjacency predicate (sum of absolute coordinate differences equals 1). Marked noncomputable because Finset.univ on the vertex subtype rides on classical packaging; decidability of adjacency is already instanced upstream.
why it matters
Supplies the exact bulk adjacency Finset for the volume-minus-boundary count of total ordered edges (siblings such as the cell-direction index set, boundary silhouettes, and total_edge_card). Module doc records the closed form $8t^2$ in 2D (4-neighbour diamond). Subtracting the polarized interface count $8t-4$ yields the monochromatic carried bulk $8t^2-8t+4$, with carried fraction $\to 1$: carry the bulk coarse, pay only the vanishing interface. That split is the exact ledger behind the coarsening north star in PolarizedBirthInterface. (Short-name E also appears in unrelated Action/Alpha modules; those edges are name collisions, not lattice uses.)
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.