memNbr
plain-language theorem explainer
Any index triple for a bichromatic interface edge at radius t has its off-spine neighbour cell (±1, y) inside the 2-D L1 diamond of radius t. Interface-count proofs cite this to type the neighbour endpoint as a vertex of the birth domain. The argument unpacks the index product bounds |y| ≤ t−1 and checks the L1 inequality by cases on the side bit.
Claim. Fix radius $t \in \mathbb{N}$ and an index $a = (y, s, o)$ in the product index set for interior spine heights with side and orientation bits. Then the neighbour lattice point $(\varepsilon, y)$, where $\varepsilon = +1$ if $s$ is true and $\varepsilon = -1$ otherwise, lies in the 2-D diamond $\{(x,y') : |x| + |y'| \le t\}$.
background
This module finishes the exact edge count for the polarized conjugate-birth interface on the 2-D diamond (and its 3-D octahedron lift). Phase 51 already confined recognition-active edges to the codimension-1 spine $x = 0$ and showed the spine is sub-extensive; here the ordered bichromatic edge list is counted by an explicit bijection with index data $(y, \mathrm{side}, \mathrm{orientation})$ for interior spine heights $|y| \le t-1$.
The ambient domain is the L1 ball ball t: lattice points with $|x| + |y| \le t$. Membership is characterized by mem_ball_iff. The spine is the column $x = 0$ inside that ball. Each bichromatic edge has one spine endpoint $(0,y)$ and one neighbour $(\pm 1, y)$; the present lemma is the neighbour half of the vertex-wellformedness obligation for that reconstruction.
The spatial dimension forced by the chain is $D = 3$, but this lemma lives in the 2-D diamond namespace used as the model case before the octahedron lift.
proof idea
Unpack membership of $a$ in the index product: the height coordinate satisfies $-!(t-1) \le y \le t-1$ (the Bool factors are discarded). Rewrite the goal via Diamond.mem_ball_iff as $|\varepsilon| + |y| \le t$ with $\varepsilon \in {+1,-1}$. Case-split on the side bit; in each branch natAbs of $\pm 1$ is 1, and omega closes $|y| + 1 \le t$ from the unpacked bounds.
why it matters
Needed by edgeFromIndex, which rebuilds each ordered bichromatic edge from its index triple and must package both endpoints as vertices of the birth domain. Without neighbour membership, the Finset bijection that proves interface_card_eq (ordered count $8t-4$) and the headline interface_increment_const (exactly 8 new ordered edges per cadence step) cannot typecheck.
That constant increment is the Lean form of the compute-watch principle on the 2-D model: recognition activity per cycle is $O(1)$ while volume is $\Theta(t^2)$. The octahedron lift (forced $D = 3$ from the T8/T9 chain) replaces the constant by a linear $\Theta(t)$ surface growth, still strictly sub-extensive in the $\Theta(t^3)$ volume. This lemma is a small but load-bearing wellformedness step on that counting path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.