ExampleConstruction: Literature-sourcedVerification: Literature-sourcedprecheck pass

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.

Extending a visible isotopy of an unknotted circle in $R^{3}$

Example

Assume ${A C}_{ω}$ . Let $S^{1} \subseteq R^{2} \times {0} \subseteq R^{3}$ be the unit circle with inclusion map $f_{0}$ , and let $f_{1} : S^{1} \to R^{3}$ be a round circle of radius $λ > 0$ centred at $c \in R^{3}$ , written as the affine image $f_{1} (x) = c + λ Q f_{0} (x)$ of $f_{0}$ for some $Q \in S O (3)$ . Then there is a compactly supported ambient isotopy $H$ of $R^{3}$ with $H_{0} = i d$ and $H_{1} \circ f_{0} = f_{1}$ : every round circle is carried to every other by an ambient isotopy supported in any prescribed open neighbourhood of the entire isotopy image $F (S^{1} \times I)$ constructed below. The example exhibits the hypothesis check of The isotopy extension theorem in the simplest case ( $M = S^{1}$ compact, $N = R^{3}$ without boundary, no boundary stratum, no properness issue) and shows that the visible motion of a round circle is always realisable ambiently.

Facts & Assumptions

Given: The unit circle $S^{1}$ with inclusion $f_{0}$ , a round circle $f_{1} = c + λ Q f_{0}$ with $λ > 0$ , $c \in R^{3}$ and $Q \in S O (3)$ , and a prescribed open neighbourhood $W$ of the entire image of the affine isotopy $F$ constructed below.

[F1]

An ordered orthonormal pair in $R^{3}$ is completed to an element of $S O (3)$ by its cross product. Step 1.1 constructs a smooth path of rotations using a fixed axis; mere topological path connectedness is not used as a smooth-path theorem.

[F2]

A smooth isotopy of embeddings is a smooth map whose slices are smooth embeddings; an ambient isotopy of $R^{3}$ is a smooth family of diffeomorphisms with $H_{0} = i d$ , and it is compactly supported when it fixes a compact set's complement (Smooth isotopies, diffeotopies and ambient isotopies, Smooth embeddings).

[L1]

Under ${A C}_{ω}$ every smooth isotopy of a compact manifold into $R^{3}$ extends to an ambient isotopy supported in any prescribed neighbourhood of the track (The isotopy extension theorem, clause 4). [F2]

[L2]

A proper injective immersion is a smooth embedding (A proper injective immersion is a smooth embedding); $S^{1}$ is compact (Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right).

[A1]

Countable choice is inherited from [L1]; the explicit affine family below selects nothing (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Verification

technique · direct

1.1F2A1constructalgebra

An orthogonal $3 \times 3$ matrix $Q$ of determinant one has a unit fixed axis $a$ : its eigenvalues have modulus one, the nonreal ones occur in conjugate pairs, and their product together with the real eigenvalues is one, so one real eigenvalue is $+ 1$ . On $a^{⊥}$ its restriction is a plane rotation through some angle $θ$ . Fix an orthonormal basis of that plane and let $Q_{t}$ fix $a$ and rotate the plane through $t θ$ ; its sine and cosine entries give a smooth path with $Q_{0} = I$ , $Q_{1} = Q$ . Define $F_{t} (x) = t c + ((1 - t) + t λ) Q_{t} f_{0} (x)$ . Each slice is the restriction of an invertible affine map because $(1 - t) + t λ > 0$ , hence is an embedding. The family is smooth and satisfies $F_{0} = f_{0}$ , $F_{1} = f_{1}$ .

2.1F1L1L2step 1.1construct

By compactness of $S^{1}$ , [L1] extends $F$ to an ambient isotopy supported in a compact subset of $W$ , with $H_{1} \circ f_{0} = f_{1}$ . Every affine parametrization of a round circle has the form $c + λ (u \cos s + v \sin s)$ for an ordered orthonormal pair $u, v$ ; completing it by $u \times v$ gives a matrix in $S O (3)$ , including when the circle parameter orientation is reversed. Thus the construction covers all such round circles. The neighbourhood must contain the whole motion, since a disconnected neighbourhood of disjoint endpoint circles cannot support a motion between its components.

3.1step 1.1step 2.1∎

Steps 1.1 and 2.1 exhibit the required compactly supported ambient isotopy carrying $f_{0}$ to $f_{1}$ , verifying the hypothesis check of The isotopy extension theorem in this example.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

45 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.

Extending a visible isotopy of an unknotted circle in R3R3