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: a homotopy that is immersive at every earlier time is a regular homotopy

Statement refuted

False claim: a smooth homotopy H:M×[0,1]→N whose slices Ht are immersions for every t<1 is a regular homotopy, so it may be used to conclude that H0 and H1 are regularly homotopic (in particular that the round circle is regularly homotopic to a point, or that a sphere may be eversioned by shrinking it).

The claim fails because a regular homotopy requires every slice, including the final one, to be an immersion.

Facts & Assumptions

Given: The family H:S1×[0,1]→R2, Ht(θ)=((1−t)cos⁡θ+t, (1−t)sin⁡θ).

[F1]

A regular homotopy between immersions is a smooth family whose every slice is an immersion, with prescribed immersive ends. Regular homotopy of immersions

[F2]

An immersion is a smooth map whose differential is injective at every point; equivalently, on a curve, a map with everywhere nonvanishing velocity. Immersions, submersions, and constant-rank maps

[F3]

Regular homotopy permits self-intersections but requires injective differential at every point of every slice. Regular homotopy allows self-intersections but never rank drop

[F4]

Smooth families are the adjoints of smooth maps and evaluation of a family at a parameter is continuous. Smooth families of maps and their evaluation maps

Counterexample

1.1F2

For every t<1 the slice Ht(θ)=((1−t)cos⁡θ+t,(1−t)sin⁡θ) has derivative Ht′(θ)=(−(1−t)sin⁡θ,(1−t)cos⁡θ) of norm 1−t>0, hence is an immersion with image the circle of radius 1−t centred at (t,0); at t=0 this is the standard unit circle.

1.2F2

At t=1 the slice is the constant map H1(θ)=(1,0), whose derivative vanishes identically: the differential has rank 0<1=dim⁡S1 at every point. So the family contains a rank drop at the final time and H1 is not an immersion.

2.1F1F2F3step 1.1step 1.2

Therefore H is not a regular homotopy in the sense of [F1], since a regular homotopy requires every slice to be immersive, and it cannot certify any regular-homotopy claim: in particular this shrinking family does not show that the circle is regularly homotopic to a point, because the point is not an immersion and the rotation number (here 1 at the initial slice) would have to remain constant while no rotation number is defined for the final slice. The failed conclusion is exactly the rank-drop phenomenon separated in [F3]: the final slice fails the injective-differential condition.

3.1F2F3F4step 1.2step 2.1∎

The family H is smooth in (θ,t), but its final slice is constant. Any perturbation that keeps this final slice still has zero final derivative, so it still fails to be a regular homotopy, independently of its size. Self-intersections are compatible with immersive slices; a rank drop is not.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

16 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