interface_length_eq_card
plain-language theorem explainer
For the polarized diamond birth field at radius t, the length of the ordered edge list filtered to bichromatic pairs equals the cardinality of the bichromatic edge Finset B(t). Anyone counting the recognition-active interface via the engine's list filter cites this bridge. The proof is a short Nodup-to-card argument: filtering preserves uniqueness of Finset.toList, then set extensionality matches membership to B.
Claim. For every natural number $t$, the length of the ordered 4-neighbour edge list of the diamond of radius $t$, restricted to pairs whose polarized charges differ, equals the cardinality of the Finset $B(t)$ of ordered adjacent pairs with unequal polarization.
background
This module sits in the polarized-birth cosmology stack. Phase 51 confined the recognition-active interface of the conjugate-birth field to the codimension-1 spine and bounded spine cells; the present file upgrades that to an exact ordered-edge count.
The ambient graph is the 2-D diamond of radius $t$. The list edges t is every ordered adjacent pair under the 4-neighbour relation (the toList of the adjacency Finset). Polarization assigns each vertex a charge; bichromatic pairs are those with unequal charge. The Finset $B(t)$ is exactly those ordered adjacent pairs with unequal polarization: the interface the engine posts as forced distinctions.
Membership in the edge list is characterized by adjacency alone (mem_edges). The bridge needed before any numeric count is that the filtered list length agrees with $|B(t)|$, so later bijections on Finsets transfer to the concrete list the numeric layer sees.
proof idea
First prove the filtered edge list is Nodup: apply List.Nodup.filter to Finset.nodup_toList on the adjacency Finset underlying edges t. Rewrite the goal via List.toFinset_card_of_nodup, reducing length to the card of the corresponding Finset. Congruence plus ext on pairs $(a,b)$ finishes: simp with List.mem_toFinset, List.mem_filter, mem_edges, decide_eq_true_eq, and the definition of $B$ shows the two Finsets have identical membership (adjacency and unequal polarization).
why it matters
This is the list-to-Finset bridge named in the module doc: without it, the exact count stays on the Finset side while the engine and the comp/mono_le_interface_succ machinery consume filtered list lengths.
Downstream, interface_card_eq evaluates $|B(t)| = 8t-4$ by an explicit bijection onto interior spine $y$ times side and orientation. Then interface_length_eq rewrites through this theorem to conclude the concrete filtered list has length $8t-4$. That numeric form feeds interface_increment_const: advancing $t\to t+1$ adds exactly eight ordered interface edges, constant and independent of world size.
In Recognition terms this is the 2-D compute-watch law: cost tracks recognition activity (interface increment $O(1)$ per cycle), not volume $\Theta(t^2)$. The same pattern lifts in the Octahedron namespace to $D=3$ (forced by the T8/T9 chain), where the increment becomes linear in $t$ on a growing codimension-1 disk.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.