Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: Literature-sourcedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)
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.

Stabilizing a framed point suspends its collapse map

Example

Assume ACω. Let p∈S1 be a single positively framed point; its Pontryagin-Thom map is the degree-+1 self-map of S1, the generator of π1(S1)≅Z (the framed-point example). Its equatorial stabilization is the same point in S2 with the prepended normal framing, whose Pontryagin-Thom map is the suspension E of the degree-+1 map, i.e. the degree-+1 self-map of S2, the generator of π2(S2)≅Z. Iterating, the stabilization of the positively framed point of Sk is the positively framed point of Sk+1 and the classes are related by the suspension isomorphisms E:πk(Sk)→πk+1(Sk+1). This verifies the stabilization-to-suspension compatibility on a nonzero class.

Facts & Assumptions

Given: A point p∈S1 with a positive framing φ of its normal bundle ν({p}⊆S1)=TpS1, and the equatorial inclusion i:S1↪S2.

[F1]

A framing of a single point of Sk is a basis of TpSk, and it is positive when that basis is positively oriented for the standard orientation; the Pontryagin-Thom map of a positively framed point is smooth with the centre as a regular value and differential sign +1, and framed cobordism classes of framed 0-manifolds are classified by the signed count (Framings of a normal bundle, the local calculation below).

[F2]

Degree is an isomorphism πr(Sr)→Z for every r≥1, sending the identity to +1; in particular the degree-+1 self-map of Sr generates πr(Sr) (Based sphere maps are classified by degree).

[F3]

Equatorial stabilization sends the class of (N,φ) to the class of the equatorial inclusion i(N) with the equatorial normal prepended to the framing, and its Pontryagin-Thom class is the suspension: PT(σ(N,φ))=E(PT(N,φ)) (Stabilized framed cobordism and the framed bordism group, Stabilizing a framed submanifold suspends its Pontryagin-Thom map).

[F4]

With the standard orientations, the outward normal of the closed northern hemisphere at a point of the equator and a positive basis of the equator, in that order, form a positive basis of the tangent space of S2; this is the boundary-orientation convention. The suspension homomorphism is determined by the sphere-prespectrum homeomorphism S1∧Sk≅Sk+1, and it sends the class of the identity of Sk to the class of the identity of Sk+1 (Suspension and sphere prespectra).

[A1]

Countable Choice ACω is inherited from the framed-cobordism, transversality and Pontryagin--Thom suppliers (The Axiom of Countable Choice (ACω)). The finite signed count itself requires no choice.

Verification

1.1A1givenalgebra

Using [A1] for the Pontryagin–Thom and regular-value degree suppliers, for a finite framed set in Sn, the centre of the collapse target has precisely that set as its regular preimage, with differential signs equal to its framing signs. The regular-value degree formula therefore gives degree equal to the signed count. Degree classifies based self-maps of Sn, and the fixed-codimension Pontryagin--Thom bijection transfers this classification to framed cobordism. A single positive point has degree +1 and its reversal degree −1.

1.2F1F2

(The framed point generates π1(S1).) By [F1] the Pontryagin-Thom map of the positively framed point (p,φ) is a smooth self-map of S1 whose differential at p has sign +1, so its degree is +1; by [F2] degree is an isomorphism π1(S1)→Z, hence the class of the framed point is the generator. A single point realizes +1 and its orientation reversal −1 in the classification of [F1].

1.3F1F2F3F4

(Its stabilization is a positively framed point.) Under equatorial stabilization the point becomes i(p)∈S2 with the framing νeq⊕φ, where νeq is the equatorial normal, by [F3]; the normal bundle of the point i(p) in S2 is all of Ti(p)S2, so this framing is a basis of Ti(p)S2. By [F4] the pair (νeq,φ) is positive for the standard orientation of S2 because φ is a positive basis of the equator, so the stabilization is again a single positively framed point. By [F1] its Pontryagin-Thom map has degree +1 and, by [F2], it generates π2(S2)≅Z.

2.1F2F3F4step 1.2step 1.3

(The suspension identity on the generator.) By [F3] the Pontryagin-Thom class of the stabilization is E of the class of the framed point, which is the generator of π1(S1) by step 1.2. By [F4] the suspension sends the class of the identity of S1 to the class of the identity of S2, and the class of the identity is the generator of π1(S1) by [F2]; hence E(PT(p,φ)) is the identity class of π2(S2), i.e. the degree-+1 self-map of S2. This agrees with step 1.3, where the Pontryagin-Thom class of the stabilization was computed directly as the generator of π2(S2): the identity PT(σ(p,φ))=E(PT(p,φ)) holds on this nonzero class.

3.1F2F3F4step 1.3step 2.1∎

(Iteration and conclusion.) Repeating the two computations one dimension higher: the stabilization of the positively framed point of Sk is the positively framed point of Sk+1 (the same boundary-orientation computation as step 1.3, where the equatorial normal is prepended to a positive basis), and its Pontryagin-Thom class is the generator of πk+1(Sk+1)≅Z; by [F3] and [F4] these classes are related by the suspension isomorphisms E:πk(Sk)→πk+1(Sk+1), which send generator to generator. The stabilized class is therefore a nonzero element of the zeroth stable stem π0s (Stable stems of the sphere), and the example verifies the stabilization-to-suspension compatibility on a nonzero class.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

62 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