Barbier's theorem for the Reuleaux triangle and the convex four-vertex theorem in Lean 4, through support functions

We give machine-checked proofs, in Lean~4 with Mathlib, of two classical theorems on convex planecurves, both developed in one model: a curve is described by its support function h, and istraced as γₕ(θ) = (h(θ) + i\,h'(θ))\,eiθ.The first is Barbier's theorem: a curve of constant width w has perimeter π w. We prove itnot only for twice continuously differentiable support functions but for support functions that aremerely C¹, with $h'$ differentiable and h+h''≥ 0 outside a countable set and $h+h''$integrable there. This covers the Reuleauxtriangle, which we construct, show to satisfy the hypotheses, and show not to be twicecontinuously differentiable, so the smooth theorem does not reach it. For the Reuleaux triangle we also identify the perimeterwith Mathlib's length and exhibit it as a Mathlib convex body of constant width. The second is the four-vertex theorem forovals given by C³ support functions with $h+h''>0$: the curvature is constant or has at least fouralternating local extrema in a period. We tie each of our own definitions to a standard notion: the perimeter toMathlib's length (total variation) --- for smooth support functions, and separately for the Reuleauxtriangle --- via a lemma, not in Mathlib, that the length of a C¹ curveis finite and equals ∫γ'; the support function to an actual convex set, whosesupport values and widths we compute; and our curvature to the textbook formula(x'y''-y'x'')/γ'³, for a curve we prove to be simple and closed.All proofs use only Lean's three standard axioms. We know of no previous complete formal proof ofeither theorem in any proof assistant, and no formalisation of the Reuleaux triangle.