The standard Hopf circle bounds a positive elliptic rational disk
ProvedBirkhoffGlobalSection.standard_hopf_elliptic_rational_diskcontact-geometrydynamical-systemssymplectic-geometry
The positive standard Hopf circle in the standard contact sphere bounds a lifted rational two-disk with exactly one positive elliptic characteristic singularity:
The disk is smooth, embedded and immersed, has positively transverse boundary, and its only antipodal coincidences are opposite boundary points. Its characteristic field has a unique zero, placed at the parameter origin, with positive scalar linearization. This supplies a concrete reference disk for comparison with geometric retrograde bindings.
Preamble
import Definitions.Def_BirkhoffGlobalSection_EllipticRationalDisk open scoped ContDiff
Formal statement
namespace BirkhoffGlobalSection
theorem standard_hopf_elliptic_rational_disk :
Nonempty (PositiveEllipticRationalDisk (standardHopfCircle '' unitCircle)) := by sorry
end BirkhoffGlobalSection
Source
Explicit stereographic hemisphere parametrization f(x,y)=(2x,1-x^2-y^2,-2y,0)/(1+x^2+y^2). Direct coordinate consequence of Def_BirkhoffGlobalSection_EllipticRationalDisk; its pullback radial contact form is 2(x dy-y dx)/(1+x^2+y^2)^2, so DW(0)=2 id. Contact sign convention: Def_BirkhoffGlobalSection_TransverseHopf.