three_mul_total_edge_card
plain-language theorem explainer
The integer octahedron |x|+|y|+|z|≤t has ordered 6-neighbour adjacency count satisfying 3·card=24t³+12t (equivalently card=8t³+4t). Anyone auditing the coarsening ledger or the engine edge list cites this closed form. Proof: Finset bijection of ordered edges onto admissible (cell, unit-direction) pairs, then apply the already-proved Dset cardinality law.
Claim. For every $t\in\mathbb{N}$, three times the number of ordered pairs of lattice points in the octahedron $|x|+|y|+|z|\le t$ that are adjacent at $L^1$-distance one equals $24t^3+12t$.
background
This module closes the adjacency ledger of the coarsening world: PolarizedBirthInterfaceCount already gives the bichromatic interface cost; here one counts every ordered adjacency, so the monochromatic (carried) bulk is total minus interface.
The ambient set is the 3-D $L^1$ ball (octahedron) of radius $t$. Six unit axis steps define neighbourship. The ordered adjacency finset $E(t)$ is all vertex pairs at $L^1$-distance one. The index set $D(t)$ is pairs (cell, direction) with both cell and cell+direction still in the ball; ordered edges are designed to biject onto $D(t)$.
Upstream, three_mul_Dset_card already evaluates $3\cdot|D(t)|=24t^3+12t$ by summing, per direction, volume minus a transverse diamond boundary (reusing the Phase-49 ball-volume laws). Spatial dimension $D=3$ is the forced constant from the foundation chain.
proof idea
Rewrite the goal so that $|E(t)|$ is replaced by $|D(t)|$, then finish by three_mul_Dset_card.
The replacement is a Finset.card_bij'. Forward map: ordered edge $(a,b)\mapsto(a,,b-a)$. Inverse: $(c,d)\mapsto(c,,c+d)$. Four side conditions: the forward image lands in $D(t)$ (adjacency means the difference is one of the six unit directions, discharged by omega); the inverse lands in $E(t)$ (case-split on the six directions); both round-trips are identity on coordinates (ring on each component, plus Subtype.ext).
No volume computation happens here; that work sits in the upstream Dset count.
why it matters
Division-free 3-D total adjacency law for the octahedron. Immediate parent is total_edge_card, which divides by three (omega) to the usable form $|E(t)|=8t^3+4t$, and then edges_length, matching the engine's octahedron edge-list length.
That total is the upper half of the carried-versus-interface split: carried_edge_card subtracts the polarized interface $8t^2-8t+4$ to get the monochromatic bulk $8t^3-8t^2+12t-4$. Module doc states the payoff: the carried fraction tends to 1, so the engine carries almost every adjacency free and pays only a vanishing interface fraction. This is the exact closed form of the coarsening north star in $D=3$ (T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.