{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R437",
  "content_hash": null,
  "slug": "l32peak-artifact-fixed-point-circle-bound",
  "type": "artifact",
  "title": "Exact fixed-point interval certificate for the incumbent",
  "summary": "A standard-library Python verifier encloses every grid value and every intervening arc using integer interval arithmetic.",
  "relevance": "For Flattest 32-term Littlewood polynomial on the unit circle, record l32peak-artifact-fixed-point-circle-bound (“Exact fixed-point interval certificate for the incumbent”) supplies evidence or a replay used to check the packet. The record states: A standard-library Python verifier encloses every grid value and every intervening arc using integer interval arithmetic.",
  "relevance_source": "recorded",
  "body": "The coefficient sequence, in increasing exponent order, is\n\\[\n(1,-1,1,1,-1,1,1,-1,-1,1,-1,-1,1,-1,1,-1,\n1,1,-1,-1,-1,-1,-1,-1,1,1,-1,-1,-1,1,1,1).\n\\]\nFor its aperiodic correlations \\(C_k\\), the verifier uses the exact identity\n\\[\nF(t)=|P(e^{it})|^2=32+2\\sum_{k=1}^{31}C_k\\cos(kt).\n\\]\nCosines on a \\(2^{18}\\)-point grid are enclosed at scale \\(10^{30}\\). The program starts from explicit rational bounds on \\(\\pi\\), reduces every angle to \\([0,\\pi/2]\\), and evaluates 24 terms of the alternating cosine series with outward integer rounding. The next term bounds the remainder. Sines are obtained by a quarter-turn of the same cosine table.\n\nFor a grid point \\(t_m\\), Taylor's theorem gives\n\\[\nF(t)\\leq F(t_m)+|F'(t_m)|h+\\tfrac12Bh^2,\n\\qquad h=\\pi/2^{18},\n\\]\nwhere the exact coefficient bound is\n\\[\nB=2\\sum_{k=1}^{31}k^2|C_k|=21264.\n\\]\nEvery point of the circle is within \\(h\\) of a grid point. The resulting all-cell comparison proves\n\\[\n7.7174710<\\max_{|z|=1}|P(z)|<7.7174713.\n\\]\nA separate 100-decimal Newton evaluation places the apparent maximizing angle at \\(0.9689875113845837543182660733966\\ldots\\) and the peak at \\(7.717471112388378843091998621392\\ldots\\), consistent with the certified enclosure. The integer certificate supplies the stated bound without relying on that Newton calculation.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "rigorous full-circle peak bounds for the displayed 32-term Littlewood polynomial",
    "bounds": {
      "terms": {
        "min": 32,
        "max": 32
      },
      "grid_points": {
        "min": 262144,
        "max": 262144
      },
      "fixed_point_decimal_places": {
        "min": 30,
        "max": 30
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "inline_python_computation",
    "entrypoint": "join source_lines with newline and run with python3",
    "runtime": "CPython 3.9 or later, standard library only",
    "citation": {
      "url": "https://doi.org/10.4007/annals.2020.192.3.6",
      "locator": "Self-contained CPython standard-library interval computation executed on 2026-07-25"
    },
    "inline_source": [
      "from hashlib import sha256",
      "from json import dumps",
      "",
      "S = 10**30",
      "PI_LO = 3141592653589793238462643383279",
      "PI_HI = PI_LO + 1",
      "M = 1 << 18",
      "TERMS = 24",
      "signs = [1,-1,1,1,-1,1,1,-1,-1,1,-1,-1,1,-1,1,-1,1,1,-1,-1,-1,-1,-1,-1,1,1,-1,-1,-1,1,1,1]",
      "",
      "def ceildiv(a, b):",
      "    return -((-a)//b)",
      "",
      "cos_table = []",
      "for r in range(M//4+1):",
      "    xlo = 2*PI_LO*r//M",
      "    xhi = ceildiv(2*PI_HI*r, M)",
      "    ylo = xlo*xlo//S",
      "    yhi = ceildiv(xhi*xhi, S)",
      "    tlo = thi = slo = shi = S",
      "    for n in range(1, TERMS+1):",
      "        den = (2*n-1)*(2*n)",
      "        tlo = tlo*ylo//(S*den)",
      "        thi = ceildiv(thi*yhi, S*den)",
      "        if n & 1:",
      "            slo -= thi",
      "            shi -= tlo",
      "        else:",
      "            slo += tlo",
      "            shi += thi",
      "    n = TERMS+1",
      "    rem = ceildiv(thi*yhi, S*(2*n-1)*(2*n))",
      "    cos_table.append((slo-rem, shi+rem))",
      "",
      "def cos_bounds(r):",
      "    r %= M",
      "    if r > M//2:",
      "        r = M-r",
      "    if r <= M//4:",
      "        return cos_table[r]",
      "    lo, hi = cos_table[M//2-r]",
      "    return -hi, -lo",
      "",
      "def sin_bounds(r):",
      "    return cos_bounds(M//4-r)",
      "",
      "corr = [sum(signs[j]*signs[j+k] for j in range(32-k)) for k in range(1,32)]",
      "b2 = 2*sum(k*k*abs(a) for k,a in enumerate(corr,1))",
      "max_grid_lo = -10**100",
      "max_grid_hi = -10**100",
      "max_lo_index = max_hi_index = 0",
      "best_taylor_num = -1",
      "best_taylor_index = 0",
      "best_derivative_abs = 0",
      "taylor_den = 2*S*S*M*M",
      "for m in range(M):",
      "    flo = fhi = 32*S",
      "    dlo = dhi = 0",
      "    for k,a in enumerate(corr,1):",
      "        lo,hi = cos_bounds(k*m)",
      "        q = 2*a",
      "        if q >= 0:",
      "            flo += q*lo",
      "            fhi += q*hi",
      "        else:",
      "            flo += q*hi",
      "            fhi += q*lo",
      "        lo,hi = sin_bounds(k*m)",
      "        q = -2*k*a",
      "        if q >= 0:",
      "            dlo += q*lo",
      "            dhi += q*hi",
      "        else:",
      "            dlo += q*hi",
      "            dhi += q*lo",
      "    if flo > max_grid_lo:",
      "        max_grid_lo,max_lo_index = flo,m",
      "    if fhi > max_grid_hi:",
      "        max_grid_hi,max_hi_index = fhi,m",
      "    derivative_abs = max(abs(dlo),abs(dhi))",
      "    taylor_num = 2*fhi*S*M*M + 2*derivative_abs*PI_HI*M + b2*PI_HI*PI_HI",
      "    if taylor_num > best_taylor_num:",
      "        best_taylor_num = taylor_num",
      "        best_taylor_index = m",
      "        best_derivative_abs = derivative_abs",
      "assert (max_lo_index,max_hi_index,best_taylor_index) == (40428,40428,40428)",
      "assert max_grid_lo*10**14 > 77174710**2*S",
      "assert best_taylor_num*10**14 < 77174713**2*taylor_den",
      "assert (2**30 + 2**15)//2 == 536887296",
      "report = {",
      "    \"autocorrelations\": corr,",
      "    \"certified_circle_amplitude_upper\": \"7.7174713\",",
      "    \"certified_grid_amplitude_lower\": \"7.7174710\",",
      "    \"coefficient_signs\": signs,",
      "    \"grid_argmax_index\": max_hi_index,",
      "    \"grid_max_lower_numerator\": max_grid_lo,",
      "    \"grid_max_upper_numerator\": max_grid_hi,",
      "    \"grid_scale\": S,",
      "    \"grid_size\": M,",
      "    \"normalized_reversal_orbits\": 536887296,",
      "    \"second_derivative_bound\": b2,",
      "    \"taylor_argmax_index\": best_taylor_index,",
      "    \"taylor_derivative_abs_upper_numerator\": best_derivative_abs,",
      "    \"taylor_upper_denominator\": taylor_den,",
      "    \"taylor_upper_numerator\": best_taylor_num,",
      "}",
      "payload = dumps(report, sort_keys=True, separators=(\",\",\":\"))",
      "print(payload)",
      "print(\"report_sha256=\"+sha256(payload.encode()).hexdigest())"
    ],
    "missing": [
      "command",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.4007/annals.2020.192.3.6",
    "locator": "Self-contained CPython standard-library interval computation executed on 2026-07-25"
  },
  "models": [],
  "relations": [
    {
      "slug": "R439",
      "title": "The minimum peak lies between 1064^(1/4) and 7.7174713",
      "object_type": "claim",
      "relation": "supports",
      "direction": "outgoing"
    },
    {
      "slug": "littlewood-32-minimum-peak",
      "title": "littlewood 32 minimum peak",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}