outer_sum_2d
plain-language theorem explainer
The sum over the integer interval [-t,t] of the slice widths 2(t-|x|)+1 equals the centered square number 2t²+2t+1. Cosmology and lattice-geometry arguments cite it as the closed form for 2D L1-ball cardinality after fibering. The proof is induction on t, peeling the two new endpoints ±(t+1) and rewriting the inner summand by +2 each step.
Claim. For every natural number $t$, $\sum_{x=-t}^{t} \bigl(2(t-|x|)+1\bigr) = 2t^2 + 2t + 1$.
background
The module LatticeBallVolume closes the cell-count formulas used by the scale-adaptive coarsening engine. That engine grows an L1 ball by one rung per recognition cycle: the 2D diamond $|x|+|y|\le t$ and the 3D octahedron $|x|+|y|+|z|\le t$. Numeric runs report totals such as 1201 cells at $t=24$ (diamond) and 2625 at $t=12$ (octahedron); the module lifts those counts to closed forms over $\mathbb{N}$.
A fixed-$x$ slice of the diamond is the integer interval $[-(t-|x|), t-|x|]$, of cardinality $2(t-|x|)+1$. Summing those widths over $x\in[-t,t]$ is exactly the outer sum proved here. The diamond itself is the filtered bounding box InterfaceComponentBound.Diamond.ball t. The same fibering pattern later builds the octahedron law on top of the diamond law, so this identity is the 2D base case of the volume ladder.
proof idea
Induction on $t$. The zero case is simp. In the successor step, split the interval $[- (n+1), n+1]$ as the old interval $[-n,n]$ with the two endpoints $\pm(n+1)$ inserted; membership side-conditions are discharged by omega. Each endpoint summand collapses to 1 because $|\pm(n+1)|=n+1$.
The remaining sum is rewritten pointwise: for $x\in[-n,n]$, $2((n+1)-|x|)+1 = (2(n-|x|)+1)+2$. Distribute the sum, apply the inductive hypothesis to the first piece, and evaluate the constant sum via the card identity $|[-n,n]|=2n+1$. A final ring closes $2n^2+2n+1 + 2(2n+1) + 2 = 2(n+1)^2+2(n+1)+1$.
why it matters
This identity is the algebraic engine behind the 2D diamond area law. Downstream, Diamond.card_ball is the one-line rewrite diamond_card_eq_sum then outer_sum_2d, giving $\mathrm{card}{|x|+|y|\le t}=2t^2+2t+1$ (centered square numbers; 1201 at $t=24$). The 3D parent three_mul_outer_sum_3d reuses the diamond area law fiberwise and needs the companion sum $\sum(t-|x|)=t^2$ that rides on the same induction pattern.
In the Recognition framework these volume laws are the geometric backbone of the sub-extensivity claim in Phases 13/14/15: the accumulated world is $\Theta(t^d)$ while the active frontier (shell) is $\Theta(t^{d-1})$, so the active fraction tends to 0 and cost localizes to a perimeter. Together with InterfaceComponentBound they underwrite the coarsening engine's reported cell counts as theorems, not measurements. Spatial dimension $D=3$ (forced upstream) is why the octahedron, not a higher ball, is the physical case; the 2D law is the necessary fiber base.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.