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.
Refuted: the figure-eight and the round circle are regularly homotopic as oriented immersions
Statement refuted
False claim: any two oriented immersed circles in the plane are regularly homotopic; in particular the Gerono lemniscate and the round circle, despite both being images of a single parametrised circle, represent the same regular homotopy class.
The claim fails because the regular homotopy invariant of oriented immersed circles is the rotation number, which is not changed by bending, translating or self-crossing moves but jumps between the two curves in question.
Facts & Assumptions
Given: The Gerono lemniscate and the round circle , both with the positive orientation of .
The rotation number of an oriented immersed circle is the degree of its unit tangent map, equal to the winding number of the velocity about the origin. Rotation number of an immersed oriented circle in the plane, The degree of a based circle loop
A smooth plane curve is an immersion exactly when its velocity is nowhere zero. Immersions, submersions, and constant-rank maps
Degree is a function on based circle-loop homotopy classes, so endpoint-fixed homotopic based loops have equal degree. Degree defines a function
Counterexample
has velocity , whose squared norm never vanishes: if then . It is therefore an immersion. If , equality of cosines gives or modulo . In the latter case ; the only distinct pair is , both mapping to . Thus the origin is its unique double point. The round circle is an injective immersion with unit-speed velocity.
The velocity of is with . The map never vanishes, and contracts the velocity loop to through nonzero vectors. Hence . The unit tangent of is , a rotation of the identity circle map and of degree .
Any smooth homotopy through immersions has continuous nonzero velocity , so its normalized velocity is a continuous homotopy of circle maps. In complex notation , , is a based circle loop, and is a homotopy fixing both endpoints at . By [F1] its degree is , since the target rotation used to base it does not change degree. By [F3] these degrees agree at the two ends. As step 1.2 gives , no such regular homotopy joins to , refuting the false claim without a choice hypothesis or the sufficiency direction of classification.
The obstruction also distinguishes maps with the same image: is an immersion with the round circle as its image and no transverse self-intersection, yet its unit tangent has degree . The invariance argument of step 2.1 therefore separates it from as well. Thus neither the image nor its number of transverse self-intersections determines the regular homotopy class; rotation number separates the figure-eight from the round circle.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
18 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
- Hassler Whitney, On regular closed curves in the plane, Compositio Mathematica 4 (1937), pp. 276–284 (standard reference, not scraped)
- John Francis, The h-Principle, Lecture 10: Classifying immersions of spheres, after Smale (notes by A. Beaudry) (standard reference, not scraped)