threePath_interface
plain-language theorem explainer
The left and right halves of the three-edge path diamond share exactly one vertex, the middle node of the path. Anyone evaluating the J-diamond defect on this seed complex cites the fact to pin the interface before summing the imbalance product. The proof unfolds the two Finset vertex sets and checks equality by cases on Fin 4.
Claim. For the three-edge path on vertices $\{0,1,2,3\}$, the left subcomplex (front two edges, vertices $\{0,1,2\}$) and the right subcomplex (last edge, vertices $\{2,3\}$) have interface $V_L \cap V_R = \{2\}$.
background
This module 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 failure
$$D(A,B;I)=SJ(A)+SJ(B)-SJ(I)-SJ(K),$$
with $SJ=2\kappa J$ the integer squared-imbalance total. The localization theorem factors $D$ as $-2$ times the sum of products of the two imbalance fields over interface vertices, so the interface set must be known exactly before any numerical evaluation.
The three-edge path is the next seed after the two-edge A15 witness. Its left half takes the front two edges (vertices ${0,1,2}$); its right half takes the last edge (vertices ${2,3}$). Their common vertices are the only place the imbalance product can be nonzero.
proof idea
One-line definitional reduction: rewrite the two vertex sets by their constructors, then prove set equality by ext on v : Fin 4 and fin_cases with simp. No external lemmas; pure Finset arithmetic on four points.
why it matters
Feeds threePath_diamond_defect, which rewrites the defect via the localization identity, substitutes this interface singleton, and obtains $D=2$ from the middle-vertex imbalances $m_A(2)=1$, $m_B(2)=-1$. That numerical seed, together with the empty-interface and balanced-interface vanishing lemmas, is packaged into the module verdict jDiamondRankVerdict (Gap 2 / C15). The path diamond is the smallest connected example where the interface is a single interior vertex rather than a glue point of two edges, confirming that the coupling formula localizes correctly beyond the A15 seed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.