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

{
 "status": "PROVED",
 "engine": "dag",
 "statement": "max over S*(cosh_sqrt) of |fekete_szego_mu1| <= 1/4 + 1e-06",
 "class": "cosh_sqrt",
 "functional": "fekete_szego_mu1",
 "bound": "1/4",
 "slack": 1e-06,
 "target_sq_hex": "0x1.00008637ce9d4p-4",
 "m": 2,
 "vars": [
  "x0",
  "x1",
  "x2",
  "x3"
 ],
 "boxes_processed": 248973,
 "n_leaves": 124487,
 "terms": [],
 "lemmas": [
  "schur-onto-coefficient-body",
  "rotation-reduction",
  "ieee754-forward-error",
  "bisection-partition",
  "fekete-szego-single-harmonic"
 ],
 "failure": null,
 "leaves_npz": "data/proofs/cosh_sqrt__fekete_szego_mu1.part0.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": {
  "proven": true,
  "method": "fs-m2-closed-form",
  "value_exact": "1/4",
  "value_float": 0.25,
  "bracket_lo": 0.25,
  "bracket_hi": 0.25,
  "extremal_gammas": [
   "0",
   "1"
  ],
  "extremal_omega": "z^2",
  "decomposition": {
   "L": "A*e^{i t} + C  (single harmonic in t)",
   "A_at_rho1": "\\frac{1}{4} - \\frac{r_{0}^{2}}{4}",
   "C_at_rho1": "- \\frac{5 r_{0}^{2}}{48}",
   "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/4",
   "value_float": 0.25,
   "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."
 }
}