idx_card
plain-language theorem explainer
For radius t ≥ 1, the index set that labels 2-D polarized-birth interface edges has cardinality exactly 8t − 4. Cosmology and compute-watch arguments cite this as the size of the parameter space {interior spine y} × {side, orientation}. The proof is a short Finset product-cardinality calculation plus omega arithmetic.
Claim. For every natural number $t \ge 1$, the finite index set $\mathrm{Icc}(-(t-1), t-1) \times \{\mathrm{true},\mathrm{false}\}^2$ has cardinality $8t - 4$. Equivalently, there are $2t-1$ admissible interior spine coordinates $y$ and $4$ choices of (side, orientation).
background
This module finishes the exact edge count for the recognition-active interface of the forced conjugate-birth field in 2-D. Phase 51 confined that interface to the codimension-1 spine and bounded spine cells; here the ordered bichromatic edges are counted exactly.
The ambient geometry is the L1 diamond (ball) of radius $t$: lattice points with $|x|+|y|\le t$. The spine is the column $x=0$ inside that diamond. Interface edges are bichromatic adjacencies with one endpoint on the spine and one neighbour at $x=\pm 1$ sharing the same $y$.
The index set packages those edges as triples $(y,\mathrm{side},\mathrm{orient})$: $y$ runs over the interior spine segment $|y|\le t-1$ (the cells that actually have an $x=\pm 1$ neighbour), and the two Booleans encode which side and which directed orientation. Its cardinality is the combinatorial size that the later bijection equates to the true edge set.
proof idea
Unfold the definition of the index set as a Cartesian product of an integer closed interval with the universe of $\mathrm{Bool}\times\mathrm{Bool}$. Apply Finset.card_product and Int.card_Icc to separate the factors. The Boolean pair universe has card $4$ by decide. The remaining arithmetic identity
$$(2t-1)\cdot 4 = 8t-4$$
(for $t\ge 1$) is discharged by omega.
why it matters
This is the numeric half of the exact 2-D interface count. Downstream, interface_card_eq rewrites its goal through this lemma and builds a Finset.card_bij' between the filtered bichromatic edge set and the index set, concluding that the ordered interface has size $8t-4$.
That equality feeds the headline corollary: the interface grows by exactly $8$ ordered edges each cadence step $t\to t+1$, independent of world volume. In Recognition Science terms this is the compute-watch principle in Lean: recognition cost tracks interface activity $O(1)$ per cycle, not the $\Theta(t^2)$ diamond volume. The same counting pattern lifts in the Octahedron namespace to $D=3$ (forcing-chain T8), where the interface becomes a growing disk and the increment is $\Theta(t)$ rather than constant, still sub-extensive in volume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.