slice_card
plain-language theorem explainer
For fixed integer x with |x| ≤ t, the horizontal slice of the L1 diamond of radius t has exactly 2(t − |x|) + 1 lattice points. Cosmology and discrete-geometry arguments cite this as the fiber width in the 2D diamond cardinality. The proof identifies the filtered interval with a centered Icc of half-width t − |x| and applies the standard integer-interval card formula.
Claim. Let $t \in \mathbb{N}$ and $x \in \mathbb{Z}$ with $|x| \le t$. Then the cardinality of $\{ y \in [-t,t] \cap \mathbb{Z} : |x| + |y| \le t \}$ equals $2(t - |x|) + 1$.
background
The module develops closed-form lattice-ball counts for the scale-adaptive coarsening engine. That engine grows its world on 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 total cell counts (e.g. 1201 cells at $t=24$ for the diamond); the module lifts those to theorems over $\mathbb{N}$.
Both volume laws fiber a $d$-ball over the first coordinate into $(d-1)$-balls. The diamond slice at fixed $x$ is the integer interval $[-(t-|x|), t-|x|]$, of odd width $2(t-|x|)+1$. Summing those widths over $x\in[-t,t]$ yields the centered-square formula $2t^2+2t+1$. The interface-component bound and these volume laws form the geometric backbone of the sub-extensivity claim in Phases 13–15: shell over ball tends to zero, so cost localizes to a perimeter.
Spatial dimension $D=3$ is forced upstream (T8/T9), which is why the 3D octahedron law sits on top of the 2D diamond law built from this slice identity.
proof idea
Show the filtered set equals the centered interval $\mathrm{Icc}(-(t-|x|), t-|x|)$ by Finset.ext: membership on both sides is equivalent by simp on mem_filter/mem_Icc plus omega on the absolute-value inequalities (using $|x|\le t$). Rewrite the goal with that equality, apply Int.card_Icc (cardinality of an integer closed interval), and finish with omega to match $2(t-|x|)+1$.
why it matters
This is the elementary fiber lemma for the 2D diamond area law. Downstream, diamond_card_eq_sum writes the diamond cardinality as $\sum_{x\in[-t,t]}(2(t-|x|)+1)$ by filtering the product of two intervals and applying this slice count pointwise. That fibered sum is then closed by induction (peeling endpoints) to $2t^2+2t+1$, the centered square numbers matching the simulation totals.
The octahedron law is built the same way on the diamond law, so the whole $\Theta(t^d)$ volume / $\Theta(t^{d-1})$ shell story for the coarsening engine rests on this identity. In the Recognition framework it supports the geometric half of sub-extensivity (Phases 13/14/15): active frontier fraction $\mathrm{shell}/\mathrm{ball}\to 0$. It does not itself invoke T5–T8 or the RCL; it is pure discrete geometry feeding the cosmology lattice counts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.