From $\log 2$ to $\pi \mathrm{/}2$: the sharp asymptotic inradius of polynomial lemniscates

Let $R_n$ be the infimum of the inradii of $\{z:\mathrm{\mid }p(z)\mathrm{\mid }<1\}$ over monic degree-$n$ polynomials whose zeros lie in the closed unit disk. We prove $n{R}_n\to \pi \mathrm{/}2$, matching the asymptotic obstruction supplied by $z^n-1$. We first establish the exact universal radius $2^{1\mathrm{/}n}-1$ for disks centered at zeros, which recovers the $(\log 2)\mathrm{/}n$ bound. Small inradius then forces radial concentration of the zeros and decay of their low reciprocal moments. These estimates give an entire limit with a modulus reflection identity; a second rescaling produces an exponential tangent and strict sublevel disks of every radius below $\pi \mathrm{/}2$. The proof is accompanied by a Lean~4 formalization and a step-by-step source index.