The inscribed parabola and the Poncelet point: the complete quadrilateral and the complete quadrangle in Lean 4

We give machine-checked proofs, in Lean 4 with Mathlib, of two families of classical theorems:one about four lines and one about four points. For four lines in general position (a completequadrilateral) we prove that the reflections of the Miquel point M in the four lines lie on theline of the four orthocentres, that M is not on that line, and that the parabola with focus Mand directrix the orthocentre line is tangent to each of the four lines, with an explicit point ofcontact on each. We also prove the elementary facts about this parabola that we use to describeit: its vertex is on it, at half the focus–directrix distance from the focus, and is the point ofthe parabola closest to the directrix; its axis is perpendicular to the directrix; and the NewtonGauss line is perpendicular to the directrix, so parallel to the axis. A further file proves thatnone of the four lines is parallel to the axis, so the tangency holds in the classical sense; thatthis is the only parabola tangent to the four lines; and Lambert’s theorem for every parabolatangent to the three side lines of a triangle. For four points with no three collinear (a completequadrangle) that are not an orthocentric system, we define the Poncelet point by an explicitformula and prove that it lies on the four nine-point circles (Mathlib’s ninePointCircle), thatthree of them already meet only there, that it lies on the four pedal circles when the points arenot concyclic, and on the circumcircle of the diagonal triangle when no two opposite sides areparallel. The formula fails exactly for orthocentric quadrangles, where we prove that the fournine-point circles coincide. Outside the orthocentric case we prove the point invariant undera generating set of permutations of the four points (hence under all), and we prove that onetransposition fails in the orthocentric case under Lean’s convention x/0 = 0. The further file alsoproves the pedal-circle and diagonal-circle statements in the orthocentric case, and that everypoint on the four nine-point circles is the centre of a rectangular conic through the four points.The original main theorems are restated with Mathlib-only types and shown non-vacuous byexplicit configurations, and they were compared with blind restatements from our prose; all theclassical statements were compared with a blind restatement from the classical literature. Allproofs use only Lean’s three standard axioms. In the sources we searched we found no earlierformal proof of the full statements; the triangle form of the reflection theorem (Steiner’s line)has an earlier formal proof in Isabelle/HOL, and other ingredients come from our earlier paper.