edgeIndex
plain-language theorem explainer
Encodes a bichromatic ordered edge on the 2-D diamond as the triple (spine y-coordinate, side of the ±1 neighbour, orientation). Downstream cardinality proofs cite it as one half of the explicit bijection between interface edges and interior-spine index data. The definition is a two-branch case split on which endpoint lies on the spine x = 0.
Claim. For radius $t$ and an ordered pair of diamond vertices $p = (u,v)$, the edge index is $(y, s, o) \in \mathbb{Z} \times \{\mathrm{true},\mathrm{false}\}^2$: if the first endpoint has $x=0$, take its $y$-coordinate, the sign of the second endpoint's $x$, and orientation $\mathrm{true}$; otherwise take the second endpoint's $y$, the sign of the first endpoint's $x$, and orientation $\mathrm{false}$.
background
The module counts recognition-active interface edges of the polarized conjugate-birth field on the 2-D L1 diamond. Phase 51 confined that interface to the codimension-1 spine and bounded spine cells; this file upgrades the bound to an exact ordered-edge count.
Vertices are lattice points in the diamond ball: $V_t = {p \in \mathbb{Z}^2 : p \in B(t)}$. A bichromatic edge joins a spine point $(0,y)$ to a neighbour $(\pm 1, y)$ sharing the same $y$. The index packages exactly that data: spine $y$, which side the off-spine neighbour sits on, and which way the ordered pair is oriented.
Upstream, $D=3$ is the spatial dimension forced by the T8/T9 chain, but the ambient count here is the 2-D diamond model used before the Octahedron lift.
proof idea
Pure definition by case split, not a proof. If the first component of the ordered pair has first coordinate $0$, it is treated as the spine endpoint: return its second coordinate as $y$, whether the second vertex has positive first coordinate as the side bit, and orientation true. Otherwise the second component is treated as the spine endpoint, with orientation false and the side bit read from the first vertex. The inverse reconstruction is the sibling edgeFromIndex.
why it matters
Feeds interface_card_eq, which proves the exact 2-D ordered interface cardinality is $8t-4$ by Finset.card_bij' with this map and its inverse. That identity is the bridge from the engine's filtered edge list to a closed form, and yields the headline corollary that the interface grows by exactly 8 ordered edges per cadence cycle, independent of world size.
In the Recognition compute-watch reading, cost tracks recognition activity (interface increment), not volume: $O(1)$ per cycle in 2-D against $\Theta(t^2)$ area. The Octahedron namespace lifts the same indexing idea to $D=3$, where the increment becomes $\Theta(t)$ on a growing spine disk. This definition is the concrete coordinate chart that makes the bijection, and thus the constant-increment statement, machine-checkable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.