TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6-luna)verified 2026-10-22 (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.

Normal framing classes relative to a spanning surface are classified by winding

Statement

Let $K$ be a smooth oriented knot in the oriented three-sphere, and let $F$ be a connected compact oriented smooth embedded surface with oriented boundary $K$ . Fix the standard round metric on $S^{3}$ . A normal field along $K$ assigns to every point $p \in K$ a nonzero vector in the plane orthogonal to $T_{p} K$ ; two such fields represent the same framing class when they are homotopic through nonzero normal fields. The inward unit vector tangent to $F$ along $K$ , together with the positive quarter-turn in each oriented normal plane, gives a reference frame. In this frame the relative normal field is a map $K ≅ S^{1} \to S^{1}$ , and its degree gives a bijection from framing classes to $Z$ . Adding $n$ positive full twists changes this integer by $n$ .

Statement references

The smooth oriented knot model in the three-sphere

Based circle loops are classified by integer degree

Facts & Assumptions

Given: A smooth oriented knot $K$ , a spanning surface $F$ as in the statement, and the standard orientation and metric on $S^{3}$ .

[F1]

An oriented link in $S^{3}$ is a smooth embedding of a finite disjoint union of oriented circles, with the fixed standard orientation of $S^{3}$ . (Oriented links in the three-sphere and ambient isotopy)

[F2]

The degree map from $π_{1} (R / Z, [0])$ to $(Z, +)$ is an isomorphism, and two based circle loops are homotopic exactly when they have equal degree. ( $Deg : π_{1} (R / Z, [0]) \to (Z, +)$ is an isomorphism)

Proof

1.1givenF1construct

At each point of $K$ , the inward unit vector in $T F$ perpendicular to $T K$ is a smooth nonzero normal vector. The orientation of $S^{3}$ , the orientation of $K$ , and the metric orient the normal plane; its positive quarter-turn supplies a smooth second unit vector. These vectors give an oriented orthonormal frame of the normal plane along all of $K$ .

2.1step 1.1givenconstruct

Normalize any nonzero normal field to unit length and express it in this reference frame as $(\cos 2 π θ (p), \sin 2 π θ (p))$ . This defines a map $r : K \to S^{1}$ . The frame identifies homotopies through nonzero normal fields exactly with free homotopies of these circle maps, since normalization is continuous and the frame is defined at every point.

3.1F2step 2.1givenalgebra∎

Fix a point of $K$ . Any free loop $r$ can be made based by a constant rotation of the target sending its value at that point to $1$ ; the rotation is homotopic to the identity because $S^{1}$ is path-connected. By [F2], based homotopy classes are classified by degree and every integer occurs. Undoing the constant rotations shows that free homotopy classes are also classified by degree. Therefore the winding parameter is a bijection to $Z$ , and multiplication by the degree- $n$ loop adds $n$ , giving a free transitive twist action.

Depends on

Used by

A Seifert framing has zero self-linking Theorem

Dependency tree · two levels

13 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

Mohamed Elhamdadi, Mustafa Hajij, and Kyle Istvan, Framed Knots, arXiv:1910.10257v6, §6, pp.15–17 (standard reference, not scraped)
Allen Hatcher, Algebraic Topology, Chapter 1, §1.1, Theorem 1.7 (standard reference, not scraped)