Alphabeta Math
CounterexampleConstruction: 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.

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 δ(θ)=(cos⁡θ,sin⁡2θ) and the round circle γ1(θ)=(cos⁡θ,sin⁡θ), both with the positive orientation of S1=R/2πZ.

[F1]

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

[F2]

A smooth plane curve is an immersion exactly when its velocity is nowhere zero. Immersions, submersions, and constant-rank maps

[F3]

Degree is a function on based circle-loop homotopy classes, so endpoint-fixed homotopic based loops have equal degree. Degree defines a function Deg⁡:π1(S1,[0])→Z

Counterexample

1.1F2algebra

δ(θ)=(cos⁡θ,sin⁡2θ) has velocity (−sin⁡θ,2cos⁡2θ), whose squared norm sin⁡2θ+4cos⁡22θ never vanishes: if sin⁡θ=0 then cos⁡2θ=1. It is therefore an immersion. If δ(θ)=δ(ϕ), equality of cosines gives ϕ=θ or ϕ=−θ modulo 2π. In the latter case sin⁡2θ=0; the only distinct pair is π/2,3π/2, both mapping to (0,0). Thus the origin is its unique double point. The round circle is an injective immersion with unit-speed velocity.

1.2F1constructalgebra

The velocity of δ is p(sin⁡θ) with p(u)=(−u,2−4u2). The map p never vanishes, and p((1−t)sin⁡θ) contracts the velocity loop to (0,2) through nonzero vectors. Hence rot⁡(δ)=0. The unit tangent of γ1 is (−sin⁡θ,cos⁡θ), a rotation of the identity circle map and of degree 1.

2.1F1F3step 1.2construct

Any smooth homotopy H:S1×[0,1]→R2 through immersions has continuous nonzero velocity ∂θH(θ,t), so its normalized velocity τ(θ,t) is a continuous homotopy of circle maps. In complex notation βt(u)=τ(2πu,t)/τ(0,t), 0≤u≤1, is a based circle loop, and (u,t)↦βt(u) is a homotopy fixing both endpoints at 1. By [F1] its degree is rot⁡(Ht), 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 0≠1, no such regular homotopy joins δ to γ1, refuting the false claim without a choice hypothesis or the sufficiency direction of classification.

3.1F1F2step 2.1algebra∎

The obstruction also distinguishes maps with the same image: γ2(θ)=(cos⁡2θ,sin⁡2θ) is an immersion with the round circle as its image and no transverse self-intersection, yet its unit tangent (−sin⁡2θ,cos⁡2θ) has degree 2. The invariance argument of step 2.1 therefore separates it from γ1 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