interface_on_spine

The module studies the recognition-active interface of the forced conjugate-birth field on the 2-D diamond of radius $t$. Phase 50 already showed the carried side: the field is $+1$ on $x>0$, $-1$ on $x<0$, and $0$ on the spine $x=0$, held as exactly three locked domains for every radius, so carried state is $O(1)$ while the world is $\Theta(t^d)$.

Here the complementary interface side is treated. The edge list is the 4-neighbour adjacency list of diamond vertices (edges t). An edge is bichromatic when the two endpoints receive different values under the polarized charge map. The spine is the column of cells with first coordinate $x=0$. Upstream, membership in the edge list is equivalent to lattice adjacency (mem_edges), and the structural fact bichromatic_endpoint_on_spine already records that a same-row step flipping $\mathrm{sign}(x)$ must touch $x=0$.

Term-mode proof by unpacking. Introduce a filtered edge $p$ and rewrite membership in the filter to obtain adjacency plus the decide-true bichromaticity hypothesis. Convert list membership to adjacency via mem_edges, and strip decide via decide_eq_true_eq. The goal is then exactly the conclusion of bichromatic_endpoint_on_spine applied to the two endpoints, which finishes the proof. No new geometry is argued here; the theorem is the list-level packaging of that structural lemma over the concrete interface filter.

This is the spine-confinement half of Phase 51. It feeds directly into the capstone birth_field_subextensive, whose second conjunct is literally this statement: the entire recognition-active interface is spine-incident. Together with Phase 50's three locked domains and the spine-cardinality bound (spine times radius fits in the diamond area), both halves of birth-field sub-extensivity become theorems: carried domains $O(1)$, active interface on a $\Theta(t^{d-1})$ codimension-1 set, both vanishing as a fraction of the $\Theta(t^d)$ world.

In Recognition Science terms this makes exact the North-Star rule that each region is carried at the coarsest $\varphi$-rung its recognition allows, for the forced conjugate-birth field. The module status is fully proved (zero sorry). It does not yet enumerate the exact edge count (numerically $8t-4$ ordered edges in 2-D); sub-extensivity content is confinement plus spine cardinality, both theorems here.