{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R484",
  "content_hash": null,
  "slug": "m127ac-attempt-lower-bound-audit",
  "type": "attempt",
  "title": "Published theory gives 132; the current enumeration report gives 133",
  "summary": "Schönhage's theorem is an independently checkable floor, while Clift's reported Hamming-weight sweep raises it by one.",
  "relevance": "For Shortest addition chain for the 127th Mersenne number, record m127ac-attempt-lower-bound-audit (“Published theory gives 132; the current enumeration report gives 133”) documents a concrete method, search boundary, or failed route. The record states: Schönhage's theorem is an independently checkable floor, while Clift's reported Hamming-weight sweep raises it by one.",
  "relevance_source": "recorded",
  "body": "Schönhage proved\n\\[\n\\ell(n)\\geq\\log_2 n+\\log_2\\nu(n)-2.13,\n\\]\nwhere \\(\\nu(n)\\) is the number of ones in the binary expansion. Substitution of \\(N=2^{127}-1\\) and \\(\\nu(N)=127\\) gives a right side of approximately \\(131.8586846868\\). Since chain length is integral,\n\\[\n\\ell(N)\\geq132.\n\\]\nThis is the strongest lower endpoint reproduced here solely from a peer-reviewed universal theorem.\n\nThe Knuth-Stolarsky inequality asserts\n\\[\n\\ell(n)\\geq\\lambda(n)+\\lceil\\log_2\\nu(n)\\rceil.\n\\]\nFlammenkamp's maintained database reports that Neill Clift completed an exhaustive verification for every target with \\(\\nu(n)\\leq128\\) in November 2023. Applying the reported result to the present target gives 133. The same page distinguishes this finite verified range from the unresolved universal conjecture.\n\nBrauer's 1939 paper supplies the star-chain construction behind the upper endpoint. Clift's 2011 paper gives an exact-search framework for point values, and the current additionchains.com site documents ongoing computations. The audit found no peer-reviewed or database entry settling \\(\\ell(2^{127}-1)\\), and no shorter explicit chain than the 136-step construction recorded here.",
  "status": "completed",
  "evidence_grade": "sourced",
  "scope": {
    "kind": "bounded",
    "statement": "lower bounds for 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": "attempt",
    "citation": {
      "url": "https://doi.org/10.1016/0304-3975(75)90008-0",
      "locator": "Arnold Schönhage, A lower bound for the length of addition chains, Theoretical Computer Science 1(1), 1975, pages 1-12; Achim Flammenkamp, Shortest Addition Chains, current Conjectures section; Neill M. Clift, Calculating optimal addition chains, Computing 91, 2011, pages 265-284"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.1016/0304-3975(75)90008-0",
    "locator": "Arnold Schönhage, A lower bound for the length of addition chains, Theoretical Computer Science 1(1), 1975, pages 1-12; Achim Flammenkamp, Shortest Addition Chains, current Conjectures section; Neill M. Clift, Calculating optimal addition chains, Computing 91, 2011, pages 265-284"
  },
  "models": [],
  "continuation": null,
  "relations": [
    {
      "slug": "R486",
      "title": "The strongest located interval is 133 through 136",
      "object_type": "claim",
      "relation": "supports",
      "direction": "outgoing"
    },
    {
      "slug": "mersenne-127-addition-chain",
      "title": "mersenne 127 addition chain",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}