three_mul_outer_sum_3d
plain-language theorem explainer
For every radius t, three times the sum of 2D diamond lattice-ball sizes over the first coordinate x in [-t,t] equals the centered octahedral polynomial 4t^3+6t^2+8t+3. Cosmology and coarsening authors cite it as the fibered outer sum that closes the 3D L1 volume law. The proof rewrites each fiber by the diamond area formula, then inducts on t, using the 2D outer-sum identity for the residual increment.
Claim. For every natural number $t$, $$3\sum_{x=-t}^{t}\#\{(y,z)\in\mathbb{Z}^2:\,|y|+|z|\le t-|x|\}=4t^3+6t^2+8t+3.$$ Equivalently, three times the outer fiber sum of 2D L1-ball cardinalities equals the division-free centered octahedral count.
background
The module supplies closed forms for the lattice-ball counts that the scale-adaptive coarsening engine accumulates: the 2D diamond $|x|+|y|\le t$ and the 3D octahedron $|x|+|y|+|z|\le t$. Numeric runs report totals such as 1201 diamond cells at $t=24$ and 2625 octahedron cells at $t=12$; the theorems lift those counts to identities over $\mathbb{N}$.
The 2D diamond ball is the finite L1 set carved from the bounding box. Its cardinality is the centered square number $2t^2+2t+1$ (the diamond area law). The 2D outer-sum theorem states $\sum_{x=-t}^{t}(2(t-|x|)+1)=2t^2+2t+1$, proved by induction peeling the endpoints $\pm(t+1)$.
A 3D octahedron fibers as a sum of 2D diamonds of radii $t-|x|$ over $x\in[-t,t]$. The present identity is exactly three times that outer sum, written division-free so the later volume law needs no rationals.
proof idea
First rewrite every fiber cardinality by the diamond area law: each summand becomes the quadratic $2(t-|x|)^2+2(t-|x|)+1$. The claim reduces to a pure $\mathbb{N}$ identity on that symmetric-interval sum.
Induct on $t$. The zero case is immediate. In the successor step, split the interval $[-n-1,n+1]$ by inserting the two new endpoints; each endpoint contributes $1$. On the inner interval, expand the quadratic shift $g((n+1)-|x|)=g(n-|x|)+4(n-|x|)+4$, split the sum, and identify the old outer sum $S$ with the inductive hypothesis.
The residual increment $T=\sum(4(n-|x|)+4)$ is rewritten as a linear combination of the 2D outer sum and the interval cardinality $2n+1$, yielding the closed form $4n^2+8n+4$. Reassemble $3(1+1+(S+T))$, substitute the IH and $T$, and finish by ring.
why it matters
This is the computational heart of the 3D volume law. The parent theorem Octahedron.three_mul_card_ball is a one-line rewrite of the octahedron card as this outer sum, then applies the present identity, giving $3\cdot\mathrm{card}(\mathrm{ball},t)=4t^3+6t^2+8t+3$ for every radius. At $t=12$ that specializes to the run-reported count 2625.
In the Recognition framework the coarsening world grows as $\Theta(t^D)$ with $D=3$ forced by the T8/T9 chain, while the active frontier is the shell $\Theta(t^{D-1})$. The volume and shell laws together make the active fraction tend to zero: cost localizes to a perimeter. Module documentation places these identities, with the interface-component bound, as the geometric backbone of the sub-extensivity claim in Phases 13/14/15.
The proof architecture mirrors the dimensional reduction in the primer: $d$-balls fiber over $(d-1)$-balls, so the octahedron law sits on the diamond law exactly as $D=3$ sits on the 2D interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.