imbalance_threePath_zero
plain-language theorem explainer
The source vertex of the directed three-edge path on four vertices has ledger imbalance −1 (indegree minus outdegree). Gap-2 / J-diamond workers cite this when evaluating the squared-imbalance total on the path witness. The proof is a one-line kernel decision on the finite incidence table of the complex.
Claim. For the directed three-edge path complex on vertices $0,1,2,3$ with edges $0\to 1\to 2\to 3$, the vertex imbalance (indegree minus outdegree) at the source vertex $0$ equals $-1$.
background
Gap 2 (C15) studies the rank and consistency of J-diamonds: four-term inclusion-exclusion defects of the recognition cost J on overlapping subcomplexes of a posting graph. The prior census-inversion route failed; this module tests whether diamond defects still organize the imbalance lattice.
A BoundedComplex carries ordered edge incidence. Vertex imbalance at v is the integer net ledger flow: indegree(v) − outdegree(v), read directly from that incidence (no extra stipulation). The squared-imbalance total SJ = 2 κ J is the integer part of the recognition cost.
The three-path complex is the minimal directed path 0 → 1 → 2 → 3 (four vertices, three edges, no triangles). It is the standard linear witness used to probe endpoint imbalance before assembling diamond defects or block sums of jCost.
proof idea
One-line proof by decide. The complex is a concrete finite object: four vertices and three directed edges. Lean evaluates indegree and outdegree of vertex 0 from the incidence table, subtracts, and checks equality with −1. No lemmas are invoked beyond the definitions of the complex and of vertex imbalance.
why it matters
Feeds blockSum_threePath, which sums jCost over the four vertices of the path and obtains 1/κ (for κ ≠ 0). That identity is the concrete evaluation step that turns endpoint imbalance into a nonzero recognition-cost total on the path witness.
In the Gap-2 program this sits after the localization theorem (diamond defect equals −2 times the interface imbalance coupling). Endpoint imbalances on paths are the elementary building blocks of those interface products; without them the diamond rank lattice has no seed data. The module aims at the A15 successor test: whether J-diamonds still yield a consistent rank structure once census inversion is abandoned.
No forcing-chain landmark (T5–T8) is settled here; the result is local gravity scaffolding for the imbalance ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.