Alphabeta Math
LemmaStatement: Literature-sourcedProof: 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.

Polynomial clutching families stabilize to linear clutching

Statement

Assume AC and let X be compact Hausdorff. Let q(z)=a0+a1z++anzn be polynomial clutching data for a bundle EX that is invertible for z=1. After adding n identity clutching summands, it is homotopic through invertible clutching maps to a general linear family Lnq=a(x)z+b(x) on (n+1)E. The construction is continuous in x and preserves the stabilized clutching class.

Facts & Assumptions

Given: AC, a compact Hausdorff X, n0, a finite-rank complex bundle EX, and coefficient endomorphisms a0,,an such that q(z) is invertible on S1.

[F1]

Whitney sums are defined by block-direct-sum transition maps (Whitney sum, tensor, dual, Hom, and exterior-power bundles).

[F2]

A homotopy of clutching automorphisms gives, by the transition-cocycle construction, a bundle over (X×S2)×I; its endpoint restrictions are isomorphic by homotopy invariance under AC (Vector bundles are glued from transition cocycles, Homotopy invariance of vector-bundle pullback, The Axiom of Choice).

Proof

technique · direct
1.1

For n=0, take L0q=q=0z+a0 and add no summand. Suppose n1. On (n+1)E define the block endomorphism. [F1, construct] Lnq(z)=(IzI000IzI000IzIanan1a1a0). Every entry is a finite polynomial in z and the coefficient bundle maps, and only the superdiagonal entries depend on z. Thus Lnq=a(x)z+b(x) varies continuously with x.

F1construct
2.1

Starting with Lnq, add z times column 1 to column 2, then z times the new column 2 to column 3, and continue. The first n rows become the first n rows of the identity, while the final entry of the last row becomes anzn++a1z+a0=q(z). Subtract suitable coefficient multiples of the first n rows from the last row to clear its first n entries. The resulting block matrix is B(z)=diag(I,,I,q(z)).

step 1.1algebra
3.1

Each column or row operation in step 2.1 is multiplication by an elementary triangular block matrix. Replacing its off-diagonal entry c by tc, 0t1, is a path of invertible elementary matrices. Since B(z) is invertible on S1 by hypothesis, reversing the finite sequence gives a homotopy through invertible clutching maps from B to Lnq. No fiber bases are selected globally: the block operations are bundle maps, and their invertibility can be checked in any local frame.

step 2.1algebraconstruct
4.1

By [F1], B clutches [nE,I][E,q]. By [F2] and step 3.1, the corresponding stabilized bundles satisfy the following isomorphism. [F1, F2, step 3.1] [E,q][nE,I][(n+1)E,Lnq]. This is the promised stable linearization. The matrix homotopy is a finite formula; AC is used only through [F2] to identify the endpoint bundles.

F1F2step 3.1

Depends on

Used by

Dependency tree · two levels

14 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