Prove2Me

Remark 2.21(1): contact forms are not stable

Proved
GrayStability.contact_forms_not_stable

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

contact-geometrydifferential-geometrysymplectic-geometry

Let α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) on the unit sphere S3⊂R4S^3\subset\mathbb{R}^4. There is no isotopy ψt\psi_t of S3S^3, t∈[0,1]t\in[0,1], with

ψt∗αt=α0on TS3  for all t∈[0,1].\psi_t^*\alpha_t=\alpha_0\quad\text{on } TS^3\ \text{ for all } t\in[0,1].

So the conformal factor λt\lambda_t in Gray's theorem cannot be removed: stability holds for contact structures, not for contact forms. The obstruction is dynamical: such a ψt\psi_t would conjugate the Reeb flows of α0\alpha_0 (all orbits closed) and αt\alpha_t (two closed orbits for irrational tt).

Preamble
import Definitions.Def_GrayStability_HopfFamily
Formal statement
namespace GrayStability

/-- Geiges, Remark 2.21 (1): contact forms are not stable. For the family
`α_t = (x₁ dy₁ - y₁ dx₁) + (1 + t)(x₂ dy₂ - y₂ dx₂)` on `S³` there is no isotopy
`ψ_t`, `t ∈ [0, 1]`, with `ψ_t^* α_t = α_0`. -/
theorem contact_forms_not_stable :
    ¬ ∃ ψ : ℝ → E 4 → E 4, IsIsotopyOf unitSphereEquation ψ ∧
      ∀ t ∈ Set.Icc (0 : ℝ) 1, ∀ y ∈ levelSet unitSphereEquation,
        ∀ v ∈ tangentSpace unitSphereEquation y,
          pullback (ψ t) (hopfFamily t) y v = hopfFamily 0 y v := by sorry

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

Read-back: contact_forms_not_stable

Objects (all concrete; the statement has no hypotheses and no free variables). Work in R4\mathbb{R}^4 (sup norm) with coordinates y=(y0,y1,y2,y3)y = (y_0, y_1, y_2, y_3); dyidy_i denotes the ii-th coordinate functional w↦wiw \mapsto w_i.

  • F:R4→R1F : \mathbb{R}^4 \to \mathbb{R}^1, F(y)=y02+y12+y22+y32−1F(y) = y_0^2 + y_1^2 + y_2^2 + y_3^2 - 1. Its level set F−1(0)F^{-1}(0) is the Euclidean unit sphere S3={y:y02+y12+y22+y32=1}S^3 = \{ y : y_0^2 + y_1^2 + y_2^2 + y_3^2 = 1 \}, and for y∈S3y \in S^3 the tangent space is Ty=ker⁡DF(y)={v:2∑iyivi=0}=y⊥T_y = \ker DF(y) = \{ v : 2\sum_i y_i v_i = 0 \} = y^{\perp} (Euclidean orthogonal complement).
  • For t∈Rt \in \mathbb{R}, the one-form αt\alpha_t on R4\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)(w)=y0w1−y1w0+(1+t)(y2w3−y3w2)\alpha_t(y)(w) = y_0 w_1 - y_1 w_0 + (1+t)(y_2 w_3 - y_3 w_2). In particular α0(y)(w)=y0w1−y1w0+y2w3−y3w2\alpha_0(y)(w) = y_0 w_1 - y_1 w_0 + y_2 w_3 - y_3 w_2, and for t∈[0,1]t \in [0,1] the factor 1+t1+t ranges over [1,2][1,2].

Statement. There does not exist a map ψ:R×R4→R4\psi : \mathbb{R} \times \mathbb{R}^4 \to \mathbb{R}^4, (t,y)↦ψt(y)(t,y) \mapsto \psi_t(y), satisfying both of the following:

  1. ψ\psi is an isotopy of S3S^3, meaning:
    • (t,y)↦ψt(y)(t,y) \mapsto \psi_t(y) is C∞C^\infty on all of R×R4\mathbb{R} \times \mathbb{R}^4;
    • ψ0(y)=y\psi_0(y) = y for every y∈S3y \in S^3 (only on S3S^3);
    • for every t∈[0,1]t \in [0,1]: ψt\psi_t maps S3S^3 into S3S^3, is injective on S3S^3, and maps S3S^3 onto S3S^3; and for every y∈S3y \in S^3 the derivative Dψt(y)D\psi_t(y) (ambient Fréchet derivative of ψt:R4→R4\psi_t : \mathbb{R}^4 \to \mathbb{R}^4 at yy) is injective on Ty=y⊥T_y = y^\perp;
  2. for every t∈[0,1]t \in [0,1], every y∈S3y \in S^3 and every v∈y⊥v \in y^\perp,
αt(ψt(y))(Dψt(y) v)=α0(y)(v),\alpha_t\big(\psi_t(y)\big)\big(D\psi_t(y)\,v\big) = \alpha_0(y)(v),

i.e. the pullback ψt∗αt\psi_t^*\alpha_t equals α0\alpha_0 exactly (factor 11) on tangent vectors of S3S^3, for all t∈[0,1]t \in [0,1].

Equivalently: for every ψ\psi satisfying the isotopy conditions in (1), there exist some t∈[0,1]t \in [0,1], y∈S3y \in S^3 and v∈y⊥v \in y^\perp with

αt(ψt(y))(Dψt(y) v)≠α0(y)(v).\alpha_t\big(\psi_t(y)\big)\big(D\psi_t(y)\,v\big) \neq \alpha_0(y)(v).

Remarks.

  • The statement is unconditional: it contains no hypothesis or assertion that the forms αt\alpha_t are contact.
  • The negation applies to the whole conjunction "isotopy and exact pullback identity"; the statement says nothing about pullback identities up to a multiplicative factor, about equality of kernels only, about t∉[0,1]t \notin [0,1], or about points off S3S^3.
  • Within the excluded objects, ψt\psi_t for t∉[0,1]t \notin [0,1] and off S3S^3 is only required to be smooth.
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