{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R486",
  "content_hash": null,
  "slug": "m127ac-claim-current-bounds",
  "type": "claim",
  "title": "The strongest located interval is 133 through 136",
  "summary": "A reported exhaustive Hamming-weight result gives the lower endpoint, while an explicit 136-step addition chain gives the upper endpoint.",
  "relevance": "For Shortest addition chain for the 127th Mersenne number, record m127ac-claim-current-bounds (“The strongest located interval is 133 through 136”) records a bound, answer, status fact, or structural consequence. The record states: A reported exhaustive Hamming-weight result gives the lower endpoint, while an explicit 136-step addition chain gives the upper endpoint.",
  "relevance_source": "recorded",
  "body": "Put\n\\[\nN=2^{127}-1=170141183460469231731687303715884105727.\n\\]\nThe strongest bound located in the literature and database audit is\n\\[\n133\\leq \\ell(N)\\leq136.\n\\]\n\nThe upper endpoint is independently replayed in this dataset. The lower endpoint uses Neill Clift's exhaustive verification of the Knuth-Stolarsky inequality for every integer of binary Hamming weight at most 128, as reported in Achim Flammenkamp's addition-chain database. Since\n\\[\n\\lambda(N)=\\lfloor\\log_2N\\rfloor=126,\n\\qquad \\nu(N)=127,\n\\]\nthat result gives\n\\[\n\\ell(N)\\geq126+\\lceil\\log_2 127\\rceil=133.\n\\]\nThe public report states the scope and completion date, November 2023, but the audit did not locate a compact certificate that can be replayed inside this fixture. For comparison, the published analytic theorem of Schönhage independently gives \\(\\ell(N)\\geq132\\).\n\nNo source found in the audit proves that 136 is optimal or supplies a chain of length at most 135. The four possible values 133, 134, 135, and 136 therefore remain open on the evidence recorded here.",
  "status": "supported",
  "evidence_grade": "sourced",
  "scope": {
    "kind": "bounded",
    "statement": "the ordinary addition-chain length of N=2^127-1",
    "bounds": {
      "mersenne_exponent": {
        "min": 127,
        "max": 127
      }
    },
    "exhaustive": false
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "claim",
    "citation": {
      "url": "https://wwwhomes.uni-bielefeld.de/achim/addition_chain.html",
      "locator": "Achim Flammenkamp, Shortest Addition Chains, Conjectures section, report that Neill Clift verified the Knuth-Stolarsky inequality for every n with v(n)<=128 by November 2023; upper endpoint replayed by m127ac-artifact-chain-replay"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://wwwhomes.uni-bielefeld.de/achim/addition_chain.html",
    "locator": "Achim Flammenkamp, Shortest Addition Chains, Conjectures section, report that Neill Clift verified the Knuth-Stolarsky inequality for every n with v(n)<=128 by November 2023; upper endpoint replayed by m127ac-artifact-chain-replay"
  },
  "models": [],
  "continuation": null,
  "relations": [
    {
      "slug": "R485",
      "title": "An explicit addition chain reaches the target in 136 steps",
      "object_type": "claim",
      "relation": "supports",
      "direction": "incoming"
    },
    {
      "slug": "R484",
      "title": "Published theory gives 132; the current enumeration report gives 133",
      "object_type": "attempt",
      "relation": "supports",
      "direction": "incoming"
    },
    {
      "slug": "R487",
      "title": "Three shorter lengths remain unresolved",
      "object_type": "claim",
      "relation": "refines",
      "direction": "incoming"
    },
    {
      "slug": "mersenne-127-addition-chain",
      "title": "mersenne 127 addition chain",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}