LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 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.

Negative Laurent powers are cleared by Hopf-line stabilization

Statement

Assume AC. If

$f (z) = \sum_{j = - r}^{s} a_{j} z^{j}$

is Laurent-polynomial clutching data for a bundle $E$ over $X \times S^{2}$ , then $z^{r} f (z)$ is polynomial. In the fixed clutching convention this multiplication tensors the glued bundle by ${pr}_{S^{2}}^{*} γ^{r}$ . The original $K$ -class is recovered by multiplying by the inverse unit $[γ]^{- r}$ .

Facts & Assumptions

Given: AC, $r, s \geq 0$ , and normalized Laurent clutching data $f$ supplied by Uniform Laurent approximation through bundle automorphisms.

[F1]

Under the fixed convention, transition maps multiply under tensor product (Clutching construction for bundles over a suspension).

[F2]

The external product pulls the Hopf line from $S^{2}$ to $X \times S^{2}$ (External product in complex K-theory).

[F3]

For $β = [γ] - 1$ , one has $β^{2} = 0$ and hence $[γ]^{- 1} = 1 - β$ (Hopf-line calculation of K⁰(S²)).

[A1]

AC is inherited from [F2] for the reduced product convention and from [F3]; the exponent-clearing calculation itself is finite algebra.

Proof

technique · direct

1.1

Multiplication gives $z^{r} f (z) = \sum_{j = - r}^{s} a_{j} z^{j + r}$ , whose exponents range from $0$ to $r + s$ . On $∣ z ∣ = 1$ the scalar $z^{r}$ is nonzero, so $z^{r} f (z)$ remains an automorphism.

algebra

2.1

The line $γ^{r}$ has transition $z^{r}$ . By [F1] and [F2], tensoring the bundle $[E, f]$ with ${pr}_{S^{2}}^{*} γ^{r}$ multiplies its transition by $z^{r}$ . Therefore $[E, z^{r} f] = [E, f] [γ]^{r}$ in $K^{0} (X \times S^{2})$ .

F1F2A1step 1.1

3.1

By [F3], $[γ]$ is a unit with $[γ]^{- r} = (1 - β)^{r} = 1 - r β$ . Multiplying the equality in step 2.1 by this unit gives $[E, f] = [E, z^{r} f] [γ]^{- r}$ , so clearing the negative powers loses no class information. This includes $r = 0$ , when no change occurs.

F3A1step 2.1algebra∎

Depends on

Used by

Fundamental product theorem for complex K-theory Theorem

Dependency tree · two levels

21 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, proof of Theorem 2.2 (standard reference, not scraped)