diamondDefect_eq_zero_of_interface_balanced
plain-language theorem explainer
On a posting-graph diamond whose edges partition the complex, if every interface vertex is one-sided balanced (imbalance vanishes on at least one side), the four-term J-defect is exactly zero. Gravity and ledger-localization arguments cite this as the Euler-gauge form of interface localization. The proof rewrites via the bilinear factorization and kills the interface sum termwise.
Claim. Let $K$ be a bounded posting complex and let $A$, $B$ be subcomplexes whose edges partition the edge set of $K$. If at every vertex of the interface $A\cap B$ the restricted ledger imbalance vanishes on at least one of the two sides, then the diamond defect vanishes: $D(A,B;K)=0$.
background
Gap 2 / C15 studies J-diamonds on bounded posting complexes: unordered pairs of proper subcomplexes whose union is $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. Recognition cost $J$ is not a valuation, so $D$ need not vanish.
A subcomplex is an edge subset together with the vertex set closed under endpoints. Restricted imbalance on a side is the net in-minus-out posting count of a vertex within that edge subset. The module's main localization identity factors the defect through the interface:
$$D=-2\sum_{v\in A\cap B}m_A(v),m_B(v).$$
Empty-interface gluing is already exact. The present statement is the complementary localization: no two-sided imbalance on the interface forces $D=0$.
proof idea
One short algebraic reduction. Rewrite the goal by the bilinear localization identity diamondDefect_eq_neg_two_inner, so the claim becomes that the interface sum of products $m_A(v)m_B(v)$ is zero. For each interface vertex the hypothesis supplies a case split: either $m_A(v)=0$ or $m_B(v)=0$. In the first case zero_mul kills the product; in the second, mul_zero. Finset.sum_eq_zero assembles the pointwise vanishings, and ring finishes $D=0$.
why it matters
This is the Euler-gauge half of the localization theorem for Gap 2: gluing asymmetry of $J$ lives only where ledger imbalance is two-sided. It is packaged into jDiamondRankVerdict as the interface_localization field, alongside the bilinear factorization, empty-interface exactness, even spectrum, and the seed defect kernel. Downstream measured checks (measured_bilinear_perfect) and hostile probes (probe_balanced_iface_is_corollary) treat it as the certified corollary that a balanced interface cannot host a nonzero diamond. In the broader RS gravity stack it confirms that boundary strata are the only domicile for J-asymmetry, matching the panel Euler-gauge lemma by an independent finite posting-graph argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.