blockSum_threePath
plain-language theorem explainer
On the three-edge path complex (vertices 0–3), the sum of the recognition cost J over all four vertices equals 1/κ for any nonzero scale κ. Gravity and ledger-cost workers cite this as the exact total cost of the path witness. The proof expands the Fin-4 sum, substitutes the four decided imbalances (−1,0,0,1), and finishes by field arithmetic.
Claim. Let $\kappa\in\mathbb{R}$ with $\kappa\neq 0$, and let $K$ be the three-edge path complex on four vertices. Then $\sum_{v\in V(K)} J_\kappa(K;v)=1/\kappa$, where $J_\kappa$ is the per-vertex recognition cost built from squared ledger imbalance scaled by $\kappa$.
background
Gap 2 (C15) studies the J-diamond rank lattice after the census-inversion route failed: the recognition cost $J$ built from vertex-level ledger imbalance is not a valuation and its moment vector lies outside the census span. The successor test is rank and consistency of J-diamonds, the four-term inclusion-exclusion defects of $J$ on overlapping subcomplexes.
A bounded complex here is a finite posting graph with vertex, edge, and triangle counts. The three-path complex is the path $0\to 1\to 2\to 3$ with four vertices and three edges. Vertex imbalance on that complex is decided: $m(0)=-1$, $m(1)=0$, $m(2)=0$, $m(3)=1$. The cost $J_\kappa$ is the local contribution of squared imbalance at scale $\kappa$ (equivalently $SJ=2\kappa J$ is the integer squared-imbalance total). Summing $J_\kappa$ over the left injection of vertices is the block (history) cost of the whole complex.
proof idea
Rewrite the sum as ranging over Fin 4 (since nV=4). Expand with Fin.sum_univ_four. Simplify each term via jCost_inl together with the four imbalance lemmas imbalance_threePath_zero through imbalance_threePath_three (values $-1,0,0,1$). After push_cast, field_simp and norm_num reduce the two nonzero squared contributions to $1/\kappa$.
why it matters
This is the exact total $J$-cost of the three-path witness used throughout the diamond-rank development. The sole immediate consumer is historyCost_threePath, which rewrites history cost through this block sum and obtains the same $1/\kappa$. That value matches the A15 seed-diamond scale (defect $1/\kappa$ on the two-edge glue), so the path sits at the same cost quantum as the smallest nonzero diamond. In the Gap-2 program it supplies a concrete, fully decided ledger total against which diamond defects and rank tests can be compared, without census inversion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.