threePathRight

This module 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 complex is the three-edge path $0\to 1\to 2\to 3$ (four vertices, three edges). The right piece takes only the last edge and its two endpoints. Together with the complementary left piece (first two edges), it forms an edge-partition diamond whose interface is the middle vertex $2$.

Definitional construction of a Subcomplex record. Vertices are hardcoded as ${2,3}$ and edges as the singleton ${2}$. The two closure fields are discharged by singleton membership: the unique edge has tail $2$ and head $3$, both already in the vertex set. No external lemmas beyond Finset singleton facts.

Supplies the right side of the three-edge path diamond, the concrete witness that the localization theorem is sharp on a path. Downstream, threePath_edges_cover and threePath_edges_disjoint show the left/right edges partition the path; threePath_interface identifies the interface as ${2}$; subImbalance_threePathRight_two gives imbalance $-1$ at vertex $2$; and threePath_diamond_defect assembles these into defect $2$ via diamondDefect_eq_neg_two_inner (middle vertex carries $m_A=1$, $m_B=-1$).

That nonzero defect is part of Gap 2 / C15: the rank-and-consistency test on J-diamonds after the census-inversion route was ruled out. It shows the interface-imbalance coupling is realized on the simplest nontrivial path geometry.