diamond_card_eq_sum
plain-language theorem explainer
The lattice-point count of the 2D L1 diamond of radius t equals the sum over x in [-t,t] of the slice widths 2(t-|x|)+1. Anyone deriving the closed form 2t^2+2t+1 (centered square numbers) cites this fibration. The proof unfolds the ball as a filtered product, converts cardinality to a double sum, and invokes the one-dimensional slice-cardinality lemma on each fiber.
Claim. For every natural number $t$, the number of integer lattice points in the diamond $\{(x,y)\in\mathbb{Z}^2 : |x|+|y|\le t\}$ equals $\sum_{x=-t}^{t}\bigl(2(t-|x|)+1\)$.
background
The module treats lattice-ball cardinalities for the scale-adaptive coarsening engine: the accumulated world lives on an L1 ball that grows by one rung per recognition cycle. In 2D that ball is the diamond $|x|+|y|\le t$; numeric runs quote total cell counts (e.g. 1201 cells at $t=24$), and the module lifts those counts to closed forms over $\mathbb{N}$.
InterfaceComponentBound.ball t is the finset realization of that diamond: the axis-aligned box $[-t,t]^2$ filtered by the L1 constraint. For fixed first coordinate $x$ with $|x|\le t$, the $y$-slice is the integer interval $[-(t-|x|), t-|x|]$. The upstream lemma slice_card records that this slice has exactly $2(t-|x|)+1$ points.
The present statement is the fibered rewrite of diamond cardinality as the sum of those slice widths over $x\in[-t,t]$. The module then evaluates the sum by induction to the centered square number $2t^2+2t+1$.
proof idea
Unfold the diamond ball definition to the filtered product of two copies of $[-t,t]$. Rewrite cardinality of a filter as a sum of indicators, then apply Finset.sum_product to separate the double sum into an outer sum over $x$ and an inner filtered sum over $y$.
For each $x$ in the outer interval, membership in $[-t,t]$ plus omega gives $|x|\le t$. Replace the inner filtered cardinality by the closed slice width via slice_card, and finish by rewriting that width again as a filter-cardinality (matching the summand shape). The whole argument is a congruence of finite sums plus the one-dimensional slice lemma; no induction yet.
why it matters
This is the bridge from the geometric definition of the 2D diamond to its closed cardinality law. The module builds the octahedron (3D) volume law on the diamond law by the same fibration pattern, so every higher-dimensional count in the file rests on this identity.
Downstream, the evaluated sum yields Diamond.card_ball t = 2t^2+2t+1, which at $t=24$ recovers the reported 1201 cells. Shell sizes then become $4t$ (diamond) and $4t^2+2$ (octahedron): active frontier $\Theta(t^{d-1})$ against bulk $\Theta(t^d)$, so the active fraction tends to zero and cost localizes to a perimeter. Together with InterfaceComponentBound, these volume laws are the geometric backbone of the sub-extensivity claim in Phases 13/14/15 of the coarsening analysis.
In the broader Recognition setting this is pure discrete geometry supporting the eight-tick / $D=3$ spatial scaffolding, not a new forcing step; it makes the simulation's cell-count reports into theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.