TheoremStatement: Literature-sourcedProof: Literature-sourcedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-14

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Cup-i coboundary identity

Statement

For mod-two cochains $a \in C^{p} (X)$ and $b \in C^{q} (X)$ and every integer $i$ ,

δ (a ⌣_{i} b) = δ a ⌣_{i} b + a ⌣_{i} δ b + a ⌣_{i - 1} b + b ⌣_{i - 1} a,

where $⌣_{j} = 0$ for $j < 0$ . The same identity holds in either relative variant of the cup- $i$ product.

Facts & Assumptions

Given: A fixed natural higher-diagonal system and cochains $a, b$ of the displayed degrees.

[F1]

Cup- $i$ is evaluation of $a \otimes b$ on $D_{i}$ , and negative indices are zero (Higher cup-i products).

[F2]

The higher diagonals satisfy $d D_{i} + D_{i} d = (1 + T) D_{i - 1}$ , with $T$ interchanging the two tensor factors (Natural higher diagonal approximations).

Proof

technique · evaluate the chain identity

1.1givenF1

If $i < 0$ , every cup product in the asserted formula has negative index, so [F1] makes both sides zero. Hence assume $i \geq 0$ and evaluate the left side on a chain $c$ of degree $p + q - i + 1$ . By the cochain-coboundary convention,

$δ (a ⌣_{i} b) (c) = (a \otimes b) D_{i} (d c) .$

2.1F2step 1.1

Substitute the higher-diagonal recurrence. Over $F_{2}$ it gives

$(a \otimes b) D_{i} (d c) = (a \otimes b) d D_{i} (c) + (a \otimes b) (1 + T) D_{i - 1} (c) .$

3.1F1step 2.1∎

Expand the two terms. The tensor coboundary has no surviving signs over $F_{2}$ , so its first term is $(δ a ⌣_{i} b + a ⌣_{i} δ b) (c)$ . Since $(a \otimes b) T = b \otimes a$ , the second is $(a ⌣_{i - 1} b + b ⌣_{i - 1} a) (c)$ . This proves the identity on every chain. The carrier property keeps every term relative when either input is relative. For $i = 0$ , both negative-index terms are zero and the formula reduces to the ordinary cup-product Leibniz identity.

Depends on

Dependency tree · 2 levels

Sources

Mosher and Tangora, Cohomology Operations and Applications