{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R483",
  "content_hash": null,
  "slug": "m127ac-artifact-chain-replay",
  "type": "artifact",
  "title": "Replayable 136-step addition chain",
  "summary": "A standard-library verifier reconstructs the displayed chain, checks all 136 sums, and fixes its canonical digest.",
  "relevance": "For Shortest addition chain for the 127th Mersenne number, record m127ac-artifact-chain-replay (“Replayable 136-step addition chain”) supplies evidence or a replay used to check the packet. The record states: A standard-library verifier reconstructs the displayed chain, checks all 136 sums, and fixes its canonical digest.",
  "relevance_source": "recorded",
  "body": "The `chain_values_decimal` field is the complete chain in order, including the initial 1. The verifier reconstructs the same list from the exponent star chain. For every appended value it records the two earlier indices used in the sum, checks those indices, checks strict increase, and verifies the final target.\n\nThe canonical compact JSON encoding of the integer list has SHA-256 digest `fb5519926465307c1ea1fd9901cbc1adbf329f51ccd0c820c3f8feef4b34f08f`. The compact report has digest `a51cd95631b6424c80e0d70e8a112814f61603489f60b02300d4763de2c03014`.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "all 136 additions in the displayed chain ending at 2^127-1",
    "bounds": {
      "additions": {
        "min": 136,
        "max": 136
      },
      "chain_values": {
        "min": 137,
        "max": 137
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "inline_python_certificate",
    "entrypoint": "join source_lines with newline and run with python3",
    "runtime": "CPython 3, standard library only",
    "citation": {
      "url": "https://wwwhomes.uni-bielefeld.de/achim/addition_chain.html",
      "locator": "Inline CPython standard-library verifier executed by TheoremDB entry research on 2026-07-25"
    },
    "outputs": "{\"chain_elements\":137,\"chain_length\":136,\"chain_sha256\":\"fb5519926465307c1ea1fd9901cbc1adbf329f51ccd0c820c3f8feef4b34f08f\",\"exponent_chain\":[1,2,3,5,7,14,28,56,63,126,127],\"target\":170141183460469231731687303715884105727,\"valid_additions\":136}\nsha256=a51cd95631b6424c80e0d70e8a112814f61603489f60b02300d4763de2c03014\n",
    "inline_source": [
      "from hashlib import sha256",
      "from json import dumps",
      "",
      "EXPONENT_CHAIN = (1, 2, 3, 5, 7, 14, 28, 56, 63, 126, 127)",
      "TARGET = (1 << 127) - 1",
      "chain = [1]",
      "parents = []",
      "known = {1: 0}",
      "",
      "for a, c in zip(EXPONENT_CHAIN, EXPONENT_CHAIN[1:]):",
      "    b = c - a",
      "    assert chain[-1] == (1 << a) - 1",
      "    assert (1 << b) - 1 in known",
      "    for _ in range(b):",
      "        j = len(chain) - 1",
      "        chain.append(chain[j] + chain[j])",
      "        parents.append((j, j))",
      "    j = len(chain) - 1",
      "    k = known[(1 << b) - 1]",
      "    chain.append(chain[j] + chain[k])",
      "    parents.append((j, k))",
      "    known[chain[-1]] = len(chain) - 1",
      "",
      "assert len(chain) == 137",
      "assert len(parents) == 136",
      "assert chain[-1] == TARGET",
      "assert all(chain[i - 1] < chain[i] for i in range(1, len(chain)))",
      "for i, (j, k) in enumerate(parents, 1):",
      "    assert j < i and k < i",
      "    assert chain[i] == chain[j] + chain[k]",
      "",
      "chain_payload = dumps(chain, separators=(',', ':'))",
      "chain_digest = sha256(chain_payload.encode()).hexdigest()",
      "assert chain_digest == 'fb5519926465307c1ea1fd9901cbc1adbf329f51ccd0c820c3f8feef4b34f08f'",
      "report = {",
      "    'chain_elements': len(chain),",
      "    'chain_length': len(chain) - 1,",
      "    'chain_sha256': chain_digest,",
      "    'exponent_chain': list(EXPONENT_CHAIN),",
      "    'target': TARGET,",
      "    'valid_additions': len(parents),",
      "}",
      "payload = dumps(report, sort_keys=True, separators=(',', ':'))",
      "digest = sha256(payload.encode()).hexdigest()",
      "assert digest == 'a51cd95631b6424c80e0d70e8a112814f61603489f60b02300d4763de2c03014'",
      "print(payload)",
      "print('sha256=' + digest)"
    ],
    "missing": [
      "command"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://wwwhomes.uni-bielefeld.de/achim/addition_chain.html",
    "locator": "Inline CPython standard-library verifier executed by TheoremDB entry research on 2026-07-25"
  },
  "models": [],
  "continuation": null,
  "relations": [
    {
      "slug": "R485",
      "title": "An explicit addition chain reaches the target in 136 steps",
      "object_type": "claim",
      "relation": "verifies",
      "direction": "outgoing"
    },
    {
      "slug": "mersenne-127-addition-chain",
      "title": "mersenne 127 addition chain",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}