spine_eq_image

In the polarized-birth cosmology modules, the world at radius $t$ is the 2-D L1 diamond (ball) of lattice points with $|x|+|y|\le t$. The birth field is the sign pattern $+1$ on $x>0$, $-1$ on $x<0$, and $0$ on the column $x=0$. Phase 50 already showed that this field is carried by exactly three locked domains for every $t$, so the carried state is $O(1)$ while volume is $\Theta(t^2)$.

This module treats the complementary interface side: where bichromatic edges (forced distinctions) sit. The spine is defined as the slice of the diamond with first coordinate zero. Upstream, mem_ball_iff states that $(x,y)$ lies in the diamond iff $|x|+|y|\le t$, so restricting to $x=0$ is exactly $|y|\le t$. The integer closed interval $[-t,t]$ therefore parametrizes the spine once mapped by $y\mapsto(0,y)$.

Term-mode proof by Finset.ext on a generic lattice point $(x,y)$. After unfolding the spine filter and simplifying with mem_ball_iff, Finset.mem_image, Finset.mem_Icc, and product injectivity, membership becomes the pair of conditions "in the diamond and $x=0$".

Left-to-right: from diamond membership plus $x=0$, recover $y$ as the preimage with $-t\le y\le t$ (via omega) and the image equality. Right-to-left: from an integer $z\in[-t,t]$ mapped to $(0,z)$, the L1 bound $|0|+|z|\le t$ holds by omega, and the first coordinate is zero by construction. Both directions are pure arithmetic on absolute values and interval bounds.

This equality is the structural identification that turns spine cardinality into ordinary interval counting. Downstream, spine_card rewrites through it, applies injectivity of $y\mapsto(0,y)$, and obtains $\mathrm{card}(\mathrm{spine},t)=2t+1$ from Int.card_Icc.

Together with interface_on_spine (every bichromatic edge of the polarized field touches $x=0$), the picture is: recognition activity is confined to a codimension-1 1-D ball of size $\Theta(t)$ inside a $\Theta(t^2)$ world, so interface over volume tends to zero as a theorem. Module status is fully proved (zero sorry). This closes the interface half of sub-extensivity for the birth field; the carried half was Phase 50's three locked domains. It does not yet enumerate exact edge counts (e.g. $8t-4$ ordered edges in 2-D), but spine confinement plus spine size already give the surface-localization claim used in the cosmology forcing narrative.