What this rests on

The certificate reduces to these classical lemmas - each checkable by hand, independently of the engine.

1. Schur parametrisation is exact

The Schur recursion maps the closed polydisc \(\overline{\mathbb D}^{m}\) exactly onto the admissible coefficient vectors \((a_2,\dots,a_{m+1})\) of the class. Ranging the Schur parameters over \(\overline{\mathbb D}^{m}\) therefore sweeps every member's coefficients — nothing admissible is missed and nothing spurious is added.

Schur 1917; Foias–Frazho; Simon, OPUC. · schur-onto-coefficient-body

2. Rotation normalisation

The functional is weight-homogeneous under \(f(z)\mapsto e^{-i\theta}f(e^{i\theta}z)\), so its maximum is attained on the rotation-normalised slice \((\gamma_0\ge 0\) real\()\). This removes one real dimension and is verifiable by hand.

Elementary weight homogeneity. · rotation-reduction

3. Sharp in closed form (single-harmonic reduction)

For the Fekete–Szegő functional the reduced problem has one free angle, and the functional is affine in it: L = A·e^{iθ} + C with A, C real. So max over θ of |L| = |A| + |C| exactly (triangle equality, attained by the right phase), and the remaining maximum over the two radii is an exact, closed-form box maximum. The certified bracket closes to a point — no slack, no second-variation needed. This is the classical Keogh–Merkes argument, mechanized.

Keogh & Merkes (1969), single-angle Schur reduction. · fekete-szego-single-harmonic

In the literature

This value over \(S^*(\varphi)\) is fixed by a published general theorem - Fekete–Szegő, \(|\gamma_2|\) and \(|A_3|\) by Ma & Minda (1994); the second Hankel determinant \(H_2(2)=(B_1/2)^2\) by Lee–Ravichandran–Supramaniam (2013). The registry re-certifies it mechanically - it is not a new result. See provenance & novelty.

closed-form engine m = 2 Schur params · closed-form proof (no box partition)

Full technical report

Sharp constant (proven exact): |a_3 - \frac{1}{4}\, a_2^2| over S*(strongly_0.5)

Let \(S^*(\varphi) = \{ f \in \mathcal{A} : zf'(z)/f(z) \prec \varphi(z) \}\) with \(\varphi(z) = \sqrt{\frac{z + 1}{1 - z}}\) (class key strongly_0.5).

Theorem (sharp). If \(f(z) = z + \sum_{n \ge 2} a_n z^n \in S^*(\varphi)\), then \(|a_3 - \frac{1}{4}\, a_2^2| \le 1/2\), and the constant \(1/2\) is best possible (attained at the extremal below). Equivalently \(\max_{S^*(\varphi)} |a_3 - \frac{1}{4}\, a_2^2| = 1/2\).

This is an exact sharp theorem, not a bracket: for the Fekete–Szegő functional the certified upper bound and the attained lower bound coincide in closed form (single-harmonic reduction below).

Status. PROVED (exact closed-form sharp theorem; numerically confirmed by dense grid scan).

Proof architecture

Exact reduction (sympy-verified): a2..a5 are polynomials in the Schwarz coefficients c1..c4 of omega; the Schur parameterization maps the closed polydisk ONTO the full coefficient body of Schwarz functions (Schur 1917; see e.g. Foias–Frazho, The Commutant Lifting Approach, Ch. 1, or Simon, OPUC Vol. 1, Thm 1.5.5 — the Schur/Geronimus parameterization), so the squared functional is an explicit polynomial P on a compact box (reduced to a single harmonic in closed form — see Sharp closure below; no box partition is used).
Rotation lemma (human-checkable): the functional is weight-homogeneous under rotation conjugation f(z) -> e^{-i t} f(e^{i t} z), so gamma_0 may be taken real in [0,1].
Closed-form sharp value (no branch-and-bound): the functional reduces to a single harmonic in the one free angle, so its maximum is computed exactly — the triangle equality in the phase, then an exact one-variable maximization (see Sharp closure below). A fine-slack interval branch-and-bound is not used, and could not be: the maximum is attained on the one-parameter family of Schwarz functions \(\gamma_0 = r_0 \in [0,1],\ \gamma_1 = e^{i\theta}\) (\(\rho = 1\)) — a positive-dimensional maximizer set — so an interval prover cannot certify it at fine slack (a fine-slack run reached 55,591,073 boxes at slack 1e-06 without closing the \(\le (1/2+\varepsilon)\) target). The closed form resolves the exact value regardless.
Independent numerical confirmation: a dense grid scan of \(|L|\) over the parameter box confirms the closed-form constant is both an upper bound and attained (tightness verified in both directions).

Attainment (explicit extremal)

Its functional value, evaluated exactly through the same symbolic reduction (30-digit certified): \(|a_3 - \frac{1}{4}\, a_2^2| = 1/2\). Hence the bracket \([1/2,\ 1/2 + 0]\) has attained lower endpoint.

Sharp closure (proven exact)

For the Fekete–Szegő functional the certified bracket closes in closed form, so no second-variation certificate is needed. With \(\gamma_0 = r_0 \in [0,1]\) real (rotation lemma) and \(\gamma_1 = \rho\, e^{i\theta}\), the Schur reduction gives a single harmonic in the one free angle:

\[ a_3 - \frac{1}{4}\, a_2^2 \;=\; A\, e^{i\theta} + C, \qquad A, C \in \mathbb{R}. \]

Hence, by the triangle inequality (sharp, attained by choosing the phase of \(e^{i\theta}\)),

\[ \max_\theta |a_3 - \frac{1}{4}\, a_2^2| = |A| + |C|, \]

and the sharp constant is the exact maximum of \(|A| + |C|\) over \(r_0, \rho \in [0,1]\). \(A\) is linear in \(\rho\) (through \(c_2\)), so the maximum is at \(\rho = 1\); the remaining one-variable maximum over \(r_0\) is computed exactly (critical points, sign-change kinks, endpoints). At \(\rho = 1\): \(A = \frac{1}{2} - \frac{r_{0}^{2}}{2}\), \(C = \frac{r_{0}^{2}}{2}\).

The maximum is \(1/2\). This is the classical Keogh–Merkes argument, mechanized: every step is exact sympy and the angular maximization is the triangle equality (no over-approximation), so the result is an honest sharp theorem \(\max |a_3 - \frac{1}{4}\, a_2^2| = 1/2\).

Here the maximum is not attained at an isolated point but on the one-parameter family of Schwarz functions \(\gamma_0 = r_0 \in [0,1],\ \gamma_1 = e^{i\theta}\) (\(\rho = 1\)). Representative extremals: \(\omega(z) = z\) and \(\omega(z) = z^2\). Each attains \(|a_3 - \frac{1}{4}\, a_2^2| = 1/2\). This positive-dimensional maximizer set is precisely what a fine-slack branch-and-bound cannot certify; the closed form proves the exact value directly.

Reproduce & raw certificate

Reproduce: python3 -m gft.proofs prove strongly_0.5 fekete_szego_mu0.25 "1/2" --slack 0
Recheck: python3 -m gft.proofs recheck data/proofs/strongly_0.5__fekete_szego_mu0.25.json