total_edge_card
plain-language theorem explainer
The L1 diamond of radius t has exactly 8t² ordered 4-neighbour adjacencies (each undirected edge counted both ways). Cosmology and coarsening arguments cite this as the bulk adjacency ledger against which the polarized interface is subtracted. The proof is a Finset bijection from ordered edges onto in-ball (cell, direction) pairs, then the already-proved 8t² count of that index set.
Claim. For every natural number $t$, the set of ordered pairs of lattice points in the diamond $|x|+|y|\le t$ that are 4-neighbours (L1 distance exactly one) has cardinality $8t^2$. Equivalently, ordered edges of the diamond biject with pairs (cell, unit direction) whose step stays inside the ball.
background
The module counts total adjacencies of the coarsening world so the monochromatic (carried) bulk can be split from the bichromatic interface. The 2D diamond is the L1 ball $|x|+|y|\le t$ on $\mathbb{Z}^2$. Four-neighbour adjacency means L1 distance exactly one: the four unit steps $(\pm 1,0)$ and $(0,\pm 1)$.
$E(t)$ is the Finset of ordered vertex pairs inside the diamond that are adjacent. $D(t)$ (the cell-direction index set) is the product of the ball with the four unit directions, filtered to those steps that remain in the ball. An upstream theorem already shows $|D(t)|=8t^2$ by summing, per direction, ball volume minus a codimension-1 silhouette of size $2t+1$.
Module framing: PolarizedBirthInterfaceCount posts the forced interface $8t-4$ in 2D; this module supplies the complementary total so carried mono edges equal total minus interface.
proof idea
Rewrite the goal as $|E(t)|=|D(t)|$ via the upstream card law for $D$. Build an explicit Finset bijection with card_bij':
- Forward: send an ordered edge $(a,b)$ to $(a,,b-a)$, the base cell and the unit difference.
- Inverse: send $(c,d)$ to $(c,,c+d)$.
Four side conditions: forward lands in $D$ (difference is a unit direction by adjacency, and $a+(b-a)=b$ stays in the ball); inverse lands in $E$ (step by a unit direction is adjacent); left and right inverses are algebraic identities on coordinates (ring). Once the bijection is in place, $|E|=|D|=8t^2$.
why it matters
This is the closed-form bulk half of the 2D adjacency ledger. Downstream, carried_edge_card subtracts the polarized interface $8t-4$ to get the monochromatic count $8t^2-8t+4$: the bulk the engine carries for free. edges_length rephrases the same count as the length of the engine edge list.
It also feeds the discrete isoperimetric laws: interface squared at most $8$ times total adjacency (2D surface scaling), and the 3D cube-versus-square companion. Together these make precise the coarsening slogan "carry the bulk coarse, pay only for the interface": the carried fraction tends to 1, and cost is sub-extensive on a perimeter. Landmark contact is the D=3 / eight-tick lattice geometry of the forcing chain, specialized here to the 2D diamond slice used by polarized birth.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.