boundary_zpos
plain-language theorem explainer
The +z face of the 3D L1 ball of radius t has exactly 2t² + 2t + 1 lattice cells: those whose upward neighbor exits the ball. Cosmology edge-count arguments cite this as the codimension-1 boundary size per unit direction. The proof is a Finset bijection onto the transverse 2D diamond, mapping each boundary cell to its (x,y) and recovering maximal z = t − |x| − |y|.
Claim. For every natural number $t$, the number of lattice points $p$ in the three-dimensional $\ell_1$ ball of radius $t$ such that $p + e_z$ lies outside the ball equals $2t^2 + 2t + 1$.
background
This module counts total ordered adjacencies of the integer L1 ball by a volume-minus-boundary ledger. In 3D the ball is the octahedron $|x|+|y|+|z|\le t$; each of the six unit directions contributes a codimension-1 face of cells whose neighbor in that direction leaves the ball. The module doc records that each such face has size equal to the transverse 2D diamond volume $2t^2+2t+1$.
The 2D diamond is the Finset of pairs $(x,y)$ with $|x|+|y|\le t$, carved from a bounding box by an L1 filter. Membership is characterized by the standard absolute-value criterion. The closed-form card of that diamond is the Phase-49 area law reused here as the target count.
The +z face consists exactly of the cells of maximal $z$ for each admissible transverse pair: $z=t-|x|-|y|$. Counting them is therefore equivalent to counting the 2D diamond.
proof idea
Rewrite the claimed cardinality as the 2D diamond card via the known area law. Build an explicit Finset.card_bij' between the filtered +z-boundary set and the 2D diamond: the forward map drops the $z$ coordinate; the inverse rebuilds $z$ as $t-|x|-|y|$.
The four side conditions (forward lands in the diamond, inverse lands in the filter, left inverse, right inverse) are discharged by unfolding the L1 membership criterion and discharging the resulting absolute-value inequalities with omega. The right-inverse case is definitional.
why it matters
Downstream, three_mul_step_card uses this face size for every unit direction: thrice the in-ball step count equals $4t^3+2t$, obtained by subtracting thrice the boundary $2t^2+2t+1$ from thrice the bulk octahedron volume. Summing over the six directions yields the closed total adjacency count $8t^3+4t$ of the coarsening world.
That total is the other side of the carried-versus-interface ledger. Subtracting the polarized bichromatic interface leaves the monochromatic carried edges, the exact closed form of "carry the bulk coarse, pay only for the interface." The result is one of the six symmetric face counts that make the 3D volume-minus-boundary argument fully rigorous.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.