Sharp constant (proven exact): |a_3 - \tfrac12 a_2^2| over S*(rational_kr)

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

Theorem (sharp). If \(f(z) = z + \sum_{n \ge 2} a_n z^n \in S^*(\varphi)\), then \(|a_3 - \tfrac12 a_2^2| \le -1/2 + sqrt(2)/2\), and the constant \(-1/2 + sqrt(2)/2\) is best possible (attained at the extremal below). Equivalently \(\max_{S^*(\varphi)} |a_3 - \tfrac12 a_2^2| = -1/2 + sqrt(2)/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 (certificate on disk, independently rechecked).

Proof architecture

1. 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 (factored-DAG evaluator: see Certificate format below).
2. 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].
3. Certified branch-and-bound: float64 interval arithmetic with IEEE-754 forward-error inflation; 57,578,165 boxes processed, 28,789,083 leaves certified below the target \((-1/2 + sqrt(2)/2 + 0.001)^2\) (the prover bounds the SQUARED functional |L|^2).
4. Independent recheck: mpmath interval arithmetic (different arithmetic, same bound family with interval coefficients) over the near-critical leaves plus a random sample.

Recheck: 7,994 leaves re-verified; worst independent bound on |L|^2: 0.0433084323280055 vs target (V+eps)^2 = 0.0433084323758256.

Attainment (explicit extremal)

The attaining member has Schur parameters \(\gamma = e_{1}\), i.e. Schwarz function \(\omega(z) = z^{2}\): the extremal is \(f_0\) with \(zf_0'/f_0 = \varphi(z^{2})\), \(f_0(z) = z\,\exp\int_0^z \frac{\varphi(t^{2})-1}{t}\,dt\). Membership in \(S^*(\varphi)\) holds by construction (subordination through the inner function \(z^{2}\)) — no numerical membership check is involved.

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

Certificate format

terms is empty by design for the dag engine: the polynomial P is evaluated on the factored expression graph defined in gft/dag.py (classical factored Schur formulas, symbolically verified against the expanded derivation in tests/test_proofs.py). The certificate is therefore relative to the code at the git commit recorded in data/proofs/audit.jsonl for this prove event; the leaf partition (leaves_npz/leaves_parts) plus that code reproduce the verification.

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 - \tfrac12 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 - \tfrac12 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{\sqrt{2} r_{0}^{2}}{2} + \frac{r_{0}^{2}}{2} - \frac{1}{2} + \frac{\sqrt{2}}{2}\), \(C = - 2 \sqrt{2} r_{0}^{2} + 3 r_{0}^{2}\).

The maximum is \(-1/2 + sqrt(2)/2\), attained at \(\omega(z) = z^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 - \tfrac12 a_2^2| = -1/2 + sqrt(2)/2\).