threePathComplex
plain-language theorem explainer
Canonical three-edge path complex on four vertices with edges 0→1→2→3 and no tetrahedra. Gravity and ledger-imbalance calculations cite it as the support of a second J-diamond witness (path plus last edge glued at the middle vertex). The body is a pure structure instance: fixed counts, decide bounds, and an explicit edge map.
Claim. Let $K$ be the bounded complex with $n_V=4$ vertices, $n_E=3$ edges, and $n_T=0$ tetrahedra, with edge endpoints $(0,1)$, $(1,2)$, $(2,3)$ in that order. This is the directed three-edge path $0\to 1\to 2\to 3$.
background
Module Gap2JDiamondRank studies J-diamonds: four-term inclusion-exclusion defects of the recognition cost $J$ on overlapping subcomplexes of a posting graph. After Gap2JEhrhartSpan ruled out census inversion for the three per-kind rates, the successor test is rank and consistency of these diamonds. A subcomplex is an edge subset with endpoint-closed vertices; a diamond is a pair of proper subcomplexes whose union is $K$, and the defect is $D(A,B;I)=SJ(A)+SJ(B)-SJ(I)-SJ(K)$ with $SJ=2\kappa J$.
BoundedComplex n packages finite vertex/edge/tet counts (bounded by $n$) together with endpoint maps. Sibling imbalance and diamond-defect lemmas compute vertex ledger imbalance $m(v)$ and the localization $D=-2\sum_v m_A(v)m_B(v)$ on the interface. The seed diamond (two edges glued at one vertex) already gives defect $1/\kappa$; the three-edge path is the next elementary support used to probe the same sign and magnitude pattern.
proof idea
Definitional instance, not a proof. Sets $n_V=4$, $n_E=3$, $n_T=0$; discharges the three bound hypotheses by decide. Edges are the piecewise map sending $0\mapsto(0,1)$, $1\mapsto(1,2)$, else $(2,3)$. The empty tet family is t.elim0 on Fin 0. No upstream lemmas are applied beyond the BoundedComplex structure fields.
why it matters
Supplies the geometric carrier for the second diamond witness in the J-diamond rank lattice. Downstream, imbalance_threePath_* fix the four vertex imbalances, imbalanceSq_threePath gives total squared imbalance $2$, and blockSum_threePath / historyCost_threePath evaluate the $J$-cost sum as $1/\kappa$. The parent theorem diamond_J_threePath splits the path as front two-edge path plus last edge along the middle vertex and obtains defect $1/\kappa$ (glued $2/\kappa$, direct $1/\kappa$), same sign as the seed diamond. That feeds the A15/C15 program: $J$ is not a valuation, defects localize on interface imbalance, and the rank lattice of such defects is the route past the failed census-inversion attack on the three per-kind gravity rates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.