{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R85",
  "content_hash": null,
  "slug": "c31m-artifact-exact-replay",
  "type": "artifact",
  "title": "Exact lower-witness and upper-certificate replay",
  "summary": "The standard-library program uses Fraction for every average, quotient, and certificate identity, then Decimal only for display.",
  "relevance": "For Sharp L2 norm of the centered maximal operator on C_31, record c31m-artifact-exact-replay (“Exact lower-witness and upper-certificate replay”) supplies evidence or a replay used to check the packet. The record states: The standard-library program uses Fraction for every average, quotient, and certificate identity, then Decimal only for display.",
  "relevance_source": "recorded",
  "body": "The replay evaluates each of the sixteen centered averages at each of the 31 coordinates. It verifies the active-radius vector, reduces the squared quotient to its exact fraction, and proves the stated decimal lower bound by cross multiplication. For the upper endpoint it checks\n\\(\\sum_{|k|\\leq r}((2r+1)^2d_k)^{-1}=1\\) at every radius. It then sums the radial weights and obtains \\(1916477/720720\\).\n\nThe witness together with its active radii has SHA-256 digest `d6e9301b3a7dc898333a7bb1c2d70a9516db17e08bc9650ea0830d128c9f5cab`. The six-line output has SHA-256 digest `5b55424e8e5e369a4b7034305fc525ae05286e9d9cd7c6f049841ecd565ca8b4`.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "all 496 averages of the displayed C_31 witness and all sixteen weighted upper-certificate identities",
    "bounds": {
      "cycle_order": {
        "min": 31,
        "max": 31
      },
      "witness_averages": {
        "min": 496,
        "max": 496
      },
      "upper_certificate_constraints": {
        "min": 16,
        "max": 16
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "inline_python_exact_computation",
    "entrypoint": "Join source_lines with LF characters and execute the resulting Python program",
    "runtime": "CPython 3.9 or later, standard library only",
    "citation": {
      "url": "https://arxiv.org/abs/2005.03146",
      "locator": "Inline Python standard-library computation executed by TheoremDB entry research on 2026-07-25"
    },
    "inline_source": [
      "from decimal import Decimal, getcontext",
      "from fractions import Fraction",
      "from hashlib import sha256",
      "import json",
      "",
      "n = 31",
      "witness = [60240784093944,71756706270677,71756706270677,69429053137658,69429053137658,124946197568962,124946197568962,634350542282289,220384421138340,634350542282289,124946197568962,124946197568962,69429053137658,69429053137658,71756706270677,71756706270677,60240784093944,60240784093944,53164211021439,53164211021439,49020565351307,49020565351307,47095643667602,47095643667602,47095643667602,47095643667602,49020565351307,49020565351307,53164211021439,53164211021439,60240784093944]",
      "expected_radii = [9,8,7,6,5,4,1,0,1,0,1,4,5,6,7,8,9,10,11,12,13,15,15,15,15,15,15,13,12,11,10]",
      "",
      "def average(j, r):",
      "    return Fraction(sum(witness[(j + k) % n] for k in range(-r, r + 1)), 2*r + 1)",
      "",
      "maxima = []",
      "radii = []",
      "for j in range(n):",
      "    values = [average(j, r) for r in range(16)]",
      "    best = max(values)",
      "    assert sum(value == best for value in values) == 1",
      "    maxima.append(best)",
      "    radii.append(values.index(best))",
      "assert radii == expected_radii",
      "ratio_squared = sum(value*value for value in maxima) / sum(value*value for value in witness)",
      "assert ratio_squared == Fraction(95224622960985697907125617859822805279079620426252, 53808054668649331334697257108564850111138302100375)",
      "assert ratio_squared > Fraction(13303042705, 10**10)**2",
      "",
      "weights = [Fraction(1)] + [Fraction(1, 4*k) for k in range(1, 16)]",
      "for r in range(16):",
      "    length = 2*r + 1",
      "    reciprocal_sum = sum(Fraction(1, length*length) / weights[abs(k)] for k in range(-r, r + 1))",
      "    assert reciprocal_sum == 1",
      "upper_squared = weights[0] + 2*sum(weights[1:])",
      "assert upper_squared == Fraction(1916477, 720720)",
      "",
      "payload = json.dumps({'witness': witness, 'radii': radii}, separators=(',', ':')).encode()",
      "payload_digest = sha256(payload).hexdigest()",
      "assert payload_digest == 'd6e9301b3a7dc898333a7bb1c2d70a9516db17e08bc9650ea0830d128c9f5cab'",
      "getcontext().prec = 60",
      "lower = (Decimal(ratio_squared.numerator) / Decimal(ratio_squared.denominator)).sqrt()",
      "upper = (Decimal(upper_squared.numerator) / Decimal(upper_squared.denominator)).sqrt()",
      "print(f'witness_sha256={payload_digest}')",
      "print('active_radii=' + ','.join(map(str, radii)))",
      "print(f'ratio_squared={ratio_squared.numerator}/{ratio_squared.denominator}')",
      "print(f'ratio={lower}')",
      "print(f'upper_squared={upper_squared.numerator}/{upper_squared.denominator}')",
      "print(f'upper={upper}')"
    ],
    "missing": [
      "command",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://arxiv.org/abs/2005.03146",
    "locator": "Inline Python standard-library computation executed by TheoremDB entry research on 2026-07-25"
  },
  "relations": [
    {
      "slug": "R89",
      "title": "An exact integer witness attains ratio 1.3303042705991634737...",
      "object_type": "claim",
      "relation": "evidences",
      "direction": "outgoing"
    },
    {
      "slug": "R88",
      "title": "A weighted Cauchy-Schwarz certificate gives N_31 squared at most 1916477/720720",
      "object_type": "claim",
      "relation": "evidences",
      "direction": "outgoing"
    },
    {
      "slug": "c31-centered-maximal-l2-norm",
      "title": "c31 centered maximal l2 norm",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}