twoEdgeRight
plain-language theorem explainer
Names the right half of the two-edge control complex: the single edge on vertices {2,3} inside the four-vertex graph of two disjoint edges. Downstream diamond-defect and cover lemmas cite it as one side of a J-diamond with empty interface. The body is a structure instance with two Finset fields and endpoint-closure proofs by singleton case analysis.
Claim. Let $K$ be the bounded complex on four vertices and two edges $0\to 1$ and $2\to 3$. The right subcomplex is the edge subset $\{1\}$ with vertex set $\{2,3\}$, closed under endpoints.
background
Gap 2 / C15 studies J-diamonds: four-term inclusion-exclusion defects of the recognition cost $J$ on overlapping subcomplexes of a posting graph. A subcomplex is a subset of edges together with a vertex set closed under their endpoints. The diamond defect is $D(A,B;I)=SJ(A)+SJ(B)-SJ(I)-SJ(K)$ with $SJ=2\kappa J$; valuations have $D=0$, but $J$ is not a valuation.
The ambient object is twoEdgeComplex: two disjoint edges $0\to 1$ and $2\to 3$ on four vertices. This definition packages the second edge as a Subcomplex of that complex. Its twin is the left edge on vertices ${0,1}$. Together they form the disjoint-union control diamond used to check that empty-interface gluings have vanishing defect.
proof idea
Structure instance, not a theorem. Vertices are the Finset ${2,3}$ and edges the singleton ${1}$. Endpoint closure is discharged by singleton membership: the unique edge is edge 1, whose tail and head land in ${2,3}$ by the edge-vertex table of the two-edge complex. Both obligations are short intro/obtain rfl/exact scripts.
why it matters
Supplies one side of the disjoint control diamond in the J-diamond rank lattice. Parent results use it to prove edge cover of the full complex, edge disjointness from the left half, empty vertex interface, and hence twoEdge_diamond_defect: defect $0$ by the empty-interface corollary of the localization theorem $D=-2\sum_v m_A(v)m_B(v)$. The hostile probe re-exports that vanishing as a sanity check.
In the module narrative this is the baseline where inclusion-exclusion cannot fail: disjoint union never produces a nonzero diamond defect. That isolates genuine nonzero defects (the A15 seed glued along one vertex) as interface-imbalance phenomena rather than bookkeeping artifacts, feeding the rank and consistency test on the relation lattice of J-diamonds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.