Definition 2.5: existence and uniqueness of the Reeb vector

Proved

GrayStability.reeb_vector_exists_unique

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$ , and let $\alpha$ be a one-form that is a contact form at $y$ . Then there is exactly one vector $R\in T_yM$ with

\alpha_y(R)=1\qquad\text{and}\qquad d\alpha_y(R,v)=0\ \text{ for all } v\in T_yM.

$R$ is the Reeb vector of $\alpha$ at $y$ . It exists because $d\alpha_y|_{T_yM}$ is a skew form of maximal rank on an odd-dimensional space, so its kernel is a line, and the contact condition makes $\alpha$ non-zero on that line.

Preamble

import Definitions.Def_GrayStability_Basic

Formal statement

namespace GrayStability

/-- Geiges, Definition 2.5 and the paragraph after it: at a point of `M` where `α` is
a contact form there is a unique Reeb vector `R ∈ T_y M`, `α(R) = 1`,
`dα(R, ·) = 0` on `T_y M`. -/
theorem reeb_vector_exists_unique {n c : ℕ} (F : E n → (Fin c → ℝ))
    (hF : IsCompactRegularLevel F) (α : OneForm n) (y : E n) (hy : y ∈ levelSet F)
    (hα : IsContactFormAt F α y) :
    ∃! R : E n, R ∈ tangentSpace F y ∧ α y R = 1 ∧
      ∀ v ∈ tangentSpace F y, extDerivOneForm α y R v = 0 := by sorry

end GrayStability

Source

Geiges, Contact geometry, Handbook of Differential Geometry Vol. II (2006) 315-382, https://arxiv.org/abs/math/0307242, Definition 2.5 and the paragraph after it, p. 6

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$ , meaning: (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$ .

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

R \in T_y, \qquad \alpha_y(R) = 1, \qquad d\alpha_y(R, v) = 0 \ \text{ for all } v \in T_y .

Uniqueness is among all $R \in \mathbb{R}^n$ satisfying these three conditions together.

Edge cases and remarks.

Only the single point $y$ enters the hypotheses on $\alpha$ ; compactness of $F^{-1}(0)$ and regularity at other points of the level set are assumed but do not appear in the conclusion.
$y \in F^{-1}(0)$ with surjective $DF(y)$ forces $c \le n$ and $\dim T_y = n - c$ . Condition (i) forces $T_y \neq \{0\}$ , so $n - c \ge 1$ ; in particular $c = 0$ (which forces $n = 0$ by compactness) makes the hypotheses unsatisfiable. Condition (ii), with $d\alpha_y$ alternating, forces $\dim \xi_y = n - c - 1$ to be even.
If $\alpha$ is not differentiable at $y$ , then $d\alpha_y \equiv 0$ , and condition (ii) holds only when $\xi_y = \{0\}$ (i.e. $n - c = 1$ ); the third condition in the conclusion is then automatic.

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