Prove2Me

The family αt\alpha_t on S3S^3 of Geiges' Remark 2.21(1)

Definition
GrayStability_HopfFamily

by Mazecto · Oct 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

contact-geometrydifferential-geometrysymplectic-geometry

On R4\mathbb{R}^4 with coordinates (x1,y1,x2,y2)(x_1,y_1,x_2,y_2), the unit sphere is S3=F−1(0)S^3=F^{-1}(0) for F(y)=∣y∣2−1F(y)=|y|^2-1, viewed as a map to R1\mathbb{R}^1. The one-parameter family of one-forms is

αt=(x1 dy1−y1 dx1)+(1+t)(x2 dy2−y2 dx2).\alpha_t=(x_1\,dy_1-y_1\,dx_1)+(1+t)(x_2\,dy_2-y_2\,dx_2).

For t≥0t\ge0 these are contact forms on S3S^3. The Reeb flow of α0\alpha_0 is the Hopf flow, all of whose orbits are closed; for irrational tt the Reeb flow of αt\alpha_t has exactly two periodic orbits.

Geiges uses this family to show that contact forms, unlike contact structures, are not stable.

Definition code
import Definitions.Def_GrayStability_Basic

/-!
# The family of contact forms of Geiges, Remark 2.21 (1)

On `S³ ⊂ ℝ⁴` with coordinates `(x₁, y₁, x₂, y₂)`:
`α_t = (x₁ dy₁ - y₁ dx₁) + (1 + t)(x₂ dy₂ - y₂ dx₂)`.
Geiges, *Contact geometry*, arXiv:math/0307242, Remark 2.21 (1), p. 15.
-/

namespace GrayStability

noncomputable section

/-- `S³ = F⁻¹(0)` for `F(y) = |y|² - 1`, as a map to `ℝ¹`. -/
def unitSphereEquation (y : E 4) : Fin 1 → ℝ := fun _ => ∑ i, y i ^ 2 - 1

/-- The coordinate covector `dxᵢ` on `ℝ⁴`. -/
def coordCovector (i : Fin 4) : E 4 →L[ℝ] ℝ :=
  ContinuousLinearMap.proj (R := ℝ) (φ := fun _ : Fin 4 => ℝ) i

/-- `α_t = (x₁ dy₁ - y₁ dx₁) + (1 + t)(x₂ dy₂ - y₂ dx₂)`, coordinates ordered
`(x₁, y₁, x₂, y₂)`. -/
def hopfFamily (t : ℝ) (y : E 4) : E 4 →L[ℝ] ℝ :=
  (y 0 • coordCovector 1 - y 1 • coordCovector 0) +
    (1 + t) • (y 2 • coordCovector 3 - y 3 • coordCovector 2)

end

end GrayStability
Source
Geiges, Contact geometry, Handbook of Differential Geometry Vol. II (2006) 315-382, https://arxiv.org/abs/math/0307242, Remark 2.21 (1), p. 15
Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

All objects live on R4\mathbb{R}^4 (sup norm), with coordinates indexed y=(y0,y1,y2,y3)y = (y_0, y_1, y_2, y_3) (indices start at 00).

Unit-sphere equation. S:R4→R1S : \mathbb{R}^4 \to \mathbb{R}^1,

S(y)=y02+y12+y22+y32−1,S(y) = y_0^2 + y_1^2 + y_2^2 + y_3^2 - 1,

viewed as a vector with one component. Its zero set is the Euclidean unit sphere {∥y∥2=1}⊂R4\{ \|y\|_2 = 1 \} \subset \mathbb{R}^4 (Euclidean, not the sup-norm sphere).

Coordinate covectors. For i∈{0,1,2,3}i \in \{0,1,2,3\}, dyi∈(R4)∗dy_i \in (\mathbb{R}^4)^* is the ii-th coordinate projection, dyi(v)=vidy_i(v) = v_i.

Hopf family. For t∈Rt \in \mathbb{R} and y∈R4y \in \mathbb{R}^4, the covector αt(y)∈(R4)∗\alpha_t(y) \in (\mathbb{R}^4)^* is

αt(y)=(y0 dy1−y1 dy0)+(1+t) (y2 dy3−y3 dy2),\alpha_t(y) = \big(y_0\, dy_1 - y_1\, dy_0\big) + (1+t)\,\big(y_2\, dy_3 - y_3\, dy_2\big),

i.e. αt(y)(v)=y0v1−y1v0+(1+t)(y2v3−y3v2)\alpha_t(y)(v) = y_0 v_1 - y_1 v_0 + (1+t)(y_2 v_3 - y_3 v_2). This is defined for every real tt (not only t∈[0,1]t \in [0,1]); at t=−1t = -1 the second bracket drops out, and at t=0t = 0 it is y0 dy1−y1 dy0+y2 dy3−y3 dy2y_0\,dy_1 - y_1\,dy_0 + y_2\,dy_3 - y_3\,dy_2. The file only defines these objects; it asserts no property of them (no smoothness, contact or level-set claim).

The file imports the basic definitions (one-forms on Rn\mathbb{R}^n, level sets, etc.) but uses only the ambient space R4\mathbb{R}^4 from them.

Human review

  • Endorsed by Shuze Chen · Oct 6, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Mazecto · Oct 6, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph