memSpine
plain-language theorem explainer
For every interface index at radius t, the spine lattice point (0, y) lies inside the 2-D L1 diamond of radius t. Anyone building the explicit edge bijection for the polarized-birth interface cites this as the membership certificate for the spine endpoint. The proof unpacks the index interval |y| ≤ t−1 and closes |0|+|y| ≤ t by omega via the diamond membership criterion.
Claim. Let $t\in\mathbb{N}$ and let $a=(y,s,o)$ belong to the index set of interior spine coordinates $|y|\le t-1$ paired with side and orientation bits. Then the spine cell $(0,y)$ lies in the 2-D diamond $\{(x,y')\in\mathbb{Z}^2:\,|x|+|y'|\le t\}$.
background
This module finishes the exact ordered-edge count of the recognition-active interface of the forced conjugate-birth field. Phase 51 confined that interface to the codimension-1 spine and bounded spine cells; here the bichromatic ordered edges are counted exactly, yielding $8t-4$ in 2-D and the constant per-cycle increment of 8.
The ambient domain is the 2-D diamond ball t: the L1 ball $|x|+|y|\le t$ realized as a Finset. Membership is characterized by mem_ball_iff: $(x,y)\in\mathrm{ball},t$ if and only if $x.\mathrm{natAbs}+y.\mathrm{natAbs}\le t$.
The index set idx t parameterizes those edges: interior spine $y$-coordinates in $[-t+1,t-1]$ times the four (side, orientation) pairs. Its cardinality is $8t-4$. Each index is meant to name a unique bichromatic edge with one endpoint on the spine $x=0$ and one neighbour at $x=\pm 1$.
proof idea
Unpack membership in idx t via the product and closed-interval characterizations to obtain the bounds $-t+1\le y\le t-1$ on the spine coordinate (the Bool pair is discarded). Rewrite the goal with Diamond.mem_ball_iff, reducing it to $|0|+|y|\le t$. The interval bounds give $|y|\le t-1$, so omega finishes the arithmetic.
why it matters
The reconstruction map edgeFromIndex builds each ordered bichromatic edge from index data $(y,\mathrm{side},\mathrm{orient})$ and needs a proof that the spine endpoint $(0,y)$ is a vertex of the diamond; this theorem supplies that certificate (the companion memNbr does the same for $(\pm 1,y)$).
Those certificates feed the explicit bijection that proves interface_card_eq ($8t-4$ ordered edges) and the headline corollary interface_increment_const: the interface grows by exactly 8 ordered edges per cadence cycle, independent of world size. That is the Lean form of the compute-watch principle: cost tracks recognition activity $O(1)$ per cycle, not volume $\Theta(t^2)$.
In the broader forcing chain this sits under the D=3 lift (Octahedron), where the same spine-membership pattern supports the surface count $8t^2-8t+4$ and linear increment $16t$, still sub-extensive against $\Theta(t^3)$ volume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.