The Steiner Deltoid as the Tangent Envelope of Wallace--Simson Lines in Isabelle/HOL

We formalize the classical Steiner deltoid construction in Isabelle/HOL using only the published Archive of Formal Proofs entry for the Wallace--Simson line. In unit-circumcircle coordinates, the deltoid has an explicit complex parametrisation. We prove its derivative formula, characterize the stationary parameters by \(m^3=abc\), and certify them as ordinary cusps using the second and third derivatives. We then prove an equality of sets between the appropriate Wallace--Simson line and the tangent line, for every parameter, including the cusp cases. The development uses complex coordinates and handles a vertex parameter by cycling to the alternate pair of feet.