diamondDefect_eq_zero_of_inter_empty
plain-language theorem explainer
When two subcomplexes partition the edges of a bounded complex and share no vertices, the four-term J-diamond defect is exactly zero. Anyone checking that disjoint union preserves inclusion-exclusion for the recognition cost cites this. The proof rewrites through the interface-coupling identity, then collapses an empty Finset sum.
Claim. Let $K$ be a bounded complex and let $A$, $B$ be subcomplexes of $K$ whose edge sets partition the edges of $K$ (union is everything, pairwise disjoint) and whose vertex sets satisfy $A_V \cap B_V = \emptyset$. Then the diamond defect $D(A,B;K)$ equals $0$.
background
This module treats Gap 2 / C15: the rank and consistency test on J-diamonds after the census-inversion route was ruled out. A subcomplex of a bounded posting complex is an edge subset together with a vertex subset closed under endpoints. A J-diamond is a pair of proper subcomplexes whose union recovers $K$; the diamond defect is the four-term inclusion-exclusion failure
$$D(A,B;I)=SJ(A)+SJ(B)-SJ(I)-SJ(K),$$
with $SJ=2\kappa J$ the integer squared-imbalance total. Valuations have $D=0$ on every diamond; $J$ is not a valuation, so defects are nonzero in general.
The parent localization identity states that, for an edge partition, the defect factors as an interface coupling: $D=-2\sum_{v\in A_V\cap B_V} m_A(v)m_B(v)$. The present lemma is the empty-interface corollary of that factorization: with no shared vertices the sum is vacant and gluing is exact.
proof idea
One-line term proof. Rewrite the defect by the localization identity diamondDefect_eq_neg_two_inner (under the edge-cover and edge-disjoint hypotheses), substitute the empty vertex intersection, reduce the sum over the empty Finset to zero, and finish with mul_zero. No case split and no induction.
why it matters
This is the first listed consequence of the localization theorem in the module narrative: disjoint union never fails inclusion-exclusion for $J$. It is recorded as the empty_interface_exact field of the package verdict jDiamondRankVerdict, alongside the full interface-coupling identity and the balanced-interface vanishing lemma. Downstream it discharges the disjoint two-edge control (twoEdge_diamond_defect, defect $0$ by the empty-interface corollary) and is re-exported as a hostile-probe corollary. Framework-wise it is the finite, posting-graph form of the panel Euler-gauge claim that gluing asymmetry of $J$ has nowhere to live when the interface is empty; the defect domicile is only the shared ledger-imbalance strata.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.