Dset
plain-language theorem explainer
Defines the index set of ordered lattice steps that stay inside the 2D L1 diamond of radius t: pairs (cell, unit direction) with both endpoints in the ball. Downstream edge-count theorems cite it as the domain that bijects with ordered adjacencies. The body is a plain product-filter construction over the diamond and the four unit directions.
Claim. For each natural number $t$, let $B_t$ be the 2D L1 ball $\{(x,y)\in\mathbb{Z}^2:\lvert x\rvert+\lvert y\rvert\le t\}$ and let $D=\{(1,0),(-1,0),(0,1),(0,-1)\}$. Define $\mathcal{D}_t$ as the finite set of pairs $(p,d)\in B_t\times D$ such that $p+d\in B_t$.
background
This module closes the adjacency ledger for the coarsening world: total ordered edges of the L1 ball, split into monochromatic (carried) versus bichromatic (interface) edges. The interface side is already counted elsewhere ($8t-4$ in 2D); here the total is obtained by a volume-minus-boundary argument so the carried count is exact.
The ambient geometry is the 2D diamond $B_t$: lattice points with $\lvert x\rvert+\lvert y\rvert\le t$, realized as a filtered bounding box. The four unit steps $D$ are the 4-neighbour lattice directions. An ordered adjacency is a pair of neighbouring cells both in $B_t$; equivalently, a cell together with a direction whose step remains inside the ball.
That equivalence is the point of this definition. Later theorems identify the ordered edge set with $\mathcal{D}_t$ by an explicit bijection, then count $\lvert\mathcal{D}_t\rvert$ by summing, per direction, $\lvert B_t\rvert$ minus the codimension-1 exit boundary.
proof idea
Definition, not a proof. Form the Cartesian product of the diamond $B_t$ with the four unit directions, then retain only those pairs whose vector sum lands back in $B_t$. No lemmas are applied; the filter is the entire content.
why it matters
This index set is the counting scaffold for the closed-form total adjacency laws. Dset_card proves $\lvert\mathcal{D}_t\rvert=8t^2$ (four directions, each contributing $2t^2$ interior steps). total_edge_card then bijects ordered edges onto $\mathcal{D}_t$, yielding the 2D law: the diamond has exactly $8t^2$ ordered 4-neighbour adjacencies.
The same pattern lifts to 3D (three_mul_Dset_card, three_mul_total_edge_card): six directions on the octahedron give $8t^3+4t$ ordered edges. Subtracting the polarized interface count produces the monochromatic carried edges $8t^2-8t+4$ in 2D, so the carried fraction tends to 1. That is the exact statement of "carry the bulk coarse, pay only for the interface" in the coarsening program. Dimension $D=3$ and the eight-tick octave sit upstream in the forcing chain; this module supplies the lattice combinatorics those continuum claims rest on when specialized to discrete birth domains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.