Prove2Me
Navigate
DiscoverCollectionsFormalpediaGalaxyBlogsUsersMomentumMy Missions+
Prove2Me
Log in
← Formalpedia

Remark 2.21(3): the Gray isotopy fixes points where α˙t\dot\alpha_tα˙t​ vanishes

Proved
GrayStability.gray_stability_fixing_stationary_points

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

contact-geometrydifferential-geometrysymplectic-geometry

Let M=F−1(0)⊂RnM=F^{-1}(0)\subset\mathbb{R}^nM=F−1(0)⊂Rn be a compact regular level and αt\alpha_tαt​, t∈[0,1]t\in[0,1]t∈[0,1], a smooth family of contact forms on MMM. Then there are an isotopy ψt\psi_tψt​ of MMM and smooth functions λt>0\lambda_t>0λt​>0 on MMM with ψt∗αt=λtα0\psi_t^*\alpha_t=\lambda_t\alpha_0ψt∗​αt​=λt​α0​ on TMTMTM for t∈[0,1]t\in[0,1]t∈[0,1], such that in addition every point p∈Mp\in Mp∈M with

α˙t(p)=0  on TpMfor all t∈[0,1]\dot\alpha_t(p)=0\ \text{ on } T_pM\quad\text{for all } t\in[0,1]α˙t​(p)=0  on Tp​Mfor all t∈[0,1]

satisfies ψt(p)=p\psi_t(p)=pψt​(p)=p for all t∈[0,1]t\in[0,1]t∈[0,1].

This relative version is the form used to prove neighbourhood theorems for submanifolds, where the forms already agree along the submanifold (Geiges, proof of Theorem 2.27, the neighbourhood theorem for isotropic submanifolds).

Preamble
import Definitions.Def_GrayStability_Basic

open scoped ContDiff
Formal statement
namespace GrayStability

/-- Geiges, Remark 2.21 (3): the Gray isotopy can be chosen so that every point `p ∈ M`
at which `α̇_t(p)` vanishes on `T_p M` for all `t ∈ [0, 1]` stays fixed. -/
theorem gray_stability_fixing_stationary_points {n c : ℕ} (F : E n → (Fin c → ℝ))
    (hF : IsCompactRegularLevel F) (α : ℝ → OneForm n) (hα : IsContactFamilyOn F α) :
    ∃ ψ : ℝ → E n → E n, IsIsotopyOf F ψ ∧
      (∃ lam : ℝ → E n → ℝ, ContDiff ℝ ∞ (fun p : ℝ × E n => lam p.1 p.2) ∧
        (∀ t ∈ Set.Icc (0 : ℝ) 1, ∀ y ∈ levelSet F, 0 < lam t y) ∧
        ∀ t ∈ Set.Icc (0 : ℝ) 1, ∀ y ∈ levelSet F, ∀ v ∈ tangentSpace F y,
          pullback (ψ t) (α t) y v = lam t y * α 0 y v) ∧
      ∀ p ∈ levelSet F,
        (∀ t ∈ Set.Icc (0 : ℝ) 1, ∀ v ∈ tangentSpace F p, formTimeDeriv α t p v = 0) →
        ∀ t ∈ Set.Icc (0 : ℝ) 1, ψ t p = p := 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 (3), p. 15
Read-back

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

Read-back: gray_stability_fixing_stationary_points

Statement. For all natural numbers n,cn, cn,c, every map F:Rn→RcF : \mathbb{R}^n \to \mathbb{R}^cF:Rn→Rc, and every map t↦αtt \mapsto \alpha_tt↦αt​ from R\mathbb{R}R to one-forms on Rn\mathbb{R}^nRn: if

  • (hypothesis on FFF) FFF is a compact regular level, i.e. F∈C∞F \in C^\inftyF∈C∞, M=F−1(0)M = F^{-1}(0)M=F−1(0) is compact, and DF(y)DF(y)DF(y) is surjective for all y∈My \in My∈M; and
  • (hypothesis on α\alphaα) α\alphaα is a contact family on MMM, i.e. (t,y)↦αt(y)(t,y) \mapsto \alpha_t(y)(t,y)↦αt​(y) is C∞C^\inftyC∞ on R×Rn\mathbb{R} \times \mathbb{R}^nR×Rn and αt\alpha_tαt​ is contact at yyy for all t∈[0,1]t \in [0,1]t∈[0,1] and all y∈My \in My∈M,

then there exists a map ψ:R×Rn→Rn\psi : \mathbb{R} \times \mathbb{R}^n \to \mathbb{R}^nψ:R×Rn→Rn which is an isotopy of MMM (definition below) such that both of the following hold.

(A) Conformal relation. There exists λ:R×Rn→R\lambda : \mathbb{R} \times \mathbb{R}^n \to \mathbb{R}λ:R×Rn→R, (t,y)↦λt(y)(t,y) \mapsto \lambda_t(y)(t,y)↦λt​(y), which is C∞C^\inftyC∞ on all of R×Rn\mathbb{R} \times \mathbb{R}^nR×Rn, with λt(y)>0\lambda_t(y) > 0λt​(y)>0 (strictly) for all t∈[0,1]t \in [0,1]t∈[0,1], y∈My \in My∈M, and

αt(ψt(y))(Dψt(y) v)=λt(y) α0(y)(v)for all t∈[0,1], y∈M, v∈Ty=ker⁡DF(y).\alpha_t\big(\psi_t(y)\big)\big(D\psi_t(y)\,v\big) = \lambda_t(y)\,\alpha_0(y)(v) \qquad \text{for all } t \in [0,1],\ y \in M,\ v \in T_y = \ker DF(y).αt​(ψt​(y))(Dψt​(y)v)=λt​(y)α0​(y)(v)for all t∈[0,1], y∈M, v∈Ty​=kerDF(y).

Positivity and the identity are required only on [0,1]×M[0,1] \times M[0,1]×M (the identity only for v∈Tyv \in T_yv∈Ty​); elsewhere λ\lambdaλ is only smooth. λ0=1\lambda_0 = 1λ0​=1 is not required.

(B) Fixed points. For every point p∈Mp \in Mp∈M: if

∂∂s∣s=t αs(p)(v)=0for all t∈[0,1] and all v∈Tp,\frac{\partial}{\partial s}\Big|_{s=t}\, \alpha_s(p)(v) = 0 \qquad \text{for all } t \in [0,1] \text{ and all } v \in T_p,∂s∂​​s=t​αs​(p)(v)=0for all t∈[0,1] and all v∈Tp​,

then ψt(p)=p\psi_t(p) = pψt​(p)=p for all t∈[0,1]t \in [0,1]t∈[0,1].

Remarks on (B), as written:

  • The same ψ\psiψ that witnesses (A) must satisfy (B), for all qualifying ppp simultaneously (ψ\psiψ is chosen before ppp is quantified; λ\lambdaλ plays no role in (B)).
  • The hypothesis of (B) concerns only the single point ppp (not a neighbourhood of ppp, and not dαd\alphadα or derivatives in yyy), only tangent vectors v∈Tpv \in T_pv∈Tp​, and only times t∈[0,1]t \in [0,1]t∈[0,1]. The time derivative is the ordinary two-sided derivative of the real function s↦αs(p)(v)s \mapsto \alpha_s(p)(v)s↦αs​(p)(v) on R\mathbb{R}R at s=ts = ts=t (including at t=0t = 0t=0 and t=1t = 1t=1); since α\alphaα is assumed smooth, the derivative exists and the "zero where not differentiable" convention does not come into play. Equivalently, the hypothesis says that αt(p)\alpha_t(p)αt​(p) restricted to TpT_pTp​ does not depend on t∈[0,1]t \in [0,1]t∈[0,1].
  • The conclusion of (B) is only ψt(p)=p\psi_t(p) = pψt​(p)=p for t∈[0,1]t \in [0,1]t∈[0,1]; nothing is asserted about Dψt(p)D\psi_t(p)Dψt​(p), about λt(p)\lambda_t(p)λt​(p), or about times outside [0,1][0,1][0,1].
  • If no point of MMM satisfies the hypothesis of (B), then (B) is vacuous.

Setting and unfolded definitions. Throughout, n,c∈Nn, c \in \mathbb{N}n,c∈N are arbitrary natural numbers (both may be 000), and Rn\mathbb{R}^nRn means the space of functions {0,…,n−1}→R\{0,\dots,n-1\} \to \mathbb{R}{0,…,n−1}→R with the sup norm. A one-form α\alphaα is any map Rn→(Rn)∗\mathbb{R}^n \to (\mathbb{R}^n)^*Rn→(Rn)∗, y↦αyy \mapsto \alpha_yy↦αy​ (a continuous linear functional at each point; no regularity is built in). Derivatives DDD are Fréchet derivatives of maps on the ambient space Rn\mathbb{R}^nRn (or R×Rn\mathbb{R} \times \mathbb{R}^nR×Rn), with the convention that a derivative is 000 at any point where the map is not differentiable. For F:Rn→RcF : \mathbb{R}^n \to \mathbb{R}^cF:Rn→Rc and a one-form α\alphaα:

  • Level set: M:=F−1(0)={y∈Rn:F(y)=0}M := F^{-1}(0) = \{ y \in \mathbb{R}^n : F(y) = 0 \}M:=F−1(0)={y∈Rn:F(y)=0}.

  • Compact regular level (hypothesis on FFF): FFF is C∞C^\inftyC∞ on all of Rn\mathbb{R}^nRn, MMM is compact, and for every y∈My \in My∈M the derivative DF(y):Rn→RcDF(y) : \mathbb{R}^n \to \mathbb{R}^cDF(y):Rn→Rc is surjective.

  • Tangent space: Ty:=ker⁡DF(y)={v∈Rn:DF(y) v=0}T_y := \ker DF(y) = \{ v \in \mathbb{R}^n : DF(y)\,v = 0 \}Ty​:=kerDF(y)={v∈Rn:DF(y)v=0} (defined for every yyy, used only for y∈My \in My∈M).

  • Exterior derivative: dαy(u,v):=(Dα(y) u)(v)−(Dα(y) v)(u)d\alpha_y(u,v) := \big(D\alpha(y)\,u\big)(v) - \big(D\alpha(y)\,v\big)(u)dαy​(u,v):=(Dα(y)u)(v)−(Dα(y)v)(u), where Dα(y):Rn→(Rn)∗D\alpha(y) : \mathbb{R}^n \to (\mathbb{R}^n)^*Dα(y):Rn→(Rn)∗ is the ambient derivative of y↦αyy \mapsto \alpha_yy↦αy​ (equal to 000 if α\alphaα is not differentiable at yyy).

  • Contact plane: ξy:={v∈Ty:αy(v)=0}\xi_y := \{ v \in T_y : \alpha_y(v) = 0 \}ξy​:={v∈Ty​:αy​(v)=0}.

  • Contact at yyy: (i) there exists v∈Tyv \in T_yv∈Ty​ with αy(v)≠0\alpha_y(v) \neq 0αy​(v)=0, and (ii) for every u∈ξyu \in \xi_yu∈ξy​ with u≠0u \neq 0u=0 there exists v∈ξyv \in \xi_yv∈ξy​ with dαy(u,v)≠0d\alpha_y(u,v) \neq 0dαy​(u,v)=0 (i.e. dαyd\alpha_ydαy​ restricted to ξy×ξy\xi_y \times \xi_yξy​×ξy​ is nondegenerate; condition (ii) is vacuous when ξy={0}\xi_y = \{0\}ξy​={0}). No orientation, sign, or dimension-parity condition is imposed explicitly.

  • Smooth family: a map t↦αtt \mapsto \alpha_tt↦αt​ from R\mathbb{R}R to one-forms such that (t,y)↦αt(y)∈(Rn)∗(t,y) \mapsto \alpha_t(y) \in (\mathbb{R}^n)^*(t,y)↦αt​(y)∈(Rn)∗ is C∞C^\inftyC∞ on all of R×Rn\mathbb{R} \times \mathbb{R}^nR×Rn.

  • Contact family on MMM (hypothesis on α\alphaα): α\alphaα is a smooth family, and for every t∈[0,1]t \in [0,1]t∈[0,1] and every y∈My \in My∈M, αt\alpha_tαt​ is contact at yyy in the above sense. Nothing is required of αt\alpha_tαt​ for t∉[0,1]t \notin [0,1]t∈/[0,1] beyond smoothness, nor off MMM beyond smoothness.

  • Isotopy of MMM: a map ψ:R×Rn→Rn\psi : \mathbb{R} \times \mathbb{R}^n \to \mathbb{R}^nψ:R×Rn→Rn, (t,y)↦ψt(y)(t,y) \mapsto \psi_t(y)(t,y)↦ψt​(y), such that

    1. (t,y)↦ψt(y)(t,y) \mapsto \psi_t(y)(t,y)↦ψt​(y) is C∞C^\inftyC∞ on all of R×Rn\mathbb{R} \times \mathbb{R}^nR×Rn;
    2. ψ0(y)=y\psi_0(y) = yψ0​(y)=y for every y∈My \in My∈M (only on MMM, not on all of Rn\mathbb{R}^nRn);
    3. for every t∈[0,1]t \in [0,1]t∈[0,1]: ψt\psi_tψt​ maps MMM into MMM, is injective on MMM, and maps MMM onto MMM; and for every y∈My \in My∈M, the linear map Dψt(y)D\psi_t(y)Dψt​(y) is injective on TyT_yTy​.

    Nothing is required of ψt\psi_tψt​ for t∉[0,1]t \notin [0,1]t∈/[0,1] other than smoothness, and nothing off MMM other than smoothness. The definition does not state separately that Dψt(y)D\psi_t(y)Dψt​(y) maps TyT_yTy​ into Tψt(y)T_{\psi_t(y)}Tψt​(y)​.

  • Pullback: (ψt∗αt)y(v):=αt(ψt(y))(Dψt(y) v)(\psi_t^*\alpha_t)_y(v) := \alpha_t\big(\psi_t(y)\big)\big(D\psi_t(y)\,v\big)(ψt∗​αt​)y​(v):=αt​(ψt​(y))(Dψt​(y)v), where Dψt(y)D\psi_t(y)Dψt​(y) is the ambient derivative of ψt:Rn→Rn\psi_t : \mathbb{R}^n \to \mathbb{R}^nψt​:Rn→Rn at yyy. Edge cases of the hypotheses.

  • Surjectivity of DF(y)DF(y)DF(y) at points of MMM forces dim⁡Ty=n−c\dim T_y = n - cdimTy​=n−c there; if c>nc > nc>n then MMM must be empty.

  • If M=∅M = \emptysetM=∅ (e.g. c>nc > nc>n; or n=0n = 0n=0 and c≥1c \ge 1c≥1; or FFF a nonzero constant with c≥1c \ge 1c≥1), every condition quantified over MMM is vacuous: both hypotheses reduce to smoothness of FFF and of α\alphaα, and the conclusion only asks for smooth objects with no constraint coming from MMM.

  • Contact condition (i) requires Ty≠{0}T_y \neq \{0\}Ty​={0} at each y∈My \in My∈M, so a nonempty MMM needs n−c≥1n - c \ge 1n−c≥1. For c=0c = 0c=0 the target R0\mathbb{R}^0R0 is a point, so F≡0F \equiv 0F≡0 and M=RnM = \mathbb{R}^nM=Rn; compactness forces n=0n = 0n=0, and then Ty={0}T_y = \{0\}Ty​={0} violates (i). Hence for c=0c = 0c=0 the two hypotheses cannot hold simultaneously.

  • If n−c=1n - c = 1n−c=1, then ξy={0}\xi_y = \{0\}ξy​={0} and contact condition (ii) is vacuous; "contact" then only means that αt(y)\alpha_t(y)αt​(y) does not vanish identically on TyT_yTy​.

  • The contact condition and dαd\alphadα use the ambient derivative of αt\alpha_tαt​ on Rn\mathbb{R}^nRn, evaluated at points of MMM on vectors of ξy\xi_yξy​.

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

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paperProve2Me Team
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me