threePath_diamond_defect
plain-language theorem explainer
On the three-edge path complex, the J-diamond split into left and right edge halves has diamond defect exactly 2. The sole interface carrier is the middle vertex, with left imbalance +1 and right imbalance −1. Gap-2 / C15 auditors cite this as the path kernel witness in the discrete defect spectrum. The proof is a short rewrite through the interface-coupling identity, two decide lemmas at that vertex, and norm_num.
Claim. Let $K$ be the bounded complex given by the three-edge path $0\to 1\to 2\to 3$. Let $A$ and $B$ be the left and right edge-halves of $K$ (an edge partition of $K$). Then the diamond defect of the pair $(A,B)$ equals $2$.
background
Gap 2 / C15 studies J-diamonds: pairs of proper subcomplexes of a posting graph whose union is the whole complex $K$. The diamond defect is the four-term inclusion-exclusion failure
$$D(A,B)=SJ(A)+SJ(B)-SJ(I)-SJ(K),$$
with $SJ=2\kappa J$ the integer squared-imbalance total and $I$ the interface. A valuation would force $D=0$ on every diamond; $J$ is not a valuation (A15), so nonzero defects are expected.
The localization theorem diamondDefect_eq_neg_two_inner states that, for an edge partition of $K$, the defect collapses to interface imbalance coupling:
$$D=-2\sum_{v\in A\cap B}m_A(v),m_B(v).$$
Empty or one-sided interfaces therefore give exact gluing. The three-edge path $0\to 1\to 2\to 3$ is the next concrete kernel after the two-edge seed: left and right halves meet only at the middle vertex.
proof idea
Rewrite the defect by the localization identity, using that the left and right edge sets cover the three-path complex and are disjoint. The interface vertex set reduces to the singleton middle vertex (index 2). Substitute the two decide lemmas: left sub-imbalance at 2 equals $+1$, right sub-imbalance at 2 equals $-1$. The remaining arithmetic is $-2\cdot(1)\cdot(-1)=2$, discharged by norm_num.
why it matters
This is the path-shaped kernel witness in the J-diamond rank lattice. Downstream it is packaged into jDiamondRankVerdict, which records the Gap-2 / C15 checklist: interface coupling, localization, empty-interface exactness, even spectrum of squared imbalance, and the seed defect. Together with the two-edge seed (defect $1/\kappa$ in $J$, integer defect 1 in $SJ$), the path shows that nonzero even defects arise from a single two-sided interface vertex with opposite unit imbalances. That pattern is the discrete content of A15's claim that $J$ fails to be a valuation, and it supplies the rank data the census-inversion route could not produce after Gap2JEhrhartSpan.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.