interface_length_eq
plain-language theorem explainer
For the 2-D diamond birth field of radius t ≥ 1, the filtered list of ordered bichromatic edges (adjacent vertices with unequal polarized charge) has length exactly 8t − 4. Cosmology and compute-watch arguments cite this as the numeric form the engine sees. The proof is a two-rewrite bridge from list length to the already-proved Finset cardinality.
Claim. For every natural number $t \ge 1$, the length of the list of ordered adjacent pairs drawn from the 4-neighbour edge list of the radius-$t$ diamond whose two endpoints carry unequal polarized birth charge equals $8t - 4$.
background
The module closes the exact interface edge count for the forced conjugate-birth field on the 2-D diamond. Phase 51 already confined recognition-active edges to the codimension-1 spine and bounded spine cells; here the bichromatic ordered-edge list is counted exactly.
The edge list edges t is every ordered adjacent pair of diamond vertices under the 4-neighbour relation. The polarized charge assigns $+1$ on the fine half $x > 0$, $-1$ on the coarse half $x < 0$, and $0$ on the spine $x = 0$. Bichromatic edges are those whose endpoints disagree under this charge; they are the recognition-active interface the engine filters.
Upstream, interface_card_eq already proves the corresponding Finset has cardinality $8t - 4$ by an explicit bijection onto interior spine sites times side and orientation. A sibling lemma equates list length of the filtered edge list to that Finset card.
proof idea
Two rewrites. First apply the sibling that identifies the filtered list length with the Finset cardinality of the same bichromatic predicate. Then apply interface_card_eq at the given $t \ge 1$, which supplies the closed form $8t - 4$. No further case analysis or bijection work is done here; those live in the Finset count.
why it matters
This is the form the numeric layer and the engine's comp / interface-succession machinery actually consume: list length, not abstract Finset card. The module headline corollary interface_increment_const (constant $+8$ ordered interface edges per cadence step $t \to t+1$) rests on this closed form, as does the 2-D compute-watch statement that forced distinctions per cycle are $O(1)$ while world volume grows as $\Theta(t^2)$.
In the Recognition framework this is the Lean statement that simulation cost tracks recognition activity on the interface, not bulk volume. The Octahedron lift (D = 3, forced by the T8/T9 chain) replaces the constant increment by a linear $\Theta(t)$ surface law; the 2-D count here is the clean base case. No downstream theorems currently depend on this declaration in the graph, but the sibling increment and total-growth corollaries are the intended consumers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.