twoEdge_interface_empty
plain-language theorem explainer
The left and right single-edge subcomplexes of the two-edge control complex have disjoint vertex sets. Anyone applying the empty-interface exactness corollary to this diamond cites this fact. The proof is exhaustive case analysis on the four vertices of the ambient Fin 4 carrier.
Claim. Let $K$ be the two-edge complex on four vertices, and let $A$ and $B$ be its two single-edge subcomplexes (the left edge on vertices $\{0,1\}$ and the right edge on the complementary pair). Then the vertex sets are disjoint: $V(A) \cap V(B) = \emptyset$.
background
Gap 2 studies J-diamonds: unordered pairs of proper subcomplexes of a posting graph whose union is the whole complex $K$. The diamond defect is the four-term inclusion-exclusion remainder
$$D(A,B;I)=SJ(A)+SJ(B)-SJ(I)-SJ(K),$$
with $SJ=2\kappa J$ the integer squared-imbalance total. Recognition cost $J$ is not a valuation, so $D$ need not vanish.
A subcomplex is an edge subset together with a vertex set closed under endpoints. The two-edge complex is the smallest disjoint-union control: two edges on four distinct vertices, split as left and right single-edge subcomplexes. The localization theorem factors $D$ as $-2$ times the sum of products of the two imbalance fields on interface vertices, so an empty interface forces $D=0$.
proof idea
Term-mode tactic proof by set extensionality on vertices. Every vertex lives in Fin 4; fin_cases splits into four singleton goals. Each goal reduces by simp against the concrete vertex Finsets in the definitions of the left and right subcomplexes (left holds ${0,1}$; right holds the complementary pair), so membership in the intersection is false in every case.
why it matters
This is the geometric hypothesis that unlocks the disjoint control diamond. Downstream, twoEdge_diamond_defect applies the empty-interface corollary and concludes defect $0$ on this complex; that control sits inside the aggregate jDiamondRankVerdict bundle (empty-interface exactness field). In the Gap 2 / C15 program it separates pure disjoint union (always exact) from genuine interface coupling, where the seed diamond with one shared vertex produces the nonzero A15 witness. It does not itself compute a defect; it only certifies the empty-interface premise.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.