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

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

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\), and the constant \(1/2\) is best possible (attained at the extremal below). Equivalently \(\max_{S^*(\varphi)} |a_3 - \tfrac12 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 (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; 46,485,173 boxes processed, 23,242,587 leaves certified below the target \((1/2 + 1e-06)^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,147 leaves re-verified; worst independent bound on |L|^2: 0.250001000000713 vs target (V+eps)^2 = 0.250001000001.

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\). Hence the bracket \([1/2,\ 1/2 + 1e-06]\) 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{1}{2} - \frac{r_{0}^{2}}{2}\), \(C = \frac{r_{0}^{2}}{2}\).

The maximum is \(1/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\).