← all proofs

What this rests on

The certificate reduces to these classical lemmas - each checkable by hand, independently of the engine.

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

{
 "status": "PROVED",
 "engine": "dag",
 "statement": "max over S*(strongly_0.25) of |hankel2_2| <= 1/16 + 0.01",
 "class": "strongly_0.25",
 "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": 11683,
 "n_leaves": 5842,
 "terms": [],
 "lemmas": [
  "schur-onto-coefficient-body",
  "rotation-reduction",
  "ieee754-forward-error",
  "bisection-partition"
 ],
 "failure": null,
 "leaves_parts": [
  "data/proofs/strongly_0.25__hankel2_2.w3.part0.npz",
  "data/proofs/strongly_0.25__hankel2_2.w1.part0.npz",
  "data/proofs/strongly_0.25__hankel2_2.w0.part0.npz",
  "data/proofs/strongly_0.25__hankel2_2.w2.part0.npz",
  "data/proofs/strongly_0.25__hankel2_2.final.npz"
 ],
 "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"
 },
 "sharp": {
  "class": "strongly_0.25",
  "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."
 }
}