forkComplex
plain-language theorem explainer
The out-fork complex is the three-vertex, two-edge posting graph with edges (0,1) and (0,2): a hub with two outgoing leaves. Gravity Gap-2 work cites it as the left half of the out-star J-diamond and as a seed for imbalance and history-cost calculations. The body is a pure structure instance: fixed counts, decide-closed bounds, and an explicit edge map.
Claim. Let $K$ be the bounded complex with $n_V=3$ vertices, $n_E=2$ edges, and $n_T=0$ tetrahedra, with edge endpoints $(0,1)$ and $(0,2)$. This is the two-edge out-fork $1 \leftarrow 0 \rightarrow 2$ inside the ambient bound $4$.
background
Gap 2 / C15 studies J-diamonds: four-term inclusion-exclusion defects of the recognition cost $J$ on overlapping subcomplexes of a posting graph. After the census-inversion route failed (no fixed kind totals, $J$ not a valuation), the module tests rank and consistency of these defects.
A subcomplex is an edge subset plus the vertices closed under endpoints. The squared-imbalance total $SJ = 2\kappa J$ yields the diamond defect $D(A,B;I) = SJ(A)+SJ(B)-SJ(I)-SJ(K)$. The localization theorem factors $D$ through interface imbalance products, so concrete small graphs are needed as witnesses.
BoundedComplex 4 packages finite vertex/edge/tet counts with endpoint maps. The out-fork is the minimal branched graph used beside the single edge and the three-edge out-star.
proof idea
Definitional instance, not a proof. Sets $n_V=3$, $n_E=2$, $n_T=0$; discharges the three bound inequalities by decide; defines edgeVerts by cases on the edge index (edge 0 maps to $(0,1)$, otherwise $(0,2)$); and takes tetVerts as the empty eliminator on Fin 0.
why it matters
This complex is the computational seed for the fork half of the Gap-2 diamond lattice. Downstream, vertex imbalances are fixed by decision (imbalance_fork_zero gives $-2$ at the hub, $+1$ at each leaf), the block sum of $jCost$ equals $3/\kappa$, and historyCost_fork records that total.
Those feed diamond_J_outStar: splitting the three-edge out-star as this fork plus one edge along the hub yields defect $-2/\kappa$, showing defects come in both signs. The same data enters blockSum_fork, the imbalance-square lemmas, and the module verdict JDiamondRankVerdict.
In the Recognition chain this is scaffolding for A15's successor test: $J$ fails to be a valuation, and the defect localizes on interface imbalance rather than on census kind totals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.