{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R791",
  "content_hash": null,
  "slug": "tmpc-artifact-rational-root-certificate",
  "type": "artifact",
  "title": "Exact rational root isolation certificate",
  "summary": "A standard-library Python program proves both endpoint signs and the required lambda interval width using Fraction arithmetic.",
  "relevance": "For The sharp Dirichlet Poincare constant with two moment constraints, record tmpc-artifact-rational-root-certificate (“Exact rational root isolation certificate”) supplies evidence or a replay used to check the packet. The record states: A standard-library Python program proves both endpoint signs and the required lambda interval width using Fraction arithmetic.",
  "relevance_source": "recorded",
  "body": "All assertions use integers and `Fraction`. Decimal arithmetic is confined to display strings. The sine enclosure is its degree-49 Taylor polynomial plus or minus \\(z^{51}/51!\\); the cosine enclosure is its degree-48 polynomial plus or minus \\(z^{50}/50!\\). Substitution into \\(h(z)=\\sin z-z\\cos z\\) is outward rounded with exact fractions.\n\nThe canonical JSON output, without a trailing line feed, has SHA-256 digest `af00f1c39a3363414eb35d1d91973da3257ab6293b6006c00814e9e9ff4c34ef`. It records signs `[1,-1]`, the exact root interval, the exact lambda interval, and its width.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "the two rational root endpoints, their induced lambda interval, and all Taylor remainder bounds used in the sign test",
    "bounds": {
      "root_endpoints": {
        "min": 2,
        "max": 2
      },
      "sin_taylor_degree": {
        "min": 49,
        "max": 49
      },
      "cos_taylor_degree": {
        "min": 48,
        "max": 48
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "runnable",
    "kind": "inline_python_computation",
    "command": "python3 certificate.py",
    "runtime": "Python 3 standard library",
    "citation": {
      "url": "https://doi.org/10.1112/S0025579314000229",
      "locator": "Self-contained Python standard-library certificate reproduced by TheoremDB entry research on 2026-07-24"
    },
    "dependencies": "Python standard library only",
    "inline_source": "from fractions import Fraction\nfrom math import factorial\nfrom decimal import Decimal, getcontext\nfrom hashlib import sha256\nfrom json import dumps\ngetcontext().prec = 40\nz_lo = Fraction(449340945790, 10**11)\nz_hi = Fraction(449340945792, 10**11)\ndef trig_bounds(x, N=24):\n    s = sum(((-1)**j*x**(2*j+1)/factorial(2*j+1) for j in range(N+1)), Fraction())\n    c = sum(((-1)**j*x**(2*j)/factorial(2*j) for j in range(N+1)), Fraction())\n    rs = x**(2*N+3)/factorial(2*N+3)\n    rc = x**(2*N+2)/factorial(2*N+2)\n    return (s-rs, s+rs), (c-rc, c+rc)\ndef h_bounds(x):\n    (sl, su), (cl, cu) = trig_bounds(x)\n    return sl-x*cu, su-x*cl\nlo_h = h_bounds(z_lo)\nhi_h = h_bounds(z_hi)\nassert lo_h[0] > Fraction(3, 10**11)\nassert hi_h[1] < -Fraction(4, 10**11)\nlambda_lo = 4*z_lo*z_lo\nlambda_hi = 4*z_hi*z_hi\nwidth = lambda_hi-lambda_lo\nassert width < Fraction(1, 10**8)\ndef frac(q): return f'{q.numerator}/{q.denominator}'\ndef dec(q): return format(Decimal(q.numerator)/Decimal(q.denominator), '.20f')\nreport = {\n    'certified_h_signs': [1, -1],\n    'cos_taylor_degree': 48,\n    'h_margin_certificates': ['h(z_lo)>3/100000000000', 'h(z_hi)<-4/100000000000'],\n    'lambda_interval_decimal': [dec(lambda_lo), dec(lambda_hi)],\n    'lambda_interval_rational': [frac(lambda_lo), frac(lambda_hi)],\n    'lambda_interval_width': frac(width),\n    'sin_taylor_degree': 49,\n    'z_interval': [frac(z_lo), frac(z_hi)],\n}\npayload = dumps(report, sort_keys=True, separators=(',', ':'))\nassert sha256(payload.encode()).hexdigest() == 'af00f1c39a3363414eb35d1d91973da3257ab6293b6006c00814e9e9ff4c34ef'\nprint(payload)",
    "missing": [
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.1112/S0025579314000229",
    "locator": "Self-contained Python standard-library certificate reproduced by TheoremDB entry research on 2026-07-24"
  },
  "relations": [
    {
      "slug": "R793",
      "title": "The sharp eigenvalue is certified to ten decimal places",
      "object_type": "claim",
      "relation": "verifies",
      "direction": "outgoing"
    },
    {
      "slug": "R1825",
      "title": "Lean target for the exact rational root certificate",
      "object_type": "formalization",
      "relation": "verifies",
      "direction": "incoming"
    },
    {
      "slug": "two-moment-poincare-constant",
      "title": "two moment poincare constant",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}