spine_card

This module treats the recognition-active interface of the polarized birth field on the 2-D diamond lattice. Phase 50 already showed that the carried side of the field (the three locked domains $+1$, $-1$, and the zero spine) is $O(1)$ while the world volume is $\Theta(t^2)$. The complementary claim is that all bichromatic edges, hence all recognition cost, touch the spine $x = 0$.

The spine is defined by filtering the diamond ball to cells with first coordinate zero. An upstream identity spine_eq_image rewrites it as the image of the closed integer interval $[-t, t]$ under the embedding $y \mapsto (0, y)$, so the spine is literally a 1-D ball of radius $t$. The ambient ball is the $\ell^1$ diamond whose volume is known separately to be $2t^2 + 2t + 1$.

Rewrite the spine via spine_eq_image as the image of Finset.Icc (-t) t under $y \mapsto (0, y)$. The map is injective (equality of pairs forces equality of the second coordinates), so Finset.card_image_of_injective reduces the count to the cardinality of the integer interval. Int.card_Icc supplies that count, and omega closes the arithmetic identity $|[-t, t]| = 2t + 1$.

This is the exact size of the codimension-1 set that carries the entire recognition-active interface in 2-D. Downstream, interface_subextensive packages the identity with the volume comparison (spine t).card * t ≤ (Diamond.ball t).card, proving that the interface fraction falls as $\sim 1/t$: cost lives on a 1-D curve while the world is the 2-D area $2t^2 + 2t + 1$.

Together with Phase 50's $O(1)$ carried domains, the pair closes both halves of birth-field sub-extensivity: carried state and active interface both vanish as fractions of the $\Theta(t^d)$ world. The module status is theorem (zero sorry). The same pattern lifts to 3-D, where the spine becomes the 2-D diamond of size $2t^2 + 2t + 1$, matching the forced spatial dimension $D = 3$ from the forcing chain.