threePathLeft
plain-language theorem explainer
Defines the left half of the three-edge path as a subcomplex: vertices 0,1,2 and the first two edges. Anyone computing the path J-diamond (defect 2 at the middle vertex) cites this side. The body is a structure instance with two Finset membership proofs that endpoints stay inside the vertex set.
Claim. On the three-edge path complex $0\to 1\to 2\to 3$, the left subcomplex consists of vertex set $\{0,1,2\}$ and edge set $\{0,1\}$ (the front two edges), with both endpoints of each chosen 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 subcomplexes of a posting graph. A subcomplex 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 three-edge path $0\to 1\to 2\to 3$ (four vertices, three edges). The localization theorem factors the defect through interface imbalance products: $D=-2\sum_v m_A(v)m_B(v)$ on the interface. This left piece is one side of the standard path diamond used to exhibit a concrete nonzero defect.
proof idea
Structure instance for Subcomplex on threePathComplex. Vertex field is the Finset ${0,1,2}$; edge field is ${0,1}$. The two obligations tail_mem and head_mem are discharged by case-splitting on edge membership (Finset.mem_insert / singleton) and inserting the corresponding endpoint into the vertex Finset. No external lemmas beyond Finset membership.
why it matters
Supplies the left arm of the three-path J-diamond. Downstream, threePath_edges_cover and threePath_edges_disjoint show the left and right edge sets partition the path; threePath_interface identifies the interface as the singleton middle vertex ${2}$; subImbalance_threePathLeft_two evaluates the left imbalance there as $+1$. Together they feed threePath_diamond_defect, which kernel-computes defect $2$ via diamondDefect_eq_neg_two_inner (middle vertex carries $m_A=1$, $m_B=-1$). That witness is the path-scale counterpart of the A15 seed diamond and anchors the rank/consistency test on J-diamonds after the census-inversion route was ruled out.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.