Certified enclosure: |H_2(2)| = |a_2 a_4 - a_3^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 (machine-certified bracket). If \(f(z) = z + \sum_{n \ge 2} a_n z^n \in S^*(\varphi)\), then \(|H_2(2)| = |a_2 a_4 - a_3^2| \le 3/4 - sqrt(2)/2 + 0.01\). Moreover \(3/4 - sqrt(2)/2\) is attained (see Attainment below), so the sharp constant lies in \([3/4 - sqrt(2)/2,\ 3/4 - sqrt(2)/2 + 0.01]\).

This is a certified enclosure with attained lower endpoint — not yet an exact sharp theorem: closing the bracket to width zero needs a local second-variation certificate at the extremal (see Open obligation).

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; 11,111 boxes processed, 5,556 leaves certified below the target \((3/4 - sqrt(2)/2 + 0.01)^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: 437 leaves re-verified; worst independent bound on |L|^2: 0.00279459338044167 vs target (V+eps)^2 = 0.00279769259644776.

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): \(|H_2(2)| = |a_2 a_4 - a_3^2| = 0.042893218813452476\). Hence the bracket \([3/4 - sqrt(2)/2,\ 3/4 - sqrt(2)/2 + 0.01]\) 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.

Open obligation

The bracket has width slack; closing it to the exact constant needs a local second-variation certificate at the extremal (planned). Every other step is machine-certified; the Schur-body theorem and the rotation lemma are the two classical facts a referee checks by hand.