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

Immersing the circle in the plane from a formal line monomorphism

Example

Assume ${A C}_{ω}$ . Give the unit circle its counterclockwise orientation and global tangent vector $τ (x) = i x$ , identifying $R^{2}$ with $C$ . A formal immersion is uniquely described by a smooth base map $f : S^{1} \to R^{2}$ and a nowhere-zero vector field $v (x) = F_{x} (τ (x)) \in R^{2}$ . Write $v = ℓ u$ with $ℓ > 0$ and $u : S^{1} \to S^{1}$ . The positive-length functions and base maps are contractible, so formal homotopy classes are classified by the degree of $u$ . The Smale–Hirsch theorem and its component corollary identify these with regular homotopy classes of parametrized immersed plane curves. The derivative of the standard inclusion has $u (x) = i x$ , of degree $+ 1$ .

Facts & Assumptions

Given: ${A C}_{ω}$ , the counterclockwise unit circle, its smooth global tangent vector $τ (x) = i x$ , and the standard inclusion.

[F1]

A formal immersion is a smooth fibrewise linear injection over a smooth base map (Formal immersion between smooth manifolds, Vector bundle maps over a smooth base map).

[L1]

Smale–Hirsch in positive codimension and the component corollary identify formal homotopy classes with regular homotopy classes (The Smale–Hirsch immersion theorem, Regular homotopy classes of immersions are formal homotopy classes).

[L2]

Based circle loops are path-homotopic exactly when their degrees agree, and every integer is the degree of a standard loop (Two based circle loops are path-homotopic if and only if they have equal degree, $\deg (ω_{n}) = n$ for every integer $n$ , The degree of a based circle loop). Here the unit circle is identified with $R / Z$ by $t \mapsto e^{2 π i t}$ .

Verification

technique · direct

1.1F1givenconstruct

Since $τ (x)$ is a basis of $T_{x} S^{1}$ , $F_{x}$ is determined by the nonzero vector $v (x) = F_{x} τ (x)$ , not just its unoriented image line. The smooth positive length $ℓ (x) = ∣ v (x) ∣$ contracts to $1$ through positive functions, while the base map contracts to the zero map in $R^{2}$ without changing $v$ in the target's standard trivialization. Thus a formal pair deforms to $(0, u)$ , where $u = v / ∣ v ∣$ is a smooth unit-vector map.

2.1L2step 1.1construct

For a map $u : S^{1} \to S^{1}$ , normalize its value at $1$ by $α (x) = u (x) \overline{u (1)}$ , a based loop. Choose one angular path from $u (1)$ to $1$ ; multiplying $u$ by this path gives a free homotopy to $α$ . A free homotopy $u_{s}$ normalizes to the based homotopy $u_{s} (x) \overline{u_{s} (1)}$ , so its degree is invariant. Conversely equal degrees give a based homotopy of the normalized maps by [L2], and the angular paths undo the normalizations. Hence free homotopy classes are exactly the integer degrees. This classification applies to smooth maps and smooth homotopies: lifting a smooth normalized map to a real angle on $[0, 1]$ , its angle is $k t + h (t)$ with $h$ smooth periodic; interpolation of periodic $h$ to zero gives a smooth homotopy to $e^{2 π i k t}$ . Smoothness of the lift follows locally from the exponential's smooth inverse on an arc.

3.1L1L2step 1.1step 2.1∎

For an immersion $f$ , the derivative direction is $u (x) = d f_{x} (τ (x)) / ∣ d f_{x} (τ (x)) ∣$ . For the standard inclusion it is $i x$ ; after normalization this is $x = e^{2 π i t}$ , of degree $+ 1$ by [L2]. The contractions in step 1.1 and the degree classification in step 2.1 identify formal homotopy classes with $Z$ ; [L1] transfers this classification to regular homotopy classes of the parametrized immersions.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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