edge_structure
plain-language theorem explainer
Any unit-distance edge joining opposite polarized charges on the 2-D diamond has one endpoint on the spine $x=0$ and the other at $x=\pm 1$, sharing the same $y$-coordinate. Interface-count arguments cite this to pin every bichromatic edge to the triple $(y,\mathrm{side},\mathrm{orientation})$. The proof is pure case analysis on $\mathrm{sign}(x)$ under L1-adjacency, discharged by omega.
Claim. For every radius $t\in\mathbb{N}$ and every pair of diamond vertices $a,b$ at L1-distance one whose polarized charges differ, either $a_x=0$ with $b_x\in\{1,-1\}$ and $a_y=b_y$, or $b_x=0$ with $a_x\in\{1,-1\}$ and $a_y=b_y$.
background
The module counts the exact recognition-active interface of the polarized birth field on the 2-D diamond. Vertices are lattice points in the L1 ball of radius $t$. Adjacency is the 4-neighbour relation: absolute coordinate differences sum to exactly one.
Polarization assigns a binary charge from the sign of the $x$-coordinate. Bichromatic edges (adjacent pairs of opposite charge) form the recognition-active interface. Phase 51 confined that interface to the codimension-1 spine $x=0$ and bounded spine cells; this module upgrades the bound to an exact edge count.
The geometric fact needed first is that every bichromatic unit edge is a horizontal step off the spine: one endpoint at $(0,y)$, the other at $(\pm 1,y)$. That pins edge data to $(y,\mathrm{side},\mathrm{orientation})$ with $|y|\le t-1$.
proof idea
Unfold adjacency to the L1-distance-one equation on integer coordinates. Simplify the polarization inequality, which is defined by case splits on $\mathrm{sign}(x)$ of each endpoint. Split on those conditionals; each branch is a finite system of linear equalities and inequalities on the two $x$-coordinates and the shared-or-not $y$-coordinates. Omega closes every branch, leaving only the two spine-neighbour configurations stated in the conclusion.
why it matters
Workhorse for interface_card_eq, which proves the ordered bichromatic edge set has cardinality $8t-4$ by exhibiting a bijection onto ${\text{interior spine }y}\times{\mathrm{side},\mathrm{orientation}}$. The structure lemma supplies the forward direction: every bichromatic edge is exactly one such triple.
That exact count yields the headline corollary that the interface grows by exactly eight ordered edges per cadence cycle $t\to t+1$, independent of world size. Recognition cost therefore tracks interface activity $O(1)$ per cycle, not volume $\Theta(t^2)$: the compute-watch principle the simulation runs on.
The same geometry lifts in the Octahedron namespace to $D=3$ (the spatial dimension forced by the T8/T9 chain), where the interface becomes a growing disk and the per-cycle increment is $\Theta(t)$ rather than constant, still sub-extensive in the $\Theta(t^3)$ volume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.