ExampleConstruction: Literature-sourcedVerification: Literature-sourcedPipeline-generatedprecheck passjudge 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.

Steenrod squares on complex projective space mod two

Example

Assume AC, and write $H^{*} ({C P}^{\infty}; F_{2}) = F_{2} [c]$ with $∣ c ∣ = 2$ . For all integers $i, j \geq 0$ ,

$S q^{2 i} (c^{j}) = (\binom{j}{i}) c^{j + i},$

with the coefficient reduced modulo two, while $S q^{r} (c^{j}) = 0$ for every odd integer $r \geq 0$ . For the named class $c_{n}$ on ${C P}^{n}$ , the same formulas hold in $F_{2} [c_{n}] / (c_{n}^{n + 1})$ ; in particular the even formula vanishes when $i > j$ or $j + i > n$ .

Facts & Assumptions

Given: Integers $i, j, n \geq 0$ and an odd integer $r \geq 0$ , with $n$ used for the finite-dimensional assertion.

[F1]

Under AC, Mod-two cohomology rings of complex projective spaces gives the finite and infinite polynomial rings on the degree-two classes $c_{n}, c$ , makes skeletal restrictions preserve them, and makes all odd cohomology groups zero.

[F2]

Total Steenrod square defines $S q (x) = \sum_{s = 0}^{\deg x} S q^{s} (x)$ as a finite sum.

[F3]

Steenrod normalization, instability, suspension, and top square gives $S q^{0} x = x$ , $S q^{s} x = 0$ for $s > \deg x$ , and $S q^{\deg x} x = x ⌣ x$ .

[F4]

Cartan formula for Steenrod squares gives the finite component formula $S q^{k} (x y) = \sum_{s + t = k} S q^{s} (x) S q^{t} (y)$ .

[F5]

Steenrod squares commute with pullback by Steenrod squares are well-defined and natural.

[F6]

Pullback preserves products and powers by Cup product is natural, unital and associative.

[A1]

The Axiom of Choice is assumed exactly through [F1].

Verification

technique · total Cartan and comparison of homogeneous degrees

1.1

The total square of the degree-two generator is $S q (c) = c + c^{2}$ . [F1, F2, F3] Normalization gives the degree-two term $S q^{0} (c) = c$ , and the top square gives the degree-four term $S q^{2} (c) = c^{2}$ . The intermediate class $S q^{1} (c)$ lies in the zero group $H^{3} ({C P}^{\infty}; F_{2})$ from [F1], and instability removes every higher component.

2.1

The total square is multiplicative on powers of $c$ . [F2, F4, step 1.1] Summing the finite Cartan identities and regrouping their finite terms gives

$S q (x y) = \sum_{k} \sum_{s + t = k} S q^{s} (x) S q^{t} (y) = S q (x) S q (y) .$

Starting with $S q (1) = 1$ , finite induction yields $S q (c^{j}) = S q (c)^{j}$ .

3.1

Homogeneous components give both the even formula and odd vanishing. [F1, step 1.1, step 2.1] The binomial theorem gives

$S q (c^{j}) = (c + c^{2})^{j} = \sum_{q = 0}^{j} (\binom{j}{q}) c^{j + q} .$

Every term on the right has degree $2 j + 2 q$ . The degree- $2 j + 2 i$ component is therefore $(\binom{j}{i}) c^{j + i}$ , and every component of degree $2 j + r$ for odd $r$ is zero. When $i > j$ , the relevant binomial coefficient is zero, agreeing with instability since $2 i > 2 j$ .

4.1

Restriction gives the finite formulas and their truncation. [F1, F5, F6, step 3.1] For $i_{n} : {C P}^{n} ↪ {C P}^{\infty}$ , naturality gives

$S q^{s} (c_{n}^{j}) = S q^{s} (i_{n}^{*} c^{j}) = i_{n}^{*} S q^{s} (c^{j}) .$

Facts [F1] and [F6] identify all powers under this pullback. Thus step 3.1 restricts to the two claimed formulas, and the relation $c_{n}^{n + 1} = 0$ makes the even right side zero when $j + i > n$ . If $j > n$ , the input and every displayed right side already vanish.

5.1

The boundary and choice conventions are complete. [F1, F2, F3, F5, F6, A1, step 1.1, step 2.1, step 3.1, step 4.1] For $j = 0$ , only $S q^{0} (1) = 1$ survives. For $i = 0$ the formula is $S q^{0} (c^{j}) = c^{j}$ ; for $i = j$ it is the top square $S q^{2 j} (c^{j}) = c^{2 j}$ ; and $i > j$ is zero. Odd indices include $r = 1$ and are zero even before finite truncation. The point case $n = 0$ , the first truncated exponent $j + i = n + 1$ , zero inputs, and nonemptiness are explicit. Degenerate singular simplices are included in the natural operations [F5]. AC is inherited only from [F1], while every sum and induction here is finite. No biconditional or converse is asserted. ∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

29 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

Hatcher, Algebraic Topology (standard reference, not scraped)