three_mul_step_card
plain-language theorem explainer
For each of the six axis unit directions on the 3D L1 octahedron of radius t, three times the number of lattice cells whose neighbour in that direction stays inside the ball equals 4t³ + 2t. Cosmology edge-count arguments cite it when assembling the total ordered adjacency. The proof is volume minus codimension-1 boundary, case-split on the six directions, closed by omega.
Claim. Let $B_t$ be the 3D $\ell^1$ ball (octahedron) of radius $t$ in $\mathbb{Z}^3$, and let $d$ be one of the six axis unit vectors. Then $$3\,\bigl|\{p\in B_t: p+d\in B_t\}\bigr| = 4t^3 + 2t.$$
background
This module counts total ordered adjacencies of the coarsening lattice world, splitting them into monochromatic (carried) edges versus bichromatic interface edges. In 3D the domain is the L1 octahedron $B_t={p\in\mathbb{Z}^3:|p|_1\le t}$, with six neighbour directions $(\pm e_x,\pm e_y,\pm e_z)$.
Ordered edges biject with pairs (cell, direction) where both the cell and its translate by the unit direction lie in $B_t$. For fixed $d$, the cells whose $d$-step leaves $B_t$ form a codimension-1 face whose cardinality equals the transverse 2D diamond volume $2t^2+2t+1$ (the six face theorems boundary_*).
The bulk volume law from LatticeBallVolume.Octahedron supplies $3,|B_t|=4t^3+6t^2+8t+3$. Subtracting three times the face count from the bulk yields the interior step count per direction.
proof idea
Invoke the octahedron volume identity $3,|B_t|=4t^3+6t^2+8t+3$. Case-split on membership of $d$ in the six-element direction set. In each case load the matching face-cardinality theorem (right/left/top/bottom/$\pm z$ boundary equals $2t^2+2t+1$). Apply the Finset split that interior-filter card plus exterior-neighbour-filter card recovers $|B_t|$. Clear trivial zero shifts, then omega discharges the arithmetic $$3(|B_t|-\mathrm{bdry})= (4t^3+6t^2+8t+3)-3(2t^2+2t+1)=4t^3+2t.$$
why it matters
Feeds directly into three_mul_Dset_card, which sums the six directions to obtain $3\cdot|D_t|=24t^3+12t$, i.e. the closed form for the total ordered adjacency count of the 3D octahedron (equivalently $8t^3+4t$ edges). That total is the ledger against which the polarized-birth interface count is subtracted, producing the exact monochromatic carried-edge formula and the carried fraction tending to 1.
Module-level north star: "carry the bulk coarse, pay only for the interface." This per-direction step is the volume-minus-boundary brick that makes the 3D total a theorem over $\mathbb{N}$ with no sorry. It sits in the cosmology lattice bookkeeping that realises the discrete $D=3$ geometry (forcing landmark T8) used by the coarsening engine.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.