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 formal frame homotopy behind sphere eversion

Example

Let $ι : S^{2} ↪ R^{3}$ be the standard embedding and $ι \circ a$ its antipodal version, with sections $s_{ι} = d ι$ and $s_{ι \circ a} = d (ι \circ a)$ of the Stiefel bundle $E = V (T S^{2}, ε^{3})$ . Move the two sections to a common value at a basepoint. The characteristic-disk model and boundary-map transport of the evaluation lemma then give based maps into $V_{2} (R^{3}) ≅ S O (3)$ ; their difference class has a based representative $F : S^{2} \to S O (3)$ . Since $S^{2}$ is simply connected, $F$ lifts through the quaternion double cover to $\tilde{F} : S^{2} \to S^{3}$ . A based nullhomotopy of $\tilde{F}$ projects to one of $F$ , proving that the difference class vanishes and the formal sections are homotopic.

Facts & Assumptions

Given: The unit sphere $S^{2}$ , the standard embedding $ι$ , the antipodal diffeomorphism $a (x) = - x$ , the two-sheeted covering homomorphism $ρ : S^{3} \to S O (3)$ , $ρ (q) (v) = q v q^{- 1}$ , and a trivialisation of $E = V (T S^{2}, ε^{3})$ over the two closed hemispheres.

[F1]

Moving to a common basepoint value and using characteristic-disk transport gives the based difference map $F : S^{2} \to V_{2} (R^{3}) ≅ S O (3)$ whose class in $π_{2}$ is the obstruction; the two formal framings of $ι$ and $ι \circ a$ are homotopic precisely when this class vanishes. Standard and reflected two-sphere immersions have homotopic formal data in R^3

[F2]

$ρ : S^{3} \to S O (3)$ is a two-sheeted covering map (the quaternion double cover of the rotations of $Im H$ ), so its image is all of $S O (3)$ and its fibres have two points; a covering map is a locally trivial bundle whose total space and base are path connected and locally path connected here. The quaternion double cover generates the third homotopy group of SO(3), Covering maps, evenly covered neighbourhoods, fibres, sheets, and trivial coverings

[F3]

Covering-space lifting criterion: a continuous map $Y \to B$ from a path connected, locally path connected space lifts along a covering $p : E \to B$ exactly when the induced subgroup of $π_{1}$ is contained in the image of $p_{*}$ ; for a simply connected $Y$ the condition is automatic. Lifting criterion for maps from path-connected locally path-connected spaces

[F5]

For $0 \leq k < r$ every continuous based map $S^{k} \to S^{r}$ is nullhomotopic. In particular $S^{2}$ is simply connected and $π_{2} (S^{3}) = 0$ . Lower-dimensional sphere maps are based nullhomotopic

[F6]

$S^{2}$ is path connected and simply connected (apply [F5] with sphere dimensions $1 < 2$ ), and $π_{2} (S O (3)) = π_{2} (O (3)) = 0$ . For $n \geq 2$ , the sphere $S^{n - 1}$ is path-connected and connected, The second homotopy group of SO(3) vanishes

[F7]

The formal immersion $(f, F)$ is a smooth $f$ with a bundle monomorphism over $f$ , so that $(ι, d ι)$ and $(ι \circ a, d (ι \circ a))$ are the formal data of the two embeddings; $V_{2} (R^{3})$ is the space of ordered orthonormal pairs. Formal immersion between smooth manifolds, Stiefel spaces, Grassmannians, and tautological bundles

Verification

1.1F1F7

Use [F1] to move the two sections to a common evaluated value and transport their characteristic-disk models to constant-boundary maps. The difference of their classes in $π_{2} (V_{2} (R^{3}))$ has a based representative $F : S^{2} \to V_{2} (R^{3})$ . Its class vanishes exactly when the original sections are homotopic. This construction does not identify the two raw hemisphere restrictions without their boundary transport.

2.1F6step 1.1

Completing an orthonormal pair to $(u, v, u \times v)$ identifies $V_{2} (R^{3})$ with $S O (3)$ by the cited vanishing lemma. A constant left translation makes the based representative take value $I$ at its basepoint. Denote the translated map again by $F$ .

3.1F2F3F6step 2.1

$F$ lifts along $ρ$ : $S^{2}$ is path connected and simply connected by [F6], so the lifting criterion [F3] applies with $Y = S^{2}$ , $B = S O (3)$ and the covering $p = ρ$ of [F2]: the subgroup of $π_{1} (S^{2})$ is trivial, hence contained in $ρ_{*} π_{1} (S^{3})$ , and a lift $\tilde{F} : S^{2} \to S^{3}$ with the prescribed basepoint exists.

4.1F5step 3.1

$\tilde{F}$ is nullhomotopic: every based map $S^{2} \to S^{3}$ is nullhomotopic through based maps by [F5], so the class of $\tilde{F}$ in $π_{2} (S^{3})$ is the distinguished element.

5.1F1step 2.1step 4.1

Project a based nullhomotopy $\tilde{H}$ of $\tilde{F}$ through $ρ$ . The composite $ρ \circ \tilde{H}$ contracts $F$ to $I$ and fixes the basepoint. Thus the difference class vanishes and [F1] gives a homotopy of the two formal sections.

6.1F1F5step 4.1step 5.1∎

The two possible lifts differ by the deck transformation $q \mapsto - q$ . Both are based-nullhomotopic at their respective basepoints because every based map $S^{2} \to S^{3}$ is nullhomotopic. Different disk frames and reference transports may change the representative difference map, but the evaluation lemma preserves its vanishing criterion. The calculation proves the formal obstruction is zero; it does not construct a regular homotopy of immersions.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

109 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

Ralph L. Cohen, Immersions of Manifolds and Homotopy Theory (Harvard CMSA Math-Science Literature Lecture write-up, June 30 2022), §2.1 eversion paragraph (standard reference, not scraped)
Allen Hatcher, Algebraic Topology, §1.3 (covering spaces, lifting criterion) and §4.2 (standard reference, not scraped)