TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-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.

Adem relations for Steenrod squares

Statement

Assume AC. Let $a, b$ be positive integers with $0 < a < 2 b$ . For every space $X$ , every $q \geq 0$ , and every $x \in H^{q} (X; F_{2})$ ,

$S q^{a} S q^{b} (x) = \sum_{j = 0}^{⌊ a / 2 ⌋} (\binom{b - j - 1}{a - 2 j}) S q^{a + b - j} S q^{j} (x) .$

The binomial coefficients are reduced modulo two. A binomial coefficient is zero when its lower index is negative or exceeds its nonnegative upper index, and a Steenrod square with an index outside its defining nonnegative range is zero.

Facts & Assumptions

Given: AC, positive integers $a, b$ with $0 < a < 2 b$ , a space $X$ , a nonnegative degree $q$ , and a class $x \in H^{q} (X; F_{2})$ .

[F1]

In each degree $2^{s} - 1 + b$ with $2^{s} > a$ , the finite-cellular cyclic squares satisfy the displayed Adem formula (Adem double-power comparison).

[F2]

On a finite oriented regular cell complex, a cohomology isomorphism from singular to cellular cohomology intertwines every singular square with the finite-cellular cyclic square (Finite-cellular cyclic squares agree with singular cup-i squares).

[F3]

Under AC, a natural singular-cohomology identity that is zero on all finite regular cell complexes is zero on every space (Natural singular-cohomology identities are detected on finite regular complexes).

[F4]

Singular Steenrod squares obey the external Cartan formula (Cartan formula for Steenrod squares).

[F5]

They satisfy $S q^{0} = id$ , instability, and $S q^{n} z = z ⌣ z$ for a degree- $n$ class (Steenrod normalization, instability, suspension, and top square).

[F6]

Every square is additive and natural, with its outside-range values zero (Steenrod squares are well-defined and natural).

[F7]

Under AC, external product is a cohomology isomorphism over a PID when one factor has finite-free homology in every degree (Cohomological Kunneth cross product is a ring isomorphism).

[F8]

Cellular homology is naturally isomorphic to singular homology for every CW complex and coefficient group (Cellular homology computes singular homology).

[F9]

AC supplies a choice function for every family of nonempty sets (The Axiom of Choice).

Proof

Proof technique: transfer the high-degree cellular calculation to singular squares, descend degrees by external product with the circle generator, and then detect the resulting natural identity on finite regular complexes.

1.1

Define the residual operation in input degree $r$ .

givenF6

$R_{r} (u) = S q^{a} S q^{b} (u) + \sum_{j = 0}^{⌊ a / 2 ⌋} (\binom{b - j - 1}{a - 2 j}) S q^{a + b - j} S q^{j} (u) .$

Addition is subtraction over $F_{2}$ . By [F6], for fixed $r$ this is a natural map $H^{r} (-; F_{2}) \to H^{r + a + b} (-; F_{2})$ . All its sums are finite, and every operation appearing in it has a nonnegative index.

1.2

Compute the circle class used for descent. [F2, F8] Regard $S^{1}$ as the boundary of a triangle, with vertices $v_{0}, v_{1}, v_{2}$ and edges $e_{01}, e_{12}, e_{02}$ . Over $F_{2}$ its cellular boundary is

\partial e_{i j} = v_{i} + v_{j} .

Hence $\ker (\partial : C_{1} \to C_{0})$ is generated by $e_{01} + e_{12} + e_{02}$ , the image has dimension two, and there are no cells above degree one. Thus cellular homology is $F_{2}$ in degrees zero and one and zero otherwise. By [F8], the same is true of singular homology, so all the singular homology groups of this $S^{1}$ are finite free.

The dual cellular coboundary sends a vertex function $(λ_{0}, λ_{1}, λ_{2})$ to $(λ_{0} + λ_{1}, λ_{1} + λ_{2}, λ_{0} + λ_{2})$ . Its image is the plane of edge functions whose three values sum to zero. Consequently the edge function taking value one on $e_{01}$ and zero on the other two edges represents the unique nonzero $\overset{ˉ}{v} \in H_{c e l l}^{1} (S^{1}; F_{2})$ . By [F2], there is a unique nonzero $v \in H_{s i n g}^{1} (S^{1}; F_{2})$ with $ι^{*} v = \overset{ˉ}{v}$ , and $H^{d} (S^{1}; F_{2}) = 0$ for $d > 1$ .

2.1

Establish the residual identity in unbounded finite degrees. [F1, F2, step 1.1] Fix $s$ with $2^{s} > a$ , put $r_{s} = 2^{s} - 1 + b$ , let $K$ be a finite oriented regular cell complex, and let $u \in H_{s i n g}^{r_{s}} (K; F_{2})$ . Write $ι^{*}$ for the isomorphism of [F2]. Applying it successively to each square in step 1.1 gives

ι^{*} R_{r_{s}} (u) = R_{r_{s}}^{c y c} (ι^{*} u) .

The right side is zero by [F1]. Since $ι^{*}$ is injective, $R_{r_{s}} (u) = 0$ . Thus $R_{r_{s}} = 0$ on every finite regular complex for every $s$ with $2^{s} > a$ .

2.2

Show that square compositions preserve the circle factor. [F4, F5, step 1.2] For a finite regular complex $K$ , a class $u \in H^{d} (K; F_{2})$ , and $k \geq 0$ , external Cartan gives

S q^{k} (u \times v) = \sum_{i + j = k} S q^{i} (u) \times S q^{j} (v) .

Here $S q^{0} (v) = v$ . The top-square formula and step 1.2 give $S q^{1} (v) = v ⌣ v = 0$ in $H^{2} (S^{1}; F_{2})$ , and instability gives $S q^{j} (v) = 0$ for $j > 1$ . Therefore

S q^{k} (u \times v) = S q^{k} (u) \times v .

Applying this equality twice covers every two-square composition occurring in $R$ . Linearity then yields

R_{d + 1} (u \times v) = R_{d} (u) \times v .

3.1

Descend the identity by one degree. [F7, step 1.2, step 2.2] Suppose $r \geq 1$ and $R_{r} = 0$ on every finite regular complex. The product of two finite regular cell complexes is finite regular, so for every such $K$ and every $u \in H^{r - 1} (K; F_{2})$ ,

0 = R_{r} (u \times v) = R_{r - 1} (u) \times v .

Apply [F7] over the PID $F_{2}$ . Its finite-free hypothesis holds for the circle by step 1.2, so external product identifies the last class with $R_{r - 1} (u) \otimes v$ . Tensoring an $F_{2}$ -vector space with the nonzero vector $v$ is injective on the first factor. Hence $R_{r - 1} (u) = 0$ , proving the one-degree descent.

4.1

Prove the finite-regular identity in every degree. [step 2.1, step 3.1] Given $q \geq 0$ , choose the least $s$ with both $2^{s} > a$ and $2^{s} - 1 + b \geq q$ . Step 2.1 gives the identity in degree $r_{s} = 2^{s} - 1 + b$ . Apply step 3.1 exactly $r_{s} - q$ times. This proves $R_{q} = 0$ on every finite regular complex. The construction works separately for each $q$ and uses no limit or simultaneous choice.

5.1

Extend from finite regular complexes to every space. [F3, F6, step 1.1, step 4.1] For the fixed input degree $q$ , step 1.1 and [F6] make $R_{q}$ a natural singular-cohomology operation, and step 4.1 makes it zero on every finite regular complex. The detection theorem [F3] therefore gives $R_{q} = 0$ on every space. Expanding its definition is exactly the formula in the statement.

6.1

Empty-space and zero-class inputs give zero, while both finite-sum endpoint indices remain included. [F1, F2, F3, F5, F6, F7, F9, step 1.1, step 1.2, step 2.1, step 2.2, step 3.1, step 4.1, step 5.1] The empty space and the zero class give zero on both sides by additivity. On a point, all positive-degree input groups vanish, while in degree zero the instability clauses in [F5] make every term zero because $a, b > 0$ . The endpoints $j = 0$ and $j = ⌊ a / 2 ⌋$ are retained. The strict inequality $a < 2 b$ makes every upper binomial index $b - j - 1$ nonnegative; the stated convention handles every oversized lower index. The values $S q^{0} = id$ used at $j = 0$ and on the circle are explicit, and all above-degree or negative-index squares have the conventions stated in [F5] and [F6]. Ordinary singular cohomology, including degenerate singular simplices, is used in [F2], [F3], and [F6], so no normalized-chain identification is hidden. The theorem is an equality, not a biconditional.

AC from [F9] is used exactly through four suppliers: [F1]'s cyclic and wreath carrier comparisons and the field duality used to identify the cyclic basis on its finite regular $Q_{N}$ ; [F2]'s carrier fillings and complements in the cellular-to-singular mapping cone; [F3]'s complement used to make cohomology evaluation injective; and [F7]'s additive Kunneth bijectivity. The triangle calculation, each product, the least integer $s$ , and the finite sequence of descents are explicitly prescribed and require no further choice. ∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

44 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

N. E. Steenrod and D. B. A. Epstein, Cohomology Operations (standard reference, not scraped)