ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedaudited 2026-09-22

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.

Complex K-AHSS for real projective space

Example

Assume AC. For $m \geq 0$ , ${\tilde{K}}^{0} ({R P}^{2 m}) ≅ Z / 2^{m}, K^{1} ({R P}^{2 m}) = 0,$ and ${\tilde{K}}^{0} ({R P}^{2 m + 1}) ≅ Z / 2^{m}, K^{1} ({R P}^{2 m + 1}) ≅ Z .$ For $m \geq 2$ , the repeated $Z / 2$ graded pieces of the collapsed page form a nonsplit extension; for $m = 0$ there is no torsion piece, and for $m = 1$ there is a single $Z / 2$ piece and hence no nontrivial additive extension.

Facts & Assumptions

[A1]

Assume AC. The $K$ -AHSS of ${R P}^{r}$ has $E_{2}^{p, q} = H^{p} ({R P}^{r}; Z)$ for even $q$ and zero for odd $q$ , with all differentials zero (every target lies in an odd degree below $r$ or in the top degree with a torsion source, and the $0$ -column survives by the rank of its edge); the integral cohomology is $Z$ in degree $0$ , $Z / 2$ in the even positive degrees below $r$ , zero in the odd degrees below $r$ , and $Z$ in degree $r$ for odd $r$ , $Z / 2$ for even $r$ (Complex K-theory AHSS, the standard universal-coefficient computation).

[A2]

Assume AC. The complexified tautological line $ξ$ has $α = [ξ] - 1$ with $α^{2} = - 2 α$ , exact order $2^{m}$ , and ${\tilde{K}}^{0} ({R P}^{r}) = Z α$ ; the odd groups are $K^{1} ({R P}^{2 m}) = 0$ and $K^{1} ({R P}^{2 m + 1}) ≅ Z$ (The complexified tautological line resolves real-projective K-theory extensions).

[A3]

Collapse alone determines only the associated graded; the cyclic structure is genuine extension data (AHSS collapse generally determines only the associated graded object, Multiplicative AHSS for a multiplicative generalized theory).

Verification

technique · direct

Given: Assume AC, $m \geq 0$ , and the $K$ -AHSS of ${R P}^{r}$ for $r = 2 m$ or $r = 2 m + 1$ .

1.1

By [A1] the stable page has one $Z / 2$ in each even cohomological degree $2, 4, \dots$ up to the dimension and, for odd $r$ , an extra $Z$ in the top degree; all differentials vanish, so these are the graded pieces of $K^{*} ({R P}^{r})$ .

2.1

The graded pieces in total degree zero are $m$ copies of $Z / 2$ together with the $Z$ from degree zero; the associated graded of ${\tilde{K}}^{0}$ is therefore $(Z / 2)^{m}$ of order $2^{m}$ .

A1step 1.1

3.1

By [A2] the class $α$ has exact order $2^{m}$ and generates ${\tilde{K}}^{0} ({R P}^{r})$ , so the $m$ copies of $Z / 2$ assemble into the single cyclic group $Z / 2^{m}$ . For $m \geq 2$ this is a nonsplit extension because $(Z / 2)^{m}$ is not cyclic; for $m = 0$ the reduced group is zero, and for $m = 1$ it is the lone graded piece $Z / 2$ . The odd-degree statement is the corresponding clause of [A2].

A2A3step 2.1

4.1

Steps 1.1, 2.1 and 3.1 verify the displayed groups and identify exactly when a nonsplit extension occurs.

step 1.1step 3.1∎

Source notes

Compare Ji, §3.2.3, printed pp. 10–11, for the vanishing of the differentials and the warning that the spectral sequence alone does not determine the torsion group.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

15 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

Caleb Ji, The Atiyah–Hirzebruch Spectral Sequence, §3.2.3, printed pp. 10–11 (standard reference, not scraped)