edgeFromIndex
plain-language theorem explainer
Reconstructs a bichromatic ordered edge of the 2-D diamond from its index triple (spine height y, lateral side, orientation). Downstream the exact interface count 8t−4 cites this as the inverse half of the Finset bijection. The body is a two-branch case on orientation that places the spine endpoint (0,y) first or second and the neighbour (±1,y) opposite.
Claim. Given radius $t$ and an index triple $a=(y,s,o)\in\mathrm{idx}(t)$ (interior spine height, side flag, orientation flag), return the ordered pair of diamond vertices forming the corresponding bichromatic edge: one endpoint is the spine point $(0,y)$ and the other is the neighbour $(\pm 1,y)$ chosen by $s$, ordered by $o$.
background
The module closes the exact ordered-edge count of the recognition-active interface of the polarized birth field in 2-D. Phase 51 confined that interface to the codimension-1 spine and bounded spine cells; here the bichromatic edges themselves are counted.
Vertices Vtx t are lattice points of the L1 ball of radius $t$. The ambient edge list is every ordered 4-neighbour adjacency in that diamond. Bichromatic edges are those with exactly one endpoint on the spine $x=0$. Each such edge is determined by an interior spine height $y$ with $|y|\le t-1$, a side $(\pm 1)$, and an orientation (spine-to-neighbour or reverse).
The companion index set packages those three data as $\mathbb{Z}\times\mathrm{Bool}\times\mathrm{Bool}$. Membership lemmas memSpine and memNbr certify that the reconstructed points lie in the ball, so the output type is a genuine pair of vertices.
proof idea
Pure constructive definition, no proof obligations beyond the membership certificates already supplied by memSpine and memNbr.
Read the triple as $(y,\mathrm{side},\mathrm{orient})$. The spine endpoint is always $(0,y)$; the neighbour is $(1,y)$ or $(-1,y)$ according to the side flag. If the orientation flag is true, emit (spine, neighbour); otherwise emit (neighbour, spine). The two branches are therefore the two ordered orientations of the same undirected adjacency.
why it matters
This is the inverse map in the explicit bijection that proves interface_card_eq: the ordered bichromatic edge set $B(t)$ has cardinality $8t-4$. That theorem applies Finset.card_bij' with forward map edgeIndex and reverse map edgeFromIndex, so without this reconstruction the card equality does not close.
The count feeds the headline corollary interface_increment_const: the interface grows by exactly 8 ordered edges per cadence step $t\to t+1$, independent of world size. In Recognition terms this is the 2-D compute-watch statement: forced distinctions per cycle are $O(1)$ while volume is $\Theta(t^2)$. The same pattern lifts in the Octahedron namespace to $D=3$ (forced by the T8/T9 chain), where the increment becomes linear in $t$ because the active interface is a growing disk.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.