pathRight
plain-language theorem explainer
The right half of the two-edge path 0→1→2: vertices {1,2} and the single edge 1→2, packaged as a closed subcomplex. Anyone citing the A15 seed J-diamond (defect 1/κ) uses this as one accumulation side. Endpoint closure is discharged by singleton membership on the edge index.
Claim. On the path complex $0 \to 1 \to 2$, the right subcomplex consists of the vertex set $\{1,2\}$ and the single edge from $1$ to $2$, with both endpoints of that edge lying in the vertex set.
background
Gap 2 / C15 studies J-diamonds: four-term inclusion-exclusion defects of the recognition cost $J$ on overlapping subregions of a posting graph. A subcomplex of a bounded complex is a subset of edges together with a vertex subset 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 here is the two-edge path $0\to 1\to 2$ (three vertices, two edges), the smallest A15 witness. The left and right halves partition its edges and meet at the middle vertex; their diamond is the seed used throughout the localization and rank arguments in this module.
proof idea
Definitional construction of a Subcomplex on the path complex. Vertices are the Finset ${1,2}$; edges are the singleton ${1}$. The two closure obligations (tail and head of every chosen edge lie in the vertex set) are proved by reducing membership in the singleton edge set to equality, then applying insert/singleton membership on ${1,2}$.
why it matters
This is one side of the A15 seed diamond. Downstream, seed_edges_cover and seed_edges_disjoint show left and right partition the path edges; seed_diamond_defect evaluates $D=2$ in $1/(2\kappa)$ units (i.e. $1/\kappa$ in $J$ units); seed_diamond_localized and seed_inner_product pin the interface coupling $m_A(1)\cdot m_B(1)=-1$ at the shared vertex. Those facts feed JDiamondRankVerdict, the C15 lattice verdict (localization, even spectrum, kernel diamonds, rank and seed-row inconsistency). In the broader RS gravity program this is the finite witness that $J$ fails to be a valuation and that defects localize on two-sided interface imbalance.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.