Liouville–Arnold theorem on integrable systems

liouville_arnold

Submitter: Kim Morrison.

Notes: §45 of Knill's 'Some Fundamental Theorems in Mathematics'. On a 2n-dimensional symplectic manifold with n smooth, pointwise linearly independent, pairwise Poisson-commuting first integrals F₁, …, F_n, every compact connected component of a joint level set is diffeomorphic to the n-torus T^n. Formalized on ℝ^{2n} with the standard symplectic form ω₀ = ∑ᵢ dpᵢ ∧ dqᵢ. Mathlib has EuclideanSpace, fderiv, AddCircle, Homeomorph but no Poisson brackets, no symplectic manifolds beyond Matrix.symplecticGroup, no first integrals, and no Liouville–Arnold theorem in any form (the Liouville files in Mathlib/Analysis/Complex/ are Liouville's theorem on bounded entire functions, a different result). The Challenge ships ~1 page of helper definitions (E, idxP, idxQ, poissonBracket, IsLiouvilleIntegrable, levelSet).

Source: V. I. Arnold, *Mathematical Methods of Classical Mechanics* (2nd ed., 1989), Theorem 49.A.1 (the standard modern reference). The result is due to Liouville (1855) for the local existence of action-angle coordinates and Arnold (1963) for the compact-connected-component topology. Listed as §45 in O. Knill, *Some Fundamental Theorems in Mathematics* (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: Joint hamiltonian flows of F₁, …, F_n commute (by Poisson-commutativity) and are everywhere transverse to the level set (by linear independence of the gradients), so each compact connected component carries a transitive free action of ℝⁿ. The stabilizer is a discrete subgroup of full rank n (compactness), hence isomorphic to ℤⁿ, exhibiting M_c as ℝⁿ/ℤⁿ ≃ T^n.

theorem declaration uses `sorry`liouville_arnold {n : ℕ} (F : Fin n → LeanEval.Geometry.LiouvilleArnold.E n → ℝ) (U : Set (LeanEval.Geometry.LiouvilleArnold.E n)) (_hU : IsOpen U)
    (_hLI : LeanEval.Geometry.LiouvilleArnold.IsLiouvilleIntegrable F U)
    (c : Fin n → ℝ)
    (_hMc_sub : LeanEval.Geometry.LiouvilleArnold.levelSet F c ⊆ U)
    (_hMc_compact : IsCompact (LeanEval.Geometry.LiouvilleArnold.levelSet F c))
    (_hMc_connected : IsConnected (LeanEval.Geometry.LiouvilleArnold.levelSet F c)) :
    Nonempty ((LeanEval.Geometry.LiouvilleArnold.levelSet F c) ≃ₜ (Fin n → AddCircle (1 : ℝ))) := byn:ℕF:Fin n → E n → ℝU:Set (E n)_hU:IsOpen U_hLI:IsLiouvilleIntegrable F Uc:Fin n → ℝ_hMc_sub:levelSet F c ⊆ U_hMc_compact:IsCompact (levelSet F c)_hMc_connected:IsConnected (levelSet F c)⊢ Nonempty (↑(levelSet F c) ≃ₜ (Fin n → AddCircle 1))
  sorryAll goals completed! 🐙

Solved by

• @GanjinZero with Seed Prover (ByteDance) on Jun 1, 2026