idx
plain-language theorem explainer
Defines the finite index set that labels every ordered bichromatic interface edge of the 2-D polarized birth diamond of radius t. Each triple is an interior spine height y with |y| ≤ t−1 together with a side (±1) and an orientation bit. Downstream cardinality and bijection proofs cite it to show the interface has exactly 8t−4 ordered edges. The body is a plain product of an integer interval with the four-element Bool×Bool universe.
Claim. For each radius $t\in\mathbb{N}$, let $\mathrm{idx}(t)$ be the finite set $\{y\in\mathbb{Z}: |y|\le t-1\}\times\{\mathrm{true},\mathrm{false}\}^2$. Elements are triples $(y,\mathrm{side},\mathrm{orient})$ parameterising interior spine cells that admit an $x=\pm 1$ neighbour, together with which side and which directed orientation the edge uses.
background
The module counts recognition-active interface edges of the forced conjugate-birth field on the 2-D L1 diamond. Phase 51 already confined activity to the codimension-1 spine (the column $x=0$ inside the diamond $|x|+|y|\le t$) and showed the spine is sub-extensive, but only bounded spine cells, not edges.
The spine is the filter of the diamond ball to $x=0$, equivalently the image of $[-t,t]$ under $y\mapsto(0,y)$. Interior spine cells are those with $|y|\le t-1$: only they have a lattice neighbour at $x=\pm 1$ still inside the diamond. Each bichromatic interface edge joins one such spine cell to one side neighbour and may be listed in either orientation, so the discrete data of an edge is exactly $(y,\mathrm{side},\mathrm{orient})$.
This definition packages that parameter space as a Finset product: the closed integer interval from $-(t-1)$ to $t-1$, crossed with the four-element universe of Bool × Bool.
proof idea
Definitional, not a proof. The body is the Cartesian product of Finset.Icc (-↑t + 1) (↑t - 1) with Finset.univ on Bool × Bool. No lemmas are applied; the subsequent theorem idx_card rewrites this product, uses Int.card_Icc and decide for the four Boolean pairs, then closes with omega to obtain cardinality $8t-4$.
why it matters
This index set is the domain of the explicit bijection that proves the headline 2-D count interface_card_eq: the ordered bichromatic edge set $B(t)$ has cardinality $8t-4$. The maps edgeIndex and edgeFromIndex send edges to triples in idx(t) and back, so Finset.card_bij' transfers the product count to the interface.
From that equality the module derives interface_increment_const: each cadence step $t\to t+1$ adds exactly eight ordered edges, independent of world size. That is the Lean form of the compute-watch principle: recognition cost tracks the interface increment $O(1)$ per cycle, not the $\Theta(t^2)$ volume. The same pattern lifts in the Octahedron namespace to $D=3$ (forced by the T8/T9 chain), where the index becomes interior spine disk times side/orient and the increment is linear in $t$.
Local consumers include idx_card, memSpine/memNbr, edgeFromIndex, and interface_card_eq.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.