blockSum_twoEdge
plain-language theorem explainer
The sum of recognition costs over the four vertices of the two-edge seed complex equals 2/κ for any nonzero Casimir κ. Gravity and ledger-cost workers cite it when evaluating the history cost of the A15 witness diamond. The proof expands the four-term Fin sum, substitutes the known vertex imbalances ±1, and simplifies the resulting rational to 2/κ.
Claim. For every real Casimir $\kappa \neq 0$, the sum of recognition costs of the four vertex letters of the two-edge complex equals $2/\kappa$. Each vertex $v$ is charged $m(v)^2/(2\kappa)$ with ledger imbalances $m\in\{-1,1,-1,1\}$, so $\sum_v m(v)^2/(2\kappa)=2/\kappa$.
background
In the Gap 2 / C15 module, recognition cost is built from vertex-level ledger imbalance. A vertex letter is charged its squared imbalance over twice the Casimir κ; edge and top-cell letters carry zero charge. The two-edge complex is the A15 seed: two edges glued along one vertex, the smallest nonzero J-diamond.
Its four vertices have imbalances $-1,+1,-1,+1$ (proved by direct decision on the finite graph). The block sum aggregates those vertex costs alone; that total later feeds the history cost of the whole complex.
The module's program is the rank and consistency test on J-diamonds: four-term inclusion-exclusion defects of J on overlapping subcomplexes. The seed diamond has defect $1/\kappa$, and this block sum is the elementary vertex total that appears when history cost is evaluated on that seed.
proof idea
Rewrite the sum over Fin nV as a sum over Fin 4. Expand with Fin.sum_univ_four into four explicit terms. Unfold the vertex clause of the cost and substitute the four imbalance lemmas (values $-1,1,-1,1$). After casting integers to reals, field simplification and numeric normalization give $4/(2\kappa)=2/\kappa$. Pure algebraic reduction in term mode; no induction.
why it matters
Feeds historyCost_twoEdge, which equates the full history cost of the two-edge complex under this cost to the same $2/\kappa$. That history cost is the ledger total used when comparing accumulation orders on the A15 seed diamond (defect $1/\kappa$). The module tests whether J-diamonds span a rank lattice after census inversion failed in the Ehrhart-span predecessor. Closing the seed evaluation is a prerequisite for the localization identity that factors diamond defect through interface imbalance products, and for the claim that gluing asymmetry of J lives only where two-sided imbalance meets. Within RS gravity this is Gap 2 of the seven-gap program on recognition-cost structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.