The certificate reduces to these classical lemmas - each checkable by hand, independently of the engine.
schur-onto-coefficient-body
rotation-reduction
fekete-szego-single-harmonic
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.
Reproduce: python3 -m gft.proofs prove order_0.75 log_gamma2 "1/8" --slack 0
Recheck: python3 -m gft.proofs recheck data/proofs/order_0.75__log_gamma2.json
{
"status": "PROVED",
"engine": "closed-form",
"statement": "max over S*(order_0.75) of |log_gamma2| = 1/8 (proven exact, closed form)",
"class": "order_0.75",
"functional": "log_gamma2",
"bound": "1/8",
"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/8",
"value_float": 0.125,
"bracket_lo": 0.125,
"bracket_hi": 0.125,
"extremal_gammas": [
"0",
"1"
],
"extremal_omega": null,
"decomposition": {
"L": "A*e^{i t} + C (single harmonic in t)",
"A_at_rho1": "\\frac{1}{8} - \\frac{r_{0}^{2}}{8}",
"C_at_rho1": "\\frac{r_{0}^{2}}{8}",
"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/8",
"value_float": 0.125,
"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 a one-parameter family of extremals (rho=1, every r0 in [0,1]; representatives omega=z and omega=z^2) \u2014 a positive-dimensional maximizer set a fine-slack branch-and-bound cannot close; the closed form settles it exactly.",
"maximizer_dim": 1,
"maximizer_desc": "the one-parameter family \\(\\gamma_0=r_0\\in[0,1],\\ \\gamma_1=e^{i\\theta}\\) (\\(\\rho=1\\))",
"representatives": [
{
"r0": "1",
"omega": "z",
"gammas": [
"1",
"0"
]
},
{
"r0": "0",
"omega": "z^2",
"gammas": [
"0",
"1"
]
}
]
}
}
We use first-party site metrics to improve navigation: page visits, internal clicks, search result counts (not search terms), and approximate active time. A random tab ID groups events for seven days; GPC/DNT turns this off. The separate visitor count uses a self-hosted pseudonymous fingerprint and also respects GPC/DNT.