three_mul_Dset_card
plain-language theorem explainer
For the 3D L1 octahedron of radius t, three times the number of valid (cell, unit-direction) pairs equals 24t³ + 12t, i.e. there are 8t³ + 4t ordered in-ball steps. Anyone counting total 6-neighbour adjacencies of the coarsening world cites this closed form. The proof rewrites the index-set card as a sum over the six axis directions and applies the per-direction step law, then multiplies by the direction count.
Claim. For every $t \in \mathbb{N}$, if $D(t)$ is the set of pairs $(p,d)$ with $p$ a lattice point of the octahedron $|x|+|y|+|z|\le t$ and $d$ a unit axis direction such that $p+d$ still lies in the octahedron, then $3\,|D(t)| = 24t^3 + 12t$.
background
This module closes the adjacency ledger of the coarsening world: total ordered edges minus the forced bichromatic interface equals the monochromatic carried bulk. In 3D the domain is the L1 octahedron of radius $t$ (the finite set of lattice points with $|x|+|y|+|z|\le t$), with six axis unit directions.
The index set $D(t)$ collects pairs (cell, direction) for which the directed step stays inside the ball; ordered edges biject onto it. Because the volume law is stated division-free over $\mathbb{N}$ as $3\cdot|\mathrm{ball},t| = 4t^3+6t^2+8t+3$ (from LatticeBallVolume), every edge count is likewise written with a leading factor of 3.
Upstream, the per-direction law already subtracts the codimension-1 silhouette: for each fixed unit $d$, three times the number of in-ball $d$-steps equals $4t^3+2t$ (bulk minus the transverse diamond of card $2t^2+2t+1$). Spatial dimension $D=3$ is the forced value from the Recognition chain (T8/T9).
proof idea
First identify $|D(t)|$ with the sum, over the six unit directions, of the number of cells whose $d$-neighbour stays in the ball: unfold the filter definition of $D(t)$, commute the product sum, and match cards.
Multiply both sides by 3 and push the factor inside the sum. For each direction apply the upstream per-direction identity three_mul_step_card, which supplies the constant $4t^3+2t$ independently of $d$.
The sum of a constant over the direction set collapses by sum_const and dirs_card (six directions). Algebra finishes: $6\cdot(4t^3+2t)=24t^3+12t$.
why it matters
This is the middle rung of the 3D total-adjacency law. Downstream, three_mul_total_edge_card transports the same polynomial from the (cell, direction) index set onto the ordered edge Finset $E(t)$ by an explicit bijection, yielding the module headline: the octahedron has exactly $8t^3+4t$ ordered 6-neighbour adjacencies (stated division-free as $3\cdot\mathrm{card}=24t^3+12t$).
That total is the left side of the carried-versus-interface split. Subtracting the polarized interface count leaves the monochromatic bulk the engine carries for free, so the carried fraction tends to 1. The module doc frames this as the exact closed form of "carry the bulk coarse, pay only for the interface."
Dimensionally it sits on the forced $D=3$ of the Recognition forcing chain (T8), with six neighbours matching the three spatial axes. No scaffolding remains: the statement is a plain theorem over $\mathbb{N}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.