A sphere contact isotopy carries the standard Hopf circle through transverse embeddings

Proved

BirkhoffGlobalSection.contact_isotopy_maps_hopf

by caleb · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

contact-geometrydynamical-systemssymplectic-geometry

Let $F_t$ be a smooth antipodally equivariant, coorientation-preserving contact isotopy of the standard three-sphere, starting at the identity and ending at $F$ . Write $H(u)=(u_1,0,-u_2,0)$ for the positive standard Hopf circle. Then its image under the endpoint map belongs to the equivariant transverse Hopf isotopy class:

F(H(S^1))\text{ admits an equivariant positive transverse isotopy from }H(S^1).

The conclusion includes joint smoothness, sphere membership, embeddedness and positive contact evaluation at every time, together with the exact final image. This supplies the passage from an ambient contact isotopy to an isotopy of the chosen binding.

Preamble

import Definitions.Def_BirkhoffGlobalSection_SphereContact
open scoped ContDiff

Formal statement

namespace BirkhoffGlobalSection

theorem contact_isotopy_maps_hopf (F : EquivariantSphereContactomorphism)
    (I : EquivariantSphereContactIsotopy F) :
    Nonempty (EquivariantTransverseHopfIsotopy
      (F.toFun '' (standardHopfCircle '' unitCircle))) := by sorry

end BirkhoffGlobalSection

Source

Direct chain-rule consequence of the definitions in Def_BirkhoffGlobalSection_SphereContact and Def_BirkhoffGlobalSection_TransverseHopf: alpha_H(u)(DH(u)Ju)=1/2 and F_t^*alpha=a_t alpha, a_t>0. Contact-isotopy convention: Min, arXiv:2207.03590v2, Section 1.1, p. 2, https://arxiv.org/pdf/2207.03590.

View graph