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 real projective space

Example

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

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

where the binomial coefficient is reduced modulo two. If $a_{n}$ is the named degree-one class on ${R P}^{n}$ , the finite-dimensional formula is

$S q^{i} (a_{n}^{j}) = (\binom{j}{i}) a_{n}^{j + i} in F_{2} [a_{n}] / (a_{n}^{n + 1}) .$

Thus the right side vanishes when $i > j$ or $j + i > n$ .

Facts & Assumptions

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

[F1]

Under AC, Mod-two cohomology ring of infinite real projective space gives the polynomial ring on $a$ . For $n \geq 1$ , restriction to ${R P}^{n}$ preserves the degree-one generator; for $n = 0$ it sends $a$ to zero.

[F2]

Total Steenrod square defines $S q (x) = \sum_{r = 0}^{\deg x} S q^{r} (x)$ on a homogeneous class, a finite sum.

[F3]

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

[F4]

Cartan formula for Steenrod squares gives $S q^{k} (x y) = \sum_{r + s = k} S q^{r} (x) S q^{s} (y)$ , with only finitely many nonzero terms.

[F5]

Real projective space cellular homology and the pinch map constructs ${R P}^{n}$ with one cell in every degree from zero through $n$ , and its integral cellular boundary coefficients are zero or two. Axiomatic cellular boundaries are integral incidence matrices with coefficients says that this integral incidence matrix acts on arbitrary coefficients. Cellular homology computes singular homology compares the resulting mod-two cellular homology with singular homology, and, under AC, Cohomology over a field is dual to homology over that field computes the corresponding singular cohomology.

[F6]

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

[F7]

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

[A1]

The Axiom of Choice is assumed exactly through the ring supplier in [F1] and field duality in [F5]. Reducing the finite cellular boundary and the binomial calculation make no further choices.

Verification

technique · total Cartan followed by a finite binomial expansion

1.1

The total square of the degree-one generator is $S q (a) = a + a^{2}$ . [F2, F3] Indeed, $S q^{0} (a) = a$ , the top square is $S q^{1} (a) = a^{2}$ , and instability removes every higher component.

2.1

The total square is multiplicative on the powers of $a$ . [F2, F4, step 1.1] All component sums are finite, so summing [F4] over $k$ gives

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

Induction on the finite integer $j$ , beginning with $S q (1) = 1$ , therefore gives $S q (a^{j}) = S q (a)^{j}$ .

3.1

The infinite-dimensional formula follows by coefficient comparison. [F1, step 1.1, step 2.1] The ordinary binomial theorem over $F_{2}$ gives

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

The homogeneous component of degree $j + i$ on the left is $S q^{i} (a^{j})$ . The component on the right is $(\binom{j}{i}) a^{j + i}$ when $0 \leq i \leq j$ , and is zero when $i > j$ , which agrees with the usual zero convention for that binomial coefficient.

4.1

Restriction gives exactly the truncated finite formula. [F1, F5, F6, F7, step 3.1] Reduction modulo two turns every boundary coefficient in [F5] into zero. Thus cellular comparison and field duality give one copy of $F_{2}$ in cohomological degrees $0, \dots, n$ and zero above degree $n$ . By [F1] and [F7], the restrictions $a_{n}^{k} = i_{n}^{*} (a^{k})$ are nonzero for $0 \leq k \leq n$ . Consequently these powers form every nonzero graded piece and

$H^{*} ({R P}^{n}; F_{2}) = F_{2} [a_{n}] / (a_{n}^{n + 1}) .$

Naturality [F6]--[F7] and [F1] give

$S q^{i} (a_{n}^{j}) = S q^{i} (i_{n}^{*} a^{j}) = i_{n}^{*} S q^{i} (a^{j}) = (\binom{j}{i}) a_{n}^{j + i} .$

The quotient in [F5] makes this zero when $j + i > n$ . If $j > n$ , both sides are already zero: the input power vanishes, while $j + i > n$ for every $i \geq 0$ .

5.1

The endpoint and choice conventions agree with the formulas. [F1, F2, F3, F5, F6, A1, step 1.1, step 2.1, step 3.1, step 4.1] For $j = 0$ , the formula says $S q^{0} (1) = 1$ and all positive squares of the unit vanish. For $i = 0$ it says $S q^{0} (a^{j}) = a^{j}$ ; for $i = j$ it is the top-square identity $S q^{j} (a^{j}) = a^{2 j}$ ; and for $i > j$ it is instability. The case $n = 0$ is the point: $a_{0} = 0$ and only its zeroth power survives. Projective spaces are nonempty, zero classes map to zero, and degenerate singular simplices are already included in the natural operations of [F6]. AC is used only by the two ring suppliers [F1] and [F5]; every sum and induction here is finite. The formula is an equality, not either direction of a biconditional. ∎

Depends on

Used by

Steenrod squares do not all lift integrally Counterexample

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

Hatcher, Algebraic Topology (standard reference, not scraped)