A starting point for a coefficient problem: the Taylor coefficients \(a_2,\dots,a_5\) of the \(\mathcal{S}^*(\varphi)\) member as explicit polynomials in the Schur parameters \(\gamma_0,\gamma_1,\dots\) (\(|\gamma_k|\le 1\)), with \(\varphi\)'s own Taylor coefficients. Plug these into your functional to get a polynomial on a box - exactly the reduction the prover certifies. Generated symbolically offline; rendered here in your browser.