B
plain-language theorem explainer
At radius t, B(t) is the Finset of ordered vertex pairs that are 4-adjacent and carry unequal polarization. It is the recognition-active interface of the polarized birth diamond: the forced distinctions the engine posts. Downstream edge-count theorems cite it as the exact object whose cardinality is 8t-4. The body is a one-line filter of the universal product of diamond vertices.
Claim. For each $t \in \mathbb{N}$, let $B(t)$ be the finite set of ordered pairs $(p,q)$ of vertices in the L1 diamond of radius $t$ such that $p$ and $q$ are 4-neighbours (L1 distance exactly one) and the polarized charges of $p$ and $q$ differ.
background
The ambient graph is the 2-D L1 diamond of radius $t$: vertices Vtx t are lattice points in the ball of radius $t$, and adjacency is the 4-neighbour relation (L1 distance exactly one). Polarization is the forced conjugate-birth charge: $+1$ on the fine half $x>0$, $-1$ on the coarse half $x<0$, and $0$ on the spine $x=0$.
Phase 51 confined the recognition-active interface of this field to the codimension-1 spine and showed the spine is sub-extensive, but only bounded spine cells. This module upgrades that to an exact ordered-edge count. The object being counted is precisely the bichromatic ordered edges: adjacent pairs whose polarization values disagree.
Those edges are the forced distinctions the recognition engine posts each cycle. The module's headline is that their number grows by a constant independent of world size, so cost tracks interface activity rather than volume.
proof idea
Pure definition, not a proof. Take the universal Finset of ordered pairs of diamond vertices and retain those pairs that satisfy both adjacency and unequal polarization. Noncomputable only because the ambient vertex type is a subtype of integer pairs; the filter itself is decidable from the decidable adjacency and polarization predicates.
why it matters
B is the interface object that the rest of the module measures. Sibling results bridge its Finset cardinality to the engine's toList edge length, then evaluate the card by an explicit bijection onto interior-spine height times side times orientation, yielding the exact count $8t-4$. The corollary is constant per-cycle growth of eight ordered edges as $t\mapsto t+1$, independent of world size: the Lean form of the compute-watch principle (cost scales with recognition activity, not $\Theta(t^2)$ volume).
The Octahedron namespace lifts the same construction to the forced spatial dimension $D=3$ (T8/T9), where the interface becomes a growing 2-D spine disk with ordered count $8t^2-8t+4$ and linear increment $16t$. Net run totals remain $\Theta(T^{D-1})$, strictly sub-extensive against brute-force spacetime cost. Downstream CostAlgebra and nucleosynthesis edges in the graph are name-collision noise on the short identifier; the real consumers are the interface card, length, and increment theorems in this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.