A certified upper bound for the distortion of the trefoil knot

The distortion of a rectifiable closed curve $\gamma\subset\mathbb R^3$ is the supremum, over pairs of distinct points, of the ratio of the length of the shorter arc of $\gamma$ between them to their distance; the distortion $\delta(K)$ of a knot type $K$ is the infimum over all curves of type $K$. For the trefoil, the published lower bound is $\delta\ge5\pi/3$, valid for every non-trivial knot (a recent preprint claims $\delta>6.5321$), and the only upper bound we found in the literature is the value $7.16$ obtained by numerical simulation. We exhibit an explicit polygon with $192$ vertices, of knot type trefoil, whose distortion is at most $6.92$. The proof is computer-assisted: the knot type is certified by an explicit piecewise-linear path of embedded polygons starting from a polygon on a torus, and the distortion by exact rational arithmetic on every pair of edges. Two separately written verifiers are supplied.