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.1

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$ . [given, F1] By the cochain-coboundary convention,

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

2.1

Substitute the higher-diagonal recurrence. [F2, step 1.1] 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.1

Expand the two terms. [F1, step 2.1] 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

Used by

Steenrod squares from cup-i Definition
Bockstein parity recurrence for Steenrod squares Lemma
Steenrod normalization, instability, suspension, and top square Proposition
Steenrod squares are well-defined and natural Theorem

Dependency tree · two levels

5 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Mosher and Tangora, Cohomology Operations and Applications (standard reference, not scraped)