ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-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.

Complex K-theory of even and odd spheres

Example

Assume AC. For $n \geq 1$ ,

$K^{0} (S^{2 n}) ≅ Z \oplus Z, K^{0} (S^{2 n + 1}) ≅ Z,$

and the corresponding reduced groups are $Z$ and $0$ . More generally, for $n \geq 0$ and $q \in Z$ ,

${\tilde{K}}^{q} (S^{n}) ≅ {\begin{cases} Z, & q - n is even, \\ 0, & q - n is odd . \end{cases}$

Facts & Assumptions

Given: integers $n \geq 0$ and $q$ , with $n \geq 1$ for the two unreduced degree-zero formulas, and AC.

[F1]

The reduced sphere calculation, including its all-degree parity formula, is Complex K-theory of spheres.

[F2]

The coefficient groups are $K^{2 k} (*) ≅ Z$ and $K^{2 k + 1} (*) = 0$ (K-theory of a point and the empty space).

[A1]

AC is required by [F1] and by the periodic clause of [F2].

Verification

technique · direct use of the reduced calculation and the split rank map

1.1

By [F1], ${\tilde{K}}^{0} (S^{2 n}) ≅ Z$ and ${\tilde{K}}^{0} (S^{2 n + 1}) = 0$ for every $n \geq 1$ . Since each such sphere is nonempty, connected, and based, restriction to the basepoint is split by pullback along the collapse $S^{m} \to *$ . Hence $K^{0} (S^{m}) ≅ K^{0} (*) \oplus {\tilde{K}}^{0} (S^{m})$ . Substitution of [F2] gives the two displayed unreduced groups.

F1F2A1algebra

1.2

Suspending the coefficient calculation gives ${\tilde{K}}^{q} (S^{n}) ≅ K^{q - n} (*)$ . By [F2], this group is $Z$ precisely when $q - n$ is even and is zero precisely when $q - n$ is odd, proving both exhaustive parity cases.

F1F2A1

2.1

At $n = 0$ , the based sphere $S^{0}$ is the disjoint union of the basepoint and one further point. Its reduced group is the difference between the two coefficient copies and hence is one copy of $K^{q} (*)$ , agreeing with step 1.2. This is why the unreduced formulas were stated only for $n \geq 1$ .

F2step 1.2∎

Depends on

Used by

The complex K-ring of CPⁿ Example

Dependency tree · two levels

9 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, Vector Bundles & K-Theory, §2.2 (standard reference, not scraped)
May, A Concise Course in Algebraic Topology, Chapter 24 §2 (standard reference, not scraped)