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. Floating-point arithmetic is sound

Every float64 operation in the interval evaluation is widened by its IEEE-754 forward-error bound, so each computed interval rigorously encloses the true real value. The numerics are a certified enclosure, not a heuristic estimate.

IEEE-754 rounding; standard interval arithmetic. · ieee754-forward-error

4. The box partition is complete

Boxes are bisected at exactly representable midpoints, so the two children tile the parent with no gap and no overlap. The union of the certified leaf boxes is therefore provably the entire domain — coverage is exhaustive.

Exact dyadic subdivision. · bisection-partition

5. 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.

dag engine m = 2 Schur params · 593,153 boxes · 296,577 certified leaves

Full technical report

Sharp constant (proven exact): |a_3 - \frac{1}{4}\, a_2^2| over S*(limacon_0.5)

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

Theorem (sharp). If \(f(z) = z + \sum_{n \ge 2} a_n z^n \in S^*(\varphi)\), then \(|a_3 - \frac{1}{4}\, 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 - \frac{1}{4}\, 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

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).
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].
Certified branch-and-bound: float64 interval arithmetic with IEEE-754 forward-error inflation; 593,153 boxes processed, 296,577 leaves certified below the target \((1/2 + 1e-06)^2\) (the prover bounds the SQUARED functional |L|^2).
Independent recheck: mpmath interval arithmetic (different arithmetic, same bound family with interval coefficients) over the near-critical leaves plus a random sample.

Recheck: 2,387 leaves re-verified; worst independent bound on |L|^2: 0.250000999916405 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 - \frac{1}{4}\, 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 - \frac{1}{4}\, 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 - \frac{1}{4}\, 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{3 r_{0}^{2}}{8}\).

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 - \frac{1}{4}\, a_2^2| = 1/2\).

Reproduce & raw certificate

Reproduce: python3 -m gft.proofs prove limacon_0.5 fekete_szego_mu0.25 "1/2" --slack 1e-06
Recheck: python3 -m gft.proofs recheck data/proofs/limacon_0.5__fekete_szego_mu0.25.json

{
 "status": "PROVED",
 "engine": "dag",
 "statement": "max over S*(limacon_0.5) of |fekete_szego_mu0.25| <= 1/2 + 1e-06",
 "class": "limacon_0.5",
 "functional": "fekete_szego_mu0.25",
 "bound": "1/2",
 "slack": 1e-06,
 "target_sq_hex": "0x1.0000431be2e8bp-2",
 "m": 2,
 "vars": [
  "x0",
  "x1",
  "x2",
  "x3"
 ],
 "boxes_processed": 593153,
 "n_leaves": 296577,
 "terms": [],
 "evaluator": {
  "type": "factored-dag",
  "definition": "gft/dag.py (classical factored Schur formulas; symbolically verified against the expanded derivation in tests/test_proofs.py)",
  "code_commit": "see matching prove event in data/proofs/audit.jsonl"
 },
 "lemmas": [
  "schur-onto-coefficient-body",
  "rotation-reduction",
  "ieee754-forward-error",
  "bisection-partition",
  "fekete-szego-single-harmonic"
 ],
 "failure": null,
 "leaves_npz": "data/proofs/limacon_0.5__fekete_szego_mu0.25.part0.npz",
 "sharp": {
  "proven": true,
  "method": "fs-m2-closed-form",
  "value_exact": "1/2",
  "value_float": 0.5,
  "bracket_lo": 0.5,
  "bracket_hi": 0.5,
  "extremal_gammas": [
   "0",
   "1"
  ],
  "extremal_omega": "z^2",
  "decomposition": {
   "L": "A*e^{i t} + C  (single harmonic in t)",
   "A_at_rho1": "\\frac{1}{2} - \\frac{r_{0}^{2}}{2}",
   "C_at_rho1": "\\frac{3 r_{0}^{2}}{8}",
   "angular_max": "max_t |L| = |A| + |C|  (triangle equality, sharp)"
  },
  "reference": "Keogh-Merkes reduction (mechanized): single-angle Schur reduction + triangle equality in the phase.",
  "candidate": {
   "value_exact": "1/2",
   "value_float": 0.5,
   "method": "fs-m2-closed-form"
  },
  "exact": true,
  "note": "Proven exact (sharp). The Fekete-Szego functional reduces to a single harmonic in the one free angle, so max_t|L| = |A|+|C| exactly (triangle equality), and the sharp constant is the exact box maximum \u2014 the certified bracket closes to a point with no slack."
 }
}