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.
We use first-party site metrics to improve navigation: page visits, internal clicks, search result counts (not search terms), and approximate active time. A random tab ID groups events for seven days; GPC/DNT turns this off. The separate visitor count uses a self-hosted pseudonymous fingerprint and also respects GPC/DNT.