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

No matching publication turned up via the registry's automated keyword + reconciliation search of the 1,067-paper corpus. That search is imperfect - it can miss a result published under a differently-named class (e.g. SL* vs lemniscate) - so treat this as unconfirmed, not a novelty claim. Confirm with a manual search before claiming priority.

{
 "status": "PROVED",
 "engine": "closed-form",
 "statement": "max over S*(bean_tanh) of |a2a3| = 1/18  (proven exact, closed form)",
 "class": "bean_tanh",
 "functional": "a2a3",
 "bound": "1/18",
 "slack": 0.0,
 "m": 2,
 "proof": "closed-form-single-harmonic (m=2; positive-dimensional maximizer set; B&B does not close at fine slack)",
 "lemmas": [
  "schur-onto-coefficient-body",
  "rotation-reduction",
  "fekete-szego-single-harmonic"
 ],
 "failure": null,
 "sharp": {
  "proven": true,
  "method": "m2-closed-form",
  "value_exact": "1/18",
  "value_float": 0.05555555555555555,
  "bracket_lo": 0.05555555555555555,
  "bracket_hi": 0.05555555555555555,
  "extremal_gammas": [
   "2/3",
   "1"
  ],
  "extremal_omega": null,
  "decomposition": {
   "L": "A*e^{i t} + C  (single harmonic in t)",
   "A_at_rho1": "- \\frac{r_{0}^{3}}{8} + \\frac{r_{0}}{8}",
   "C_at_rho1": "\\frac{r_{0}^{3}}{32}",
   "angular_max": "max_t |L| = |A| + |C|  (triangle equality, sharp)"
  },
  "reference": "Single-angle Schur reduction + triangle equality in the phase: the m=2 coefficient body has one free angle, so |L| = |A e^{i t} + C| maximizes to |A| + |C| exactly.",
  "candidate": {
   "value_exact": "1/18",
   "value_float": 0.05555555555555555,
   "method": "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, no slack. The maximum is attained on 0 distinct extremals \u2014 a positive-dimensional maximizer set a fine-slack branch-and-bound cannot close; the closed form settles it exactly.",
  "maximizer_dim": 0,
  "maximizer_desc": "0 distinct extremals ()",
  "representatives": []
 }
}