interface_card_eq
plain-language theorem explainer
For radius t ≥ 1, the polarized 2-D diamond has exactly 8t − 4 ordered bichromatic interface edges. Cosmology and compute-watch arguments cite this as the exact perimeter cost the engine must post. The proof is a Finset bijection from those edges onto interior spine heights times side and orientation, whose index set has cardinality 8t − 4.
Claim. For every natural number $t \ge 1$, the finite set of ordered adjacent pairs of lattice vertices in the $L^1$ diamond of radius $t$ on which the polarized birth field takes opposite values has cardinality $8t - 4$.
background
The module sits in the polarized-birth cosmology stack. Phase 51 confined recognition-active distinctions of the forced conjugate-birth field to a codimension-1 spine and bounded spine cells, but left the exact interface edge count open. This file closes that gap for the 2-D diamond and records the constant per-cycle increment.
The ambient geometry is the $L^1$ ball (diamond) of radius $t$: lattice points with $|x|+|y|\le t$. Adjacency is 4-neighbour: $L^1$ distance exactly one. Vertices carry a polarization; the interface $B(t)$ is the Finset of ordered adjacent pairs on which the two endpoints have unequal polarization. Those bichromatic edges are the forced distinctions the recognition engine posts.
Upstream, membership in the diamond is characterized by mem_ball_iff, and the edge list is the filter of adjacent ordered pairs inside the ball. The structural fact used here is that every bichromatic edge meets the spine $x=0$ at exactly one endpoint and a neighbour at $(\pm 1,y)$ sharing the same $y$.
proof idea
Rewrite the claim as equality with the cardinality of an explicit index Finset idx t (via the sibling idx_card). Then apply Finset.card_bij' with maps edgeIndex and edgeFromIndex.
Forward: from a bichromatic adjacent pair, edge_structure splits into the two cases (spine endpoint on the left or right). In each case the shared $y$ lands in $I_{cc}(-(t-1),t-1)$ and the side/orientation bits fill the remaining coordinates of idx.
Backward: edgeFromIndex rebuilds a pair from $(y,\mathrm{side},\mathrm{orient})$; adjacency and polarization mismatch are checked by case split and omega.
The two inverse laws are pure case analysis on the same spine dichotomy, using Subtype.ext / Prod.ext and the defining equations of the index maps. The index set itself is a product whose size is $8t-4$.
why it matters
This is the exact 2-D interface edge count the module advertises: ordered edges equal $8t-4$ (twice the undirected perimeter $4t-2$). Downstream, carried_edge_card subtracts it from the total adjacency $8t^2$ to get the monochromatic bulk $8t^2-8t+4$; carried_ge_interface then shows carried edges dominate the interface for $t\ge 1$. The discrete isoperimetric laws interface_sq_le_total and (in 3-D) interface_cube_le_total_sq rewrite the interface side via this identity. Cost-side, interfaceCost_card feeds the same count into recognition cost.
In the framework this is the Lean form of the compute-watch principle in $D=2$: recognition activity is the interface increment, $O(1)$ per cadence cycle (interface_increment_const grows by exactly 8 ordered edges when $t\mapsto t+1$), while volume is $\Theta(t^2)$. The forcing chain selects $D=3$ (T8); the Octahedron lift replaces the constant increment by a linear $\Theta(t)$ surface law, still sub-extensive in $\Theta(t^3)$ volume. Net run totals remain $\Theta(T^{D-1})$ forced distinctions rather than brute-force spacetime $\Theta(T^{D+1})$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.