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 · 10,987 boxes · 5,494 certified leaves

Full technical report

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

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

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 1/16 + 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

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; 10,987 boxes processed, 5,494 leaves certified below the target \((1/16 + 0.01)^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,507 leaves re-verified; worst independent bound on |L|^2: 0.00525597061373758 vs target (V+eps)^2 = 0.00525625.

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 bean_tanh hankel2_2 "1/16" --slack 0.01
Recheck: python3 -m gft.proofs recheck data/proofs/bean_tanh__hankel2_2.json

{
 "status": "PROVED",
 "engine": "dag",
 "statement": "max over S*(bean_tanh) of |hankel2_2| <= 1/16 + 0.01",
 "class": "bean_tanh",
 "functional": "hankel2_2",
 "bound": "1/16",
 "slack": 0.01,
 "target_sq_hex": "0x1.58793dd97f62ap-8",
 "m": 3,
 "vars": [
  "x0",
  "x1",
  "x2",
  "x3",
  "x4",
  "x5",
  "x6"
 ],
 "boxes_processed": 10987,
 "n_leaves": 5494,
 "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/bean_tanh__hankel2_2.w0.part0.npz",
  "data/proofs/bean_tanh__hankel2_2.w1.part0.npz",
  "data/proofs/bean_tanh__hankel2_2.w2.part0.npz",
  "data/proofs/bean_tanh__hankel2_2.w3.part0.npz",
  "data/proofs/bean_tanh__hankel2_2.final.npz"
 ],
 "sharp": {
  "class": "bean_tanh",
  "functional": "hankel2_2",
  "bound": "1/16",
  "slack": 0.01,
  "bracket_lo": 0.0625,
  "bracket_hi": 0.0725,
  "extremal_gammas": [
   0.0,
   1.0,
   0.0
  ],
  "candidate": {
   "value_exact": "1/16",
   "value_float": 0.0625,
   "method": "declared bound"
  },
  "exact": true,
  "note": "Candidate exact constant recognised from the certified bracket and matched to the attained extremal value. Not a proof; sharp closure requires the second-variation certificate."
 }
}