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

The Pontryagin-Thom map of the standard framed equator

Example

Assume ACω. For m≥1 let Sm−1⊆Sm be the equator, framed by the outward unit normal of the closed northern hemisphere. The standard hemisphere sweep in Sm×I is a compact neat framed cobordism from this framed equator to the empty manifold, so the framed equator is framed null-cobordant and its Pontryagin-Thom map Sm→S1 is nullhomotopic; for m=1 the two equator points carry opposite signs and the signed count is 0. Stabilizing this fixed (m−1)-dimensional equator raises its codimension, not its dimension, and suspends its zero collapse class. When m=1, this zero-dimensional example contrasts with a single positive point, which represents +1 in π1(S1) and in the zeroth stable stem.

Facts & Assumptions

Given: An integer m≥1, the sphere Sm with its standard orientation, the equator Sm−1={x∈Sm:xm+1=0}, and the outward unit normal field νeq of the closed northern hemisphere H={x∈Sm:xm+1≥0} along its boundary.

[F1]

A framing of a closed embedded submanifold is a trivialization of its normal bundle; the normal bundle of the equator in Sm is the rank-one bundle spanned by ∂s in the height coordinate s=xm+1, and νeq trivializes it (Framings of a normal bundle).

[F2]

The Pontryagin-Thom map of a closed framed codimension-k submanifold is p∘Φφ∘c; for the empty submanifold the tube is empty, the collapse is the constant map to the basepoint and the Pontryagin-Thom map of ∅ is the constant based map (The Pontryagin-Thom map of a framed submanifold).

[F3]

Framed-cobordant closed framed submanifolds have based homotopic Pontryagin-Thom maps, the empty framed submanifold included (Framed cobordant submanifolds have homotopic Pontryagin-Thom maps, Framed cobordism of framed submanifolds).

[F4]

Framed cobordism classes of closed framed 0-manifolds of Sn are classified by the signed count, a single positively framed point realizes +1 and its orientation reversal −1, and degree is an isomorphism πn(Sn)→Z (computed below).

[F5]

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

[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.2F1F4

(The equator and its framing.) The equator is a closed embedded (m−1)-submanifold of Sm; in the height coordinate s=xm+1 its normal bundle is the rank-one bundle spanned by ∂s, and the restriction of νeq is a nonvanishing section, hence a framing. For m=1 the equator is the two-point set {(±1,0)} and νeq=(0,−1) at both points; with respect to the standard orientation of S1, whose positive tangent is (0,1) at (1,0) and (0,−1) at (−1,0), the first framing is negative and the second positive.

1.3F1F3construct

Let σ be the smooth step function and put h(t)=2t σ(8t−1). For 0≤t≤1/2, take W={(x,t)∈Sm×I:xm+1=h(t)}. Near t=0, h=0, so W is the product of the equator with time. For 1/4≤t≤1/2, h(t)=2t, and at the cap (x,t)=(em+1,1/2) the derivative h′=2 makes the defining function xm+1−h(t) a submersion. In local pole coordinates the surface is the smooth graph t=xm+1/2; it has no cap boundary. Elsewhere on W the height gradient in Sm is nonzero. Thus W is a compact neat embedded m-manifold with only the equatorial boundary at time zero and a literal product collar. The field V=(−∇Smxm+1,h′(t)) is a nonvanishing normal field: its two components cannot vanish together on W. Near time zero it is (−em+1,0), the outward normal of the northern hemisphere, with no time dependence. Trivialize the quotient normal by sending [V] to 1. This frames W and extends the equator framing throughout its end collar. Hence W is a framed null-cobordism.

2.1F2F3F4step 1.2step 1.3

(Nullhomotopy and the one-dimensional count.) By step 1.3 and [F3] the Pontryagin-Thom map of (Sm−1,νeq) is based homotopic to the Pontryagin-Thom map of the empty framed submanifold, which is the constant map by [F2]; hence the framed equator is framed null-cobordant and its Pontryagin-Thom map Sm→S1 is nullhomotopic. For m=1 this is also visible in the classification of [F4]: the two equator points carry signs −1 and +1 by step 1.2, so their signed count is 0 and their framed class is the class of the empty 0-manifold.

3.1F4F5step 2.1∎

Stabilizing this equator preserves its dimension m−1 and changes its ambient sphere from Sm to Sm+1, hence its codimension from one to two. By [F5], its collapse class suspends from the zero element of πm(S1) to zero in πm+1(S2), and remains zero under iteration. For m=1 both this equator and a single positively framed point are zero-dimensional; by [F4] their classes are 0 and +1, respectively. For m>1 a single point belongs to a different dimension and is not a generator of the equator's stable stem.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

70 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