1 Introduction

This is a formalization of an "elementary" proof of Poncelet’s closure theorem: it only involves basic algebra and group laws of elliptic curves. It is more "low level" comparing to most modern proof of the theorem, where explicit curves and maps are constructed.

1.1 The theorem statement

Given two nondegenerate plane conics Outer and Inner, if it is possible to find a \(n\)-sided polygon simultaneously inscribed in Outer and circumscribed around Inner, then it is possible to find another such polygon, one of whose vertices is an arbitrary point on Outer.

1.2 Notes

The theorem is usually considered in the real or complex projective plane, but as the arguments are purely algebraic, we will be able to formalize this in any underlying field with characteristic 0. (In fact most of the arguments work for fields with any characteristic not equal to 2, but this is not fully formalized yet)

As we are in projective plane, it is possible that the polygon will contain points at infinity or lines at infinity.

Several degenerate cases need to be considered, mainly concerning about degenerate intersection of conics (tangent). Some of these degenerate cases can be naturally included in the general case, while others needs to be discussed separately.

Even in the non-degenerate case, it is possible for a polygon to contain repeated vertices and edges. This happens when a vertex lands on a intersection of the two conics, or an edge is a shared tangent of the two conics. Algebraically, as we will define directed edges, we can distinguish between repeated edges, so this is generally not an issue. However, it can be confusing when presented geometrically.