The Poincare-Bendixson Theorem in Isabelle/HOL
summary
Formalizes the planar Poincare–Bendixson claim in Isabelle/HOL, building on the existing Jordan curve theorem and ODE/real-analysis libraries. Key result is a monotonicity lemma encoded by constructing explicit flow regions r1 and r2 and proving they lie on opposite sides of the Jordan curve, eliminating six of eight sketchy textbook cases. A symmetric version is generated via Isabelle locales; the main lemma is about 760 lines, plus ~30 lines of boilerplate to export the reverse-time lemma.
AI-written summary · about
chapters (10)
- 0:00Start
- 0:49Background
- 7:57The Monotonously Lemma
- 8:31Proof
- 9:03Jordan Curve
- 11:15Formalization
- 14:42Symmetric Lemma
- 15:05Conclusions
- 18:35Plans To Work in Higher Dimensions
- 19:43Motivation from the Analysis of Hybrid Systems
related talks
01h 02mLogic, Optimization, and Constraint Programming: A Fruitful Collaboration
28mFormalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite Systems
01h 22mTutorial 3: Geometric Invariant Theory
30mFormalization of Differential Privacy in Isabelle/HOL
26mOn the Intersection of a Sparse Curve and a Low-degree Curve: A Polynomial Version of the Lost Theor
31mAn Isabelle Formalization of Co-rewrite Pairs for Non-reachability in Term Rewriting
24mClassical Notions of Computation and the Hasegawa-Thielecke Theorem
34mFormalizing the ∞-categorical Yoneda lemma