Alphabeta Math
CorollaryStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-13
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.

Each homotopy representative is supported on a finite CW subcomplex

Statement

For a CW complex X, every continuous map from a compact sphere Sn or disk Dn into X has image in a finite CW subcomplex. Every specified homotopy between such maps also has image in a finite CW subcomplex. These assertions quantify separately over each map and each homotopy; they do not assert a single finite subcomplex that works for all representatives.

If the chosen basepoint x0X is a zero-cell, every based homotopy class in πn(X,x0), n1, has a representative whose image is contained in Xn. No such based skeletal assertion is made for a basepoint outside Xn. All these conclusions are choice-free: only the finite-relative-source clause of cellular approximation is used.

Facts & Assumptions

Proof

Given: A CW complex X, one map f:SnX or f:DnX, or one specified homotopy H with one of these domains. For the based assertion, n1 and x0 is a zero-cell.

1.1

The Euclidean sphere and disk are closed and bounded, as are their products with I=[0,1], regarded as subsets of a finite-dimensional Euclidean space. Thus [F3] makes them compact. D0 is a singleton and S0 consists of two points, which are compact by taking one covering member for each of finitely many points. Their products with I are a single interval or two intervals, also closed bounded Euclidean subsets after the usual embeddings.

F3given
1.2

The sphere has a finite n-dimensional CW structure with its designated basepoint as a vertex. One concrete construction for n1 attaches one n-disk to a point by collapsing its entire boundary. To identify the quotient with Sn, send uDn of norm r>0 to (sin(πr)u/r,cos(πr)), and send zero to the north pole. This is continuous at zero since sin(πr)πr, is constant at the south pole on the boundary, and is a bijection from the interior to the complement of that pole. The induced continuous bijection from the compact quotient to the Hausdorff sphere is a homeomorphism: the quotient is compact by pulling open covers back to the disk. A closed subset is compact by [F4], its image is compact by the same cover argument, and that image in the Hausdorff sphere is closed by [F4]. Identify the pole with the designated sphere basepoint. This realizes the usual two-cell based sphere.

F3F4given
2.1

Apply [F1] directly to f, and separately to the specified H. It gives finite subcomplexes containing their images. The finite subcomplex for H automatically contains both endpoint images, since the endpoints are restrictions of H. This does not require selecting representatives of a family of homotopy classes, nor choosing simultaneous finite subcomplexes for such a family.

F1step 1.1
2.2

For a given based representative f:(Sn,)(X,x0), its restriction to the source vertex is cellular because x0X0. Apply the finite-relative-source clause of [F2] to (Sn,) and (X,{x0}). It produces a based homotopy to g that is cellular. The source has dimension n, so g(Sn)Xn. Since the homotopy fixes the basepoint, g represents precisely the original based class. This applies to each class by beginning with any one representative; it asserts existence for each class and does not select representatives simultaneously.

F2step 1.2
3.1

Each homotopy just obtained, being a specified map on Sn×I, also satisfies step 2.1. A basepoint outside Xn cannot belong to the image of a based map landing in Xn, so such a skeletal conclusion would be impossible and has not been asserted. The assertions about compact images have no basepoint restriction. Zero-dimensional compact domains were treated in step 1.1; the skeletal group assertion begins at n=1, and no π0 group law is implied. Only choice-free [F1], [F3] and the expressly choice-free clause of [F2] have been used.

step 1.1step 2.1step 2.2

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

48 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