pathLeft
plain-language theorem explainer
Names the left half of the two-edge path complex 0→1→2 as a subcomplex: vertices {0,1} and the single edge 0. It is the A-side of the seed J-diamond used throughout the Gap-2/C15 rank lattice. The definition is a structure instance whose endpoint-closure obligations are discharged by singleton membership.
Claim. Let $K$ be the path complex with three vertices and two edges $0\to 1\to 2$. The left path subcomplex is the pair of vertex set $\{0,1\}$ and edge set $\{0\}$, closed under endpoints of that edge.
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 of a bounded complex is a subset of edges together with a vertex subset closed under their endpoints.
The ambient object is the path complex: two edges glued at one vertex, $0\to 1\to 2$. The classical A15 witness is the diamond formed by splitting this path into its two edges. The diamond defect is $D(A,B;I)=SJ(A)+SJ(B)-SJ(I)-SJ(K)$ with $SJ=2\kappa J$; nonzero defects show $J$ is not a valuation.
This definition supplies the left leg of that seed diamond. Its right counterpart and the localization identity $D=-2\sum_{v\in A\cap B}m_A(v)m_B(v)$ are developed in the same module.
proof idea
Structure instance, not a theorem. Vertices are the Finset ${0,1}$ on $\mathrm{Fin},3$; edges are the singleton ${0}$ on $\mathrm{Fin},2$. The two closure fields tail_mem and head_mem are proved by singleton elimination: the unique edge is $0$, whose tail is $0$ (in the insert) and whose head is $1$ (in the singleton of the insert).
why it matters
This is the A-side of the seed diamond that A15 named and C15 builds. Downstream, seed_edges_cover and seed_edges_disjoint show the left and right path halves partition the edge set of the path complex; seed_diamond_defect evaluates the defect as $2$ in $1/(2\kappa)$ units (i.e. $1/\kappa$ in $J$ units); seed_diamond_localized and seed_inner_product pin the interface coupling at the shared vertex.
Those facts feed JDiamondRankVerdict, the C15 lattice package: localization, even spectrum, kernel-computed unit diamonds, rank facts, and seed-row inconsistency. In the broader RS gravity program this closes the successor test after the Ehrhart-span failure of census inversion: defects localize to interface imbalance rather than to global kind totals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.