Formalising the h-Principle and Sphere Eversion
Patrick Massot, Floris van Doorn, Oliver Nash
cs.LO
Oct 14, 2022 · v1
TL;DR
Formalizes the local h-principle and Smale's sphere eversion theorem in Lean using convex integration.
Abstract
In differential topology and geometry, the h-principle is a property enjoyed by certain construction problems. Roughly speaking, it states that the only obstructions to the existence of a solution come from algebraic topology. We describe a formalisation in Lean of the local h-principle for first-order, open, ample partial differential relations. This is a significant result in differential topology, originally proven by Gromov in 1973 as part of his sweeping effort which greatly generalised many previous flexibility results in topology and geometry. In particular it reproves Smale's celebrated sphere eversion theorem, a visually striking and counter-intuitive construction. Our formalisation uses Theillière's implementation of convex integration from 2018. This paper is the first part of the sphere eversion project, aiming to formalise the global version of the h-principle for open and ample first order differential relations, for maps between smooth manifolds. Our current local version for vector spaces is the main ingredient of this proof, and is sufficient to prove the titular corollary of the project. From a broader perspective, the goal of this project is to show that one can formalise advanced mathematics with a strongly geometric flavour and not only algebraically-flavoured mathematics.
Problem
The h-principle and sphere eversion theorem are landmark results in differential topology that had never been formalized in a proof assistant, and it was unclear whether strongly geometric mathematics (as opposed to algebraically-flavored results) could be formalized.
Approach
The authors formalize in Lean the local h-principle for first-order, open, ample partial differential relations, following Theilliere's 2018 implementation of convex integration. This local version for vector spaces is the main ingredient for the global version needed for sphere eversion. The formalization demonstrates that advanced geometric mathematics can be handled in Lean's dependent type theory.
Results
The local h-principle is fully formalized, which is sufficient to prove sphere eversion as a corollary. This represents the first formalization of a significant result in differential topology with a strongly geometric character.
