twoEdgeLeft
plain-language theorem explainer
Defines the left half of the two-edge control complex: vertices {0,1} and the single edge 0→1 inside the four-vertex graph of two disjoint edges. Gravity and Gap-2 diamond-rank arguments cite it as one side of the empty-interface J-diamond. The body is a structure instance with two short membership proofs that endpoints lie in the vertex set.
Claim. Let $K$ be the bounded complex of two disjoint edges on four vertices ($0\to 1$ and $2\to 3$). The left subcomplex is the pair of vertex set $\{0,1\}$ and edge set $\{0\}$, with both endpoints of edge $0$ required to lie in $\{0,1\}$.
background
Gap 2 / C15 studies J-diamonds: four-term inclusion-exclusion defects of the recognition cost $J$ (via the integer squared-imbalance total $SJ$) on pairs of proper subcomplexes of a posting graph. A subcomplex is a subset of edges together with a vertex subset closed under endpoints.
The ambient object is twoEdgeComplex: four vertices, two edges $0\to 1$ and $2\to 3$, no triangles. That complex is the disjoint control for the localization theorem diamondDefect_eq_neg_two_inner, which factors the diamond defect as $-2$ times the sum of products of the two imbalance fields on the interface. Empty interface forces defect zero.
This definition packages the first edge as a Subcomplex instance so cover, disjointness, and empty-intersection lemmas can name both sides of the diamond.
proof idea
Structure instance, not a theorem. Vertex field is the Finset ${0,1}$; edge field is the singleton ${0}$. The two obligations tail_mem and head_mem are discharged by singleton elimination on the edge index, then Finset insert/singleton membership for vertices $0$ and $1$ respectively. No upstream lemmas beyond Finset API.
why it matters
Supplies one leg of the disjoint-edge control diamond in the J-diamond rank lattice. Downstream, twoEdge_edges_cover, twoEdge_edges_disjoint, and twoEdge_interface_empty establish that the two sides partition the edge set and meet in no vertices; twoEdge_diamond_defect then concludes defect $0$ by the empty-interface corollary. The hostile probe probe_disjoint_defect_SJ reuses the same identity.
In the module narrative this is the positive control opposite the A15 seed (two edges glued at one vertex, nonzero defect). It confirms that $J$'s failure of valuation is localized to two-sided interface imbalance, not a global bookkeeping error. That localization is the successor test after Gap2JEhrhartSpan ruled out census inversion for the three per-kind rates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.