Theorem 2.20 (proof): unique solution of the Moser equation (2.1)–(2.2)

Proved

GrayStability.moser_equation_unique_solution

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

contact-geometrydifferential-geometrysymplectic-geometry

Let $M=F^{-1}(0)\subset\mathbb{R}^n$ be a compact regular level, $y\in M$ , $\alpha$ a contact form at $y$ , and $\beta\in(\mathbb{R}^n)^*$ any covector. Then there is exactly one $X\in\xi_y=T_yM\cap\ker\alpha_y$ for which some $\mu\in\mathbb{R}$ satisfies

\beta(v)+d\alpha_y(X,v)=\mu\,\alpha_y(v)\qquad\text{for all } v\in T_yM.

With $\beta=\dot\alpha_t$ this is equation (2.1), $\dot\alpha_t+i_{X_t}d\alpha_t=\mu_t\alpha_t$ ; evaluating at the Reeb vector forces $\mu=\beta(R)$ , which is (2.2). The unique pointwise solution is the vector field whose flow is the Gray isotopy.

Preamble

import Definitions.Def_GrayStability_Basic

Formal statement

namespace GrayStability

/-- Geiges, proof of Theorem 2.20, equations (2.1)–(2.2): at a point where `α` is a
contact form, for every covector `β` there is a unique `X ∈ ξ_y` solving
`β + i_X dα = μ α` on `T_y M` for some `μ ∈ ℝ`. -/
theorem moser_equation_unique_solution {n c : ℕ} (F : E n → (Fin c → ℝ))
    (hF : IsCompactRegularLevel F) (α : OneForm n) (y : E n) (hy : y ∈ levelSet F)
    (hα : IsContactFormAt F α y) (β : E n →L[ℝ] ℝ) :
    ∃! X : E n, X ∈ contactPlane F α y ∧ ∃ μ : ℝ,
      ∀ v ∈ tangentSpace F y, β v + extDerivOneForm α y X v = μ * α 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, proof of Theorem 2.20, equations (2.1) and (2.2), p. 15

Read-back

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

Data and hypotheses. Let $n, c \in \mathbb{N}$ be arbitrary and let $F : \mathbb{R}^n \to \mathbb{R}^c$ ( $\mathbb{R}^n$ with the sup norm) satisfy:

$F$ is $C^\infty$ on $\mathbb{R}^n$ , its zero set $F^{-1}(0)$ is compact, and $DF(y') : \mathbb{R}^n \to \mathbb{R}^c$ is surjective at every $y' \in F^{-1}(0)$ .

Let $\alpha : \mathbb{R}^n \to (\mathbb{R}^n)^*$ , $y \mapsto \alpha_y$ , be an arbitrary map (no continuity or differentiability assumed). Let $y \in \mathbb{R}^n$ with $F(y) = 0$ . Write $T_y = \ker DF(y)$ , $\xi_y = \{ v \in T_y : \alpha_y(v) = 0 \}$ , and

d\alpha_y(u,v) = \big(D\alpha(y)\,u\big)(v) - \big(D\alpha(y)\,v\big)(u),

where $D\alpha(y)$ is the Fréchet derivative of $y \mapsto \alpha_y$ at $y$ , taken to be $0$ if $\alpha$ is not differentiable at $y$ . Assume $\alpha$ is a contact form at $y$ : (i) $\alpha_y(v) \neq 0$ for some $v \in T_y$ , and (ii) for every nonzero $u \in \xi_y$ there is $v \in \xi_y$ with $d\alpha_y(u,v) \neq 0$ . Finally let $\beta \in (\mathbb{R}^n)^*$ be an arbitrary continuous linear functional on all of $\mathbb{R}^n$ (only its values on $T_y$ enter the conclusion).

Conclusion. There exists exactly one vector $X \in \mathbb{R}^n$ such that

$X \in \xi_y$ (i.e. $DF(y)X = 0$ and $\alpha_y(X) = 0$ ), and
there exists a real number $\mu$ with

\beta(v) + d\alpha_y(X, v) = \mu\, \alpha_y(v) \qquad \text{for all } v \in T_y .

Uniqueness is asserted for $X$ only; $\mu$ is existentially quantified inside the property and no uniqueness of $\mu$ is stated. The vector $X$ sits in the first slot of $d\alpha_y$ .

Edge cases and remarks.

Only the single point $y$ enters the hypotheses on $\alpha$ ; compactness of $F^{-1}(0)$ and regularity at other points are assumed but do not appear in the conclusion.
As in the contact condition generally: $c \le n$ , $\dim T_y = n - c \ge 1$ (by (i)), so $c = 0$ makes the hypotheses unsatisfiable; (ii) forces $\dim \xi_y = n - c - 1$ even.
If $\alpha$ is not differentiable at $y$ , then $d\alpha_y \equiv 0$ and (ii) forces $\xi_y = \{0\}$ , so the only candidate is $X = 0$ and the condition reduces to $\beta|_{T_y}$ being a multiple of $\alpha_y|_{T_y}$ .
$\beta = 0$ is allowed.

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