imbalance_fork_zero
plain-language theorem explainer
On the two-edge out-fork (source with two outgoing edges), the ledger imbalance at the source vertex is exactly -2. Gravity and J-diamond calculations that need the seed fork's squared-imbalance total cite this identity. The proof is a one-line finite decision on incidence counts.
Claim. Let $K$ be the two-edge out-fork on three vertices with edges $1 \leftarrow 0 \rightarrow 2$. The net recognition imbalance at the source vertex $0$ (in-degree minus out-degree) equals $-2$.
background
Gap 2 studies whether the recognition cost $J$, built from vertex-level ledger imbalance, can act like a valuation on posting graphs. A subcomplex is an edge subset with endpoint-closed vertices. The diamond defect is the four-term inclusion-exclusion failure of the integer squared-imbalance total on overlapping subcomplexes; localization says that defect equals $-2$ times the sum of products of the two sides' imbalances on the interface.
Vertex imbalance is the net recognition imbalance of a vertex letter: in-degree minus out-degree, read from the carrier's ordered edge incidence. The fork complex is the elementary two-edge out-fork $1 \leftarrow 0 \rightarrow 2$ (three vertices, two edges, no triangles). It is the standard seed for imbalance and $J$-cost bookkeeping before diamond rank tests.
proof idea
One-line computational proof: decide evaluates the finite incidence data of the fork. Vertex $0$ has out-degree $2$ and in-degree $0$, so imbalance is $0-2=-2$. No lemmas beyond the definitions of the fork complex and vertex imbalance are required.
why it matters
Feeds blockSum_fork, which sums the per-vertex $J$-costs on the fork and obtains $3/\kappa$. That block sum is part of the Gap 2 / C15 program: rank and consistency tests on J-diamonds after the census-inversion route was ruled out. The fork is the smallest directed witness with a nonzero source imbalance, so pinning imbalance $-2$ at the hub locks the integer side of $SJ=2\kappa J$ before interface-coupling identities (localization of diamond defect) are applied. Within RS gravity scaffolding this is bookkeeping, not a forcing-chain step, but it closes a concrete seed case the diamond lattice needs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.