spine
plain-language theorem explainer
Defines the spine of the 2-D L1 diamond of radius t as the lattice cells with first coordinate zero. Cosmology and interface-cost arguments cite it as the codimension-1 carrier of all bichromatic edges of the polarized birth field. The body is a one-line filter of the diamond ball on x = 0.
Claim. For each radius $t \in \mathbb{N}$, the spine is the finite set of integer lattice points $(x,y)$ in the 2-D diamond $|x|+|y| \le t$ with $x = 0$. Equivalently, it is the image of the segment $[-t,t]$ under $y \mapsto (0,y)$, a 1-D ball of cardinality $2t+1$.
background
The module studies the recognition-active interface of the polarized birth field on the 2-D diamond. Phase 50 already showed the carried side: charge $+1$ on $x>0$, $-1$ on $x<0$, and $0$ on $x=0$ locks into exactly three monochromatic domains for every radius, so carried cost is $O(1)$ while volume is $\Theta(t^2)$.
The complementary question is where recognition activity (bichromatic edges) lives. Upstream, InterfaceComponentBound.ball is the L1 diamond: the Finset of lattice points in the bounding box filtered by $|x|+|y|\le t$. Spatial dimension $D=3$ is forced by T8/T9 in the foundation chain, but this definition works in the 2-D diamond slice used for the interface argument.
The spine is the vertical midline of that diamond: the column $x=0$. Module text records that every charge flip of $\mathrm{sign}(x)$ must cross this column, so the entire active interface is confined there.
proof idea
Pure definition: take the 2-D diamond ball of radius $t$ and retain only those points whose first coordinate equals zero. No lemmas are applied; the filter is the entire content. Downstream lemmas (spine_eq_image, spine_card) then identify it with the image of $[-t,t]$ under $y\mapsto(0,y)$ and prove cardinality $2t+1$.
why it matters
This is the geometric carrier for the interface half of birth-field sub-extensivity. Downstream, bichromatic_endpoint_on_spine and interface_on_spine place every bichromatic edge endpoint on this set; interface_subextensive and birth_field_subextensive then get $\mathrm{interface}/\mathrm{volume}\to 0$ because the spine is a codimension-1 ball of size $\Theta(t^{d-1})$.
In PolarizedBirthDomains it feeds polarized_components_le_three, polarized_carried_subextensive, and the descent lemma hdesc (roots live on the spine). Graded-rung cost ledgers (Phase 56) use the same interface-localization pattern: total cost equals interface cost, bulk free. Together with the three locked domains, spine confinement closes both halves of the sub-extensivity picture for the conjugate-birth field: carried $O(1)$, active surface $\Theta(t^{d-1})$, world $\Theta(t^d)$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.