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

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 = 3 Schur params · 7,555 boxes · 170,818 certified leaves

Full technical report

Certified enclosure: |H_2(2)| = |a_2 a_4 - a_3^2| over S*(limacon_0.3)

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

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/32 + 0.02\).

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

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; 7,555 boxes processed, 170,818 leaves certified below the target \((3/32 + 0.02)^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: 1,374 leaves re-verified; worst independent bound on |L|^2: 0.0129377726265949 vs target (V+eps)^2 = 0.0129390625.

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.

Reproduce & raw certificate

Reproduce: python3 -m gft.proofs prove limacon_0.3 hankel2_2 "3/32" --slack 0.02
Recheck: python3 -m gft.proofs recheck data/proofs/limacon_0.3__hankel2_2.json

{
 "status": "PROVED",
 "engine": "dag",
 "statement": "max over S*(limacon_0.3) of |hankel2_2| <= 3/32 + 0.02",
 "class": "limacon_0.3",
 "functional": "hankel2_2",
 "bound": "3/32",
 "slack": 0.02,
 "target_sq_hex": "0x1.a7fcb923a29c6p-7",
 "m": 3,
 "vars": [
  "x0",
  "x1",
  "x2",
  "x3",
  "x4",
  "x5",
  "x6"
 ],
 "boxes_processed": 7555,
 "n_leaves": 170818,
 "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"
 ],
 "failure": null,
 "leaves_parts": [
  "data/proofs/limacon_0.3__hankel2_2.w3.part0.npz",
  "data/proofs/limacon_0.3__hankel2_2.w2.part0.npz",
  "data/proofs/limacon_0.3__hankel2_2.w1.part0.npz",
  "data/proofs/limacon_0.3__hankel2_2.w0.part0.npz",
  "data/proofs/limacon_0.3__hankel2_2.final.npz"
 ],
 "sharp": {
  "class": "limacon_0.3",
  "functional": "hankel2_2",
  "bound": "3/32",
  "slack": 0.02,
  "bracket_lo": 0.09,
  "bracket_hi": 0.11375,
  "extremal_gammas": [
   0.0,
   1.0,
   0.0
  ],
  "candidate": {
   "value_exact": "9/100",
   "value_float": 0.09,
   "method": "attained extremal \u03c9=z\u00b2 (bracket_lo); moment-SOS-confirmed"
  },
  "exact": true,
  "note": "Candidate = the rigorously attained extremal value (sharp.bracket_lo, at \u03c9=z\u00b2), confirmed sharp by moment-SOS (gft/sos.py, cross-checked 3 ways) and equal to the general second-Hankel value (B\u2081/2)\u00b2 for S*(\u03c6) (Lee\u2013Ravichandran\u2013Supramaniam 2013). The earlier candidate equalled the loose B&B bound and exceeded (B\u2081/2)\u00b2 \u2014 impossible as a sharp value. Rigorous enclosure (bound/slack) unchanged; exact-rational upper certificate still open (heavy box)."
 }
}