Hankel H₂(2) over Four-leaf S*_{4L} · Geometric Function Atlas

← all proofs

Certificate under review. This legacy or incomplete artifact is retained for audit, but cannot carry public proof wording until its v1 replay contract validates.

Stored legacy claim for Hankel H₂(2) over Four-leaf S*_{4L}. Its proof wording is withheld pending a valid replayable v1 certificate.

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

Papers in the corpus touching this class and functional - check whether the bound is already published before you cite the machine result.

Fekete-Szegö Problem and Second Hankel Determinant for a Subclass of Bi-Univalent Functions Associated With Four Leaf Domain
Timilehin Gideon Shaba, Serkan Aracı, B.O. Adebesin · 2023

dag engine m = 3 Schur params · 9,671 boxes · 71,753 certified leaves

Reproduce & raw certificate

Reproduce: python3 -m gft.proofs prove four_leaf hankel2_2 "3/16" --slack 0.02
Recheck: python3 -m gft.proofs recheck data/proofs/four_leaf__hankel2_2.json

{
 "status": "PROVED",
 "engine": "dag",
 "statement": "max over S*(four_leaf) of |hankel2_2| <= 3/16 + 0.02",
 "class": "four_leaf",
 "functional": "hankel2_2",
 "bound": "3/16",
 "slack": 0.02,
 "target_sq_hex": "0x1.60b780346dc5cp-5",
 "m": 3,
 "vars": [
  "x0",
  "x1",
  "x2",
  "x3",
  "x4",
  "x5",
  "x6"
 ],
 "boxes_processed": 9671,
 "n_leaves": 71753,
 "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/four_leaf__hankel2_2.w1.part0.npz",
  "data/proofs/four_leaf__hankel2_2.w2.part0.npz",
  "data/proofs/four_leaf__hankel2_2.w3.part0.npz",
  "data/proofs/four_leaf__hankel2_2.w0.part0.npz",
  "data/proofs/four_leaf__hankel2_2.final.npz"
 ],
 "sharp": {
  "class": "four_leaf",
  "functional": "hankel2_2",
  "bound": "3/16",
  "slack": 0.02,
  "bracket_lo": 0.1736111111111111,
  "bracket_hi": 0.2075,
  "extremal_gammas": [
   0.0,
   1.0,
   0.0
  ],
  "candidate": {
   "value_exact": "25/144",
   "value_float": 0.1736111111111111,
   "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)."
 }
}