bichromatic_endpoint_on_spine
plain-language theorem explainer
Any two 4-adjacent cells of the polarized diamond that carry different charges must have an endpoint on the spine x = 0. Interface and birth-field arguments cite this to pin recognition activity to a codimension-1 set. The proof is pure case analysis: unfold unit L1 adjacency, case-split the sign definition of the charge, then omega forces a zero first coordinate.
Claim. For every radius $t\in\mathbb{N}$ and vertices $a,b$ of the $L^1$ diamond of radius $t$, if $a$ and $b$ are $4$-neighbours (unit $L^1$ distance) and the polarized charges differ, then $a_x=0$ or $b_x=0$. Here the polarized charge is $+1$ on $x>0$, $-1$ on $x<0$, and $0$ on the spine $x=0$.
background
The module studies the recognition-active interface of the forced conjugate-birth field on the 2D diamond lattice. Vertices are lattice points in the $L^1$ ball of radius $t$. Four-neighbour adjacency means unit $L^1$ distance: $|\Delta x|+|\Delta y|=1$.
The polarized charge (from PolarizedBirthDomains) is the forced birth assignment: $+1$ on the fine half $x>0$, $-1$ on the coarse half $x<0$, and $0$ on the spine $x=0$. Phase 50 already showed the carried side is three locked domains for every radius. This module treats the complementary interface side: where bichromatic (charge-flipping) edges sit.
Upstream, adj is exactly that unit $L^1$ relation, and mono_le_interface_succ bounds monochromatic domain count by the number of bichromatic edges plus one. The present lemma is the geometric fact that every such bichromatic edge touches $x=0$.
proof idea
Term-mode case analysis, no external lemmas beyond the definitions. Unfold adjacency to $|\Delta x|+|\Delta y|=1$. Simplify the polarized charge on both endpoints (the nested if on the sign of the first coordinate). Split on those conditionals: the only way the two charges differ is if the pair straddles or meets the spine. In every differing branch, the unit-step constraint on the first coordinate forces at least one endpoint to have $x=0$, discharged by omega.
why it matters
This is the atomic geometric step for spine confinement of the birth-field interface. The immediate parent is interface_on_spine, which lifts the pairwise statement to every edge in the filtered bichromatic edge list (the exact list bounded by mono_le_interface_succ).
Together with Phase 50 domain locking, it closes both halves of sub-extensivity for the birth field: carried domains stay $O(1)$ while the active interface lives on a $\Theta(t^{d-1})$ spine (segment in 2D, diamond in 3D), so interface over volume tends to zero as a theorem, not a numeric check. In the Recognition picture this is the structural reason recognition cost localizes to a surface rather than filling the $\Theta(t^d)$ world. It does not yet enumerate the exact edge count; confinement plus spine cardinality already give the sub-extensive content.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.