diamondDefect
plain-language theorem explainer
Integer four-term inclusion-exclusion defect of squared ledger imbalance on a pair of subcomplexes of a posting graph: side charges minus interface charge minus full-complex charge. Gravity and Gap-2 workers cite it as the raw diamond quantity before localization. The body is a direct algebraic combination of subcomplex charges, with the interface written on the edge intersection so no disjointness is assumed.
Claim. For a bounded posting complex $K$ and subcomplexes $A,B\subseteq K$, the diamond defect is the integer $$D(A,B)=SJ(A)+SJ(B)-SJ(I)-SJ(K),$$ where $SJ(S)=\sum_{v\in S}m_S(v)^2$ is the squared-imbalance charge of $S$, $I$ is the interface (vertices and edges of $A\cap B$), and the interface term is expanded explicitly so the definition does not require $A$ and $B$ to be edge-disjoint.
background
Gap 2 / C15 studies whether the recognition cost $J$ (built from vertex-level ledger imbalance on posting graphs) can serve as a valuation on overlapping regions. A subcomplex of a bounded complex is a subset of edges together with a vertex set closed under endpoints. The integer charge of a subcomplex is the sum of squared imbalances of its vertices under its own edge set; in units of $1/(2\kappa)$ that charge is $J$.
A J-diamond is a pair of proper subcomplexes whose union recovers $K$: two accumulation orders of the same complex. The diamond defect is the four-term difference $SJ(A)+SJ(B)-SJ(I)-SJ(K)$. Valuations have vanishing defect on every diamond; $J$ is not a valuation, so defects are generically nonzero. The module imports the Ehrhart-span failure of census inversion and runs the successor rank test on these defects.
Upstream, subCharge supplies the side and interface charges; the full-complex term is the global squared-imbalance total. The interface charge is written on the edge intersection so the definition itself needs no partition hypothesis.
proof idea
Pure definition, not a theorem. The body adds the two subcomplex charges, subtracts the sum of squared imbalances of the edge-intersection restricted to the vertex intersection (the explicit interface charge), and subtracts the global imbalance square of $K$. No lemmas are applied; the four-term shape is the inclusion-exclusion defect written so overlapping edges are allowed.
why it matters
This is the raw quantity for the entire J-diamond rank lattice. The main localization theorem rewrites it as minus twice the interface inner product of the two imbalance fields, so the defect is supported only where both sides carry imbalance. Immediate corollaries: empty interface implies exact gluing; interface with no two-sided imbalance implies vanishing defect (finite Euler-gauge localization for posting graphs).
Downstream, the C15 verdict structure packages the localization identity, evenness of the spectrum, kernel-computed unit diamonds (seed defect, out-star defect $-4$), rank facts, and seed-row inconsistency. Concrete witnesses such as the out-star and seed diamonds evaluate this definition after applying the coupling identity. In the broader RS gravity chain it is the Gap-2 successor to the failed census-inversion route: defects, not kind totals, carry the obstruction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.