{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R399",
  "content_hash": null,
  "slug": "hs16-artifact-root-enclosure",
  "type": "artifact",
  "title": "Exact rational Rouché enclosure for one simple zero",
  "summary": "Fraction arithmetic proves one zero in a radius 5e-14 disk, then places its real representative in a rectangle of diameter below 3e-15.",
  "relevance": "For Nearest hard-square partition-function zero for the sixteen grid, record hs16-artifact-root-enclosure (“Exact rational Rouché enclosure for one simple zero”) supplies evidence or a replay used to check the packet. The record states: Fraction arithmetic proves one zero in a radius 5e-14 disk, then places its real representative in a rectangle of diameter below 3e-15.",
  "relevance_source": "recorded",
  "body": "Put \\(c=-0.12200537154105\\), \\(R=5\\mathbin{\\cdot}10^{-14}\\), and expand\n\\[\nZ_{16}(c+t)=\\sum_{j=0}^{128}b_jt^j\n\\]\nwith exact rational \\(b_j\\). On \\(|t|=R\\), the linear part obeys\n\\[\n|b_0+b_1t|\\geq |b_1|R-|b_0|.\n\\]\nThe exact calculation proves that this lower bound exceeds \\(11298452952\\) times \\(\\sum_{j\\geq2}|b_j|R^j\\). The linear zero lies inside the circle, so Rouché's theorem gives exactly one zero there, counted with multiplicity.\n\nExact endpoint signs place a real zero between -0.122005371541038 and -0.122005371541037. The stated rectangle lies inside the Rouché disk. It therefore contains that zero and no second zero.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "one local complex disk and one contained rational rectangle near -0.122005371541037445 for the exact degree-128 polynomial Z16",
    "bounds": {
      "polynomial_degree": {
        "min": 128,
        "max": 128
      },
      "rouche_disk_radius_numerator": {
        "min": 5,
        "max": 5
      },
      "rouche_disk_radius_denominator": {
        "min": 100000000000000,
        "max": 100000000000000
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "inline_python_exact_root_certificate",
    "entrypoint": "Place the transfer output at hs16_coefficients.json, join source_lines with newline characters, save as certify.py, and run python3 certify.py",
    "runtime": "CPython 3.8 or later, standard library only",
    "citation": {
      "url": "https://doi.org/10.1007/s10955-004-2055-4",
      "locator": "Inline Python 3 rational certificate executed on 2026-07-25"
    },
    "inline_source": [
      "from fractions import Fraction",
      "from hashlib import sha256",
      "from json import dumps, load",
      "from math import comb",
      "with open('hs16_coefficients.json') as handle:",
      "    coefficients = load(handle)",
      "assert len(coefficients) == 129",
      "csv = ','.join(map(str, coefficients))",
      "assert sha256(csv.encode()).hexdigest() == 'a65ab0dc72ec69b3408416bfc816478869e6542f1076592842277e109c515d96'",
      "def value(row, x):",
      "    answer = Fraction(0)",
      "    for coefficient in reversed(row):",
      "        answer = answer * x + coefficient",
      "    return answer",
      "left = Fraction(-122005371541038, 10**15)",
      "right = Fraction(-122005371541037, 10**15)",
      "imaginary_radius = Fraction(1, 10**15)",
      "assert value(coefficients, left) < 0 < value(coefficients, right)",
      "center = Fraction(-2440107430821, 2 * 10**13)",
      "radius = Fraction(5, 10**14)",
      "taylor = [",
      "    sum(Fraction(coefficients[k] * comb(k, j)) * center**(k-j) for k in range(j, len(coefficients)))",
      "    for j in range(len(coefficients))",
      "]",
      "tail = sum(abs(taylor[j]) * radius**j for j in range(2, len(taylor)))",
      "linear_margin = abs(taylor[1]) * radius - abs(taylor[0])",
      "assert abs(taylor[0]) < abs(taylor[1]) * radius",
      "assert linear_margin > 11298452952 * tail",
      "assert all((x-center)**2 + imaginary_radius**2 < radius**2 for x in (left, right))",
      "report = {",
      "    'coefficient_csv_sha256': sha256(csv.encode()).hexdigest(),",
      "    'degree': 128,",
      "    'endpoint_signs': [-1, 1],",
      "    'root_rectangle': {",
      "        'real': ['-0.122005371541038', '-0.122005371541037'],",
      "        'imag': ['-0.000000000000001', '0.000000000000001'],",
      "        'diameter_upper': '0.000000000000003',",
      "    },",
      "    'rouche_disk': {",
      "        'center': '-0.12200537154105',",
      "        'radius': '0.00000000000005',",
      "        'linear_margin_over_tail_gt': 11298452952,",
      "    },",
      "    'zeros_in_disk': 1,",
      "    'z_at_1': str(sum(coefficients)),",
      "}",
      "payload = dumps(report, sort_keys=True, separators=(',', ':'))",
      "assert sha256(payload.encode()).hexdigest() == '628e3166033acfe07a7fbef5eb88aa4dfc7b5d23acd7a66f0ad9e122dda63dd8'",
      "print(payload)",
      "print('report_sha256=' + sha256(payload.encode()).hexdigest())"
    ],
    "missing": [
      "command",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.1007/s10955-004-2055-4",
    "locator": "Inline Python 3 rational certificate executed on 2026-07-25"
  },
  "relations": [
    {
      "slug": "R401",
      "title": "A certified radius bracket and an isolated real zero for the sixteen grid",
      "object_type": "claim",
      "relation": "supports",
      "direction": "outgoing"
    },
    {
      "slug": "hard-square-sixteen-zero-radius",
      "title": "hard square sixteen zero radius",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}