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| = |2a_2^2 - a_3| over S*(exponential)

Let \(S^*(\varphi) = \{ f \in \mathcal{A} : zf'(z)/f(z) \prec \varphi(z) \}\) with \(\varphi(z) = e^{z}\) (class key exponential).

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

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 1 distinct extremals (omega=z) — a positive-dimensional maximizer set — so an interval prover cannot certify it at fine slack. 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| = |2a_2^2 - a_3| = 5/4\). Hence the bracket \([5/4,\ 5/4 + 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| = |2a_2^2 - a_3 \;=\; 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| = |2a_2^2 - a_3| = |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{r_{0}^{2}}{2} - \frac{1}{2}\), \(C = \frac{5 r_{0}^{2}}{4}\).

The maximum is \(5/4\). 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| = |2a_2^2 - a_3| = 5/4\).

Here the maximum is not attained at an isolated point but on 1 distinct extremals (omega=z). Representative extremals: \(\omega(z) = z\). Each attains \(|A_3| = |2a_2^2 - a_3| = 5/4\). 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 exponential inv_a3 "5/4" --slack 0
Recheck: python3 -m gft.proofs recheck data/proofs/exponential__inv_a3.json