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): |\gamma_2| = |\tfrac12 a_3 - \tfrac14 a_2^2| over S*(janowski_A1_B0)

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

Theorem (sharp). If \(f(z) = z + \sum_{n \ge 2} a_n z^n \in S^*(\varphi)\), then \(|\gamma_2| = |\tfrac12 a_3 - \tfrac14 a_2^2| \le 1/4\), and the constant \(1/4\) is best possible (attained at the extremal below). Equivalently \(\max_{S^*(\varphi)} |\gamma_2| = |\tfrac12 a_3 - \tfrac14 a_2^2| = 1/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^2) — 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): \(|\gamma_2| = |\tfrac12 a_3 - \tfrac14 a_2^2| = 1/4\). Hence the bracket \([1/4,\ 1/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:

\[ \gamma_2| = |\tfrac12 a_3 - \tfrac14 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 |\gamma_2| = |\tfrac12 a_3 - \tfrac14 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}{4} - \frac{r_{0}^{2}}{4}\), \(C = 0\).

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

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