dirs
plain-language theorem explainer
The four cardinal unit steps on the integer lattice: east, west, north, and south. Anyone counting 4-neighbour adjacencies on the 2D L1 ball cites this as the fixed direction set. It is a literal four-element Finset, not a derived construction.
Claim. The unit direction set of the 4-neighbour lattice on $\mathbb{Z}^2$ is $\{(1,0),(-1,0),(0,1),(0,-1)\}$.
background
This module counts total ordered adjacencies of the L1 ball (the diamond) so that monochromatic carried edges can be split from bichromatic interface edges. The engine pays only for the interface; the bulk is carried free. Ordered edges are pairs (cell, direction) where both the cell and its neighbour lie in the ball.
The direction set is the four axis-aligned unit steps of the 4-neighbour grid. Downstream, the product of the ball with this set is filtered to those steps that stay inside, giving the index set whose cardinality is the total ordered edge count. The module reuses the Phase-49 diamond volume law $\mathrm{card}(\mathrm{ball}, t)=2t^2+2t+1$ and a per-direction boundary of size $2t+1$.
proof idea
Literal Finset definition: the four pairs are written out by hand. No lemmas, no tactics.
why it matters
This is the direction alphabet for the entire 2D edge ledger. It feeds the cardinality fact that there are four directions, the (cell, direction) index set, the per-direction in-ball step count $2t^2$, and the closed form total ordered adjacency count $8t^2$. That total minus the polarized interface $8t-4$ yields the monochromatic carried count $8t^2-8t+4$, the exact statement of "carry the bulk coarse, pay only for the interface" in the coarsening north star. The same pattern lifts to the 3D octahedron with six directions; here the 2D case is fixed first.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.