Machine proofs of sharp coefficient-functional bounds: methods

Technical report for the gft.proofs certified-optimization proof factory (v2, 2026-06-11). Companion to the per-theorem certificates in this directory and to the blog posts "Trust, but Verify" and "Beyond Verification".

1. What is being proved

Statements of the form

For every f ∈ S*(φ): |L(a₂, …, a₅)| ≤ V + ε

where S*(φ) is a Ma–Minda starlike class, L is a coefficient functional (Fekete–Szegő, Zalcman a₃²−a₅, Hankel determinants H₂(2), H₃(1)), V is the conjectured sharp value (typically an exact rational identified by the discovery experiments), and ε is an explicit tiny slack (10⁻⁶ or better). Combined with the attainment certificate (an explicit member achieving V, verified in interval arithmetic), each theorem brackets the sharp constant in [V, V + ε].

The slack is honest: closing ε → 0 needs a local argument at the extremal (second-variation certificate), which is planned but not yet mechanized. Everything else is machine-certified.

2. The reduction (exact, no truncation)

1. Membership. f ∈ S*(φ) ⟺ zf′/f = φ(ω) for a Schwarz function ω. The coefficients a₂..a₅ of f are explicit polynomials in the Taylor coefficients c₁..c₄ of ω and the (exact, real) Taylor coefficients B₁..B₄ of φ — derived symbolically via the exponential recurrence, and cross-validated against an independent FFT-based pipeline to 10⁻¹⁵ at random members.

2. Coefficient body. The set of feasible (c₁, …, c₄) is exactly the image of the closed polydisk under the Schur-parameter map. We use the classical factored formulas (w_k := 1 − |γ_k|²):

   c₁ = γ₀ c₂ = w₀γ₁ c₃ = w₀(w₁γ₂ − γ̄₀γ₁²) c₄ = w₀(w₁w₂γ₃ − w₁γ̄₁γ₂² − 2w₁γ̄₀γ₁γ₂ + γ̄₀²γ₁³)

verified symbolically (exact polynomial identity) against the series expansion of the Schur recursion. 3. Rotation lemma (human-checkable, one line per functional). All four functionals are weight-homogeneous under the rotation conjugation f ↦ e^{−iθ}f(e^{iθ}z), which maps S*(φ) onto itself and c_k ↦ e^{ikθ}c_k; hence γ₀ = c₁ may be taken real in [0, 1]. 4. Polar box. γ_k = r_k e^{it_k}; the feasible set is the exact box [0,1]^m × [0,2π]^{m−1}. cos t_k, sin t_k are enclosed over each t-subinterval (endpoint + critical-angle analysis), and the (C_k, S_k)-rectangle contains the true arc, so every bound computed over it covers the feasible set.

After the reduction, "the theorem" is: an explicit polynomial P = |L|² is ≤ (V+ε)² on a compact box. That is a finite, checkable claim.

3. Rigorous arithmetic

Two implementations, used prover/checker style:

• Prover: batched float64 interval arithmetic with forward-error inflation — after every add/multiply/power the enclosure is widened by the standard IEEE-754 relative-error bound, so computed bounds are true bounds (the classical forward-error lemma; padding is ~4·2⁻⁵² per operation, orders of magnitude below the proof slack).
• Checker: mpmath.iv (arbitrary-precision interval arithmetic, an independent implementation) re-verifies the certificate's leaf boxes.

4. Bound forms — and why the expression representation matters

Three rigorous upper-bound forms are computed per box; the minimum is used:

1. plain interval extension (O(h) overestimate),
2. first-order centered form P(mid) + Σ max|∂_vP(box)|·h_v (O(h²)),
3. second-order Taylor form P(mid) + Σ|∂_vP(mid)|·h_v + ½Σ max|H_ij(box)|·h_i·h_j (gradient at a point, so every error term carries a small width — this is what converges at attained maxima on boundary faces).

Plus two standard accelerators:

• Monotonicity slide: where the interval gradient is sign-definite the maximum lies on the corresponding face; the box collapses in that dimension. This is the mechanized analog of the phase-normalization steps in the human proofs.
• Gradient-aware bisection: split the dimension whose smear term actually blocks certification (degenerate faces need boxes thin in one direction only — isotropic splitting is exponentially wasteful).

The dependency lesson (v1 → v2). Interval arithmetic loses correlations between multiple occurrences of a variable. On the degenerate Schur faces (|γ₀| = 1, where the parameterization collapses), the expanded polynomial's interval Hessian evaluates to [−0.44, +0.44] where the truth is exactly 0 — an h-independent 1.6×10⁻² floor that no subdivision fixes. v2 therefore evaluates the factored expression graph (hash-consed DAG, built from the factored coefficient formulas above, never expanded): (1 − r₀²) is computed once as a tiny interval and annihilates everything it multiplies. The measured effect on the v1 killer box: 1.6×10⁻² → 7.6×10⁻¹⁴. A residual dependency (w₀ + r₀² ≡ 1 along certain attainment lines) still blocks the Fekete–Szegő/H₂(2) calibrations; the H₃(1) family is unaffected because its extremal γ = (0, 0, ε) sits where those factors vanish. We report this openly: which statements this machine can currently prove is determined by where their extremals live.

5. The trust chain

No stochastic component anywhere; no LLM anywhere. Every run is deterministic and reproducible from the repository.

6. Status taxonomy

• PROVED (bracket): max ≤ V + ε machine-certified; ≥ V attained.
• FAILED + witness: the bound is false near the witness, or the evaluator cannot yet converge there (the certificate says which).
• Sharp-value claims (ε = 0) remain conjectures pending the local certificate at the extremal.